LF4 §14.2 Robertson uncertainty on the Kähler instance (ontic variance form)

Category: 3-Local (LF4 §14.2 follow-up — concrete Robertson bound expressed in terms of ontic-side integrated variances).

Glossary: https://glossary.constraintsurfacedynamics.com/robertson-uncertainty/ Plain-language, CSD-role and formal statements of the Robertson uncertainty relation, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

Connects CsdLean4/LF4/SpectralVariance.lean (the Hilbert ↔ ontic variance correspondence at the integration level) to CsdLean4/Empirical/QM/Uncertainty.lean (the QM Robertson bound on Hilbert variances). The composite gives the Robertson bound on ontic variances: for any pair of Hermitian matrices A, B : Matrix (Fin N) (Fin N) ℂ and unit ψ : EuclideanSpace ℂ (Fin N), on any Kähler instance with preparation Dirac p₀ × vol_T²,

(∫ A_centered_ontic dμψ) · (∫ B_centered_ontic dμψ) ≥ ¼ ‖⟨ψ, [A, B] ψ⟩‖².

Module contents

• variance_eq_norm_sq_sub_expectation_sq — generic Hilbert-space variance simplification: for symmetric T and unit ψ, Var T ψ = ‖T ψ‖² − (re ⟨ψ, T ψ⟩)². This is the standard QM identity Var = ⟨A²⟩ − ⟨A⟩² in the form needed to bridge SpectralVariance.

• QM_variance_eq_spectralVariance — the bridge: for Hermitian A and unit ψ, Empirical.Uncertainty.variance A.toEuclideanLin ψ = spectralVariance hA ψ.

• QM_variance_eq_integral_spectralOnticCentered — composition with the integration headline from SpectralCarving / SpectralVariance: Empirical.Uncertainty.variance A.toEuclideanLin ψ = ∫ spectralOnticCentered hA ψ dμψ on the Kähler instance.

• kahler_robertson_ontic_variance — the headline ontic-variance Robertson bound. Composes QM_variance_eq_integral_spectralOnticCentered (applied twice, to A and B) with the QM-side Empirical.Uncertainty.robertson_uncertainty (the abstract Hilbert Robertson bound) into a concrete inequality on the Kähler instance with the LHS expressed purely via ontic-side integrals.

Tier-2 posture (unchanged)

The bridge variance = spectralVariance = ∫ spectralOnticCentered dμψ composes three theorems that each compute the same value via structurally distinct machinery (Hilbert-space variance via norm-sub-sq; spectral expansion via Parseval + eigenvalue equation; ontic-side via N-arc carving + Lebesgue integral). The Robertson bound itself is QM-side Hilbert-only content (Cauchy–Schwarz + commutator algebra); the LF4 content is the realisation of that bound on ontic-side observables.

Axiom posture

Foundational triple only.

theorem CSD.LF4.variance_eq_norm_sq_sub_expectation_sq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {T : Module.End ℂ H} (hT : LinearMap.IsSymmetric T) {ψ : H} (hψ : ‖ψ‖ = 1) : Empirical.Uncertainty.variance T ψ = ‖T ψ‖ ^ 2 - RCLike.re (inner ℂ ψ (T ψ)) ^ 2

Variance equals norm-squared minus expectation-squared (under symmetric T and unit ψ). The standard QM Var = ⟨A²⟩ − ⟨A⟩² written via ‖T ψ‖² (which equals re ⟨ψ, T² ψ⟩ for self-adjoint T). Generic Hilbert-space statement; no matrix or Kähler structure.

theorem CSD.LF4.QM_variance_eq_spectralVariance {N : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ‖ψ‖ = 1) : Empirical.Uncertainty.variance (Matrix.toEuclideanLin A) ψ = spectralVariance hA ψ

Hilbert variance ↔ spectral variance bridge for Hermitian matrices on EuclideanSpace ℂ (Fin N) and unit ψ. Composes variance_eq_norm_sq_sub_expectation_sq (the QM-side simplification) with spectralVariance_eq_hilbert_norm_sq_diff (the spectral identity).

theorem CSD.LF4.QM_variance_eq_integral_spectralOnticCentered {N M : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ‖ψ‖ = 1) (p₀ : CPN M) : Empirical.Uncertainty.variance (Matrix.toEuclideanLin A) ψ = ∫ (σ : CPN M × KTorus), spectralOnticCentered hA ψ σ ∂(MeasureTheory.Measure.dirac p₀).prod MeasureTheory.volume

QM variance ↔ ontic-side integrated variance: composition of the spectral bridge with the integration headline. The Hilbert-space variance of a Hermitian matrix's action on a unit state, on the Kähler instance, equals the integral of the centered ontic spectral observable.

theorem CSD.LF4.kahler_robertson_ontic_variance {N M : ℕ} {A B : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ‖ψ‖ = 1) (p₀ : CPN M) : (∫ (σ : CPN M × KTorus), spectralOnticCentered hA ψ σ ∂(MeasureTheory.Measure.dirac p₀).prod MeasureTheory.volume) * ∫ (σ : CPN M × KTorus), spectralOnticCentered hB ψ σ ∂(MeasureTheory.Measure.dirac p₀).prod MeasureTheory.volume ≥ 1 / 4 * ‖inner ℂ ψ ((Matrix.toEuclideanLin A * Matrix.toEuclideanLin B - Matrix.toEuclideanLin B * Matrix.toEuclideanLin A) ψ)‖ ^ 2

Robertson uncertainty on ontic variances (the LF4 §14.2 realisation of the QM Robertson bound). For any pair of Hermitian matrices A, B : Matrix (Fin N) (Fin N) ℂ and unit ψ : EuclideanSpace ℂ (Fin N), on any Kähler instance KSigma M with preparation (Dirac p₀) × vol_T²,

(∫ spectralOnticCentered hA ψ dμψ) · (∫ spectralOnticCentered hB ψ dμψ) ≥ ¼ ‖⟨ψ, [A.toEuclideanLin, B.toEuclideanLin] ψ⟩‖².

Composes QM_variance_eq_integral_spectralOnticCentered (applied to A and B) with Empirical.Uncertainty.robertson_uncertainty (the QM Hilbert Robertson bound). The LHS is purely ontic; the RHS is the Hilbert-space commutator overlap (the Robertson lower bound).