LF4 §14.2 spectral variance and ontic variance correspondence

Category: 3-Local (LF4 §14.2 follow-up — Hilbert ↔ ontic variance identity for any Hermitian observable, building on SpectralCarving.lean's integration headline).

For Hermitian A : Matrix (Fin N) (Fin N) ℂ and unit state ψ : EuclideanSpace ℂ (Fin N), the variance has both Hilbert and ontic spectral expressions:

Var_ψ(A) := ‖A ψ‖² − ⟨A⟩² = ∑ᵢ (λᵢ − ⟨A⟩)² · ‖⟨uᵢ, ψ⟩‖² (Hilbert spectral form) = ∫ (∑ᵢ (λᵢ − ⟨A⟩)² · 1_{R_i})(σ) dμψ (ontic spectral form)

where ⟨A⟩ = re ⟨ψ, A ψ⟩, λᵢ are the eigenvalues, uᵢ are an orthonormal eigenbasis (Matrix.IsHermitian.eigenvectorBasis), and R_i are the N-arc spectral regions from SpectralCarving.

Module contents

• Phase F.1 — inner_eigenvector_image (extracted from SpectralExpansion.lean's proof) and hilbert_norm_sq_apply_hermitian (‖A ψ‖² = ∑ᵢ λᵢ² · bornWeights), the Hilbert-side variance ingredient.

• Phase F.2 — spectralVariance hA ψ := ∑ᵢ (λᵢ − ⟨A⟩)² · bornWeights (the spectral form) plus spectralVariance_eq_hilbert_norm_sq_diff : spectralVariance = ‖A ψ‖² − ⟨A⟩² (the Hilbert ↔ spectral identity, deriving the standard QM Var = ⟨A²⟩ − ⟨A⟩² form via ‖A ψ‖² = re ⟨ψ, A² ψ⟩ for self-adjoint A).

• Phase F.3 — spectralOnticCentered := ∑ᵢ (λᵢ − ⟨A⟩)² · 1_{R_i} (the ontic counterpart) and the headline integral_spectralOnticCentered_eq_variance : ∫ spectralOnticCentered dμψ = spectralVariance hA ψ, the ontic ↔ Hilbert-spectral variance correspondence at the integration level. Composes the Phase D template (integral_finsetSum + diracProd_spectralRegion) with bornWeights_sum_eq_one.

Tier-2 posture (unchanged)

spectralVariance is defined as the spectral form. The Hilbert ↔ spectral identity is a genuine algebraic theorem (expanding (λᵢ − ⟨A⟩)² and using ∑ bornWeights = 1, ∑ λᵢ · bornWeights = ⟨A⟩, ∑ λᵢ² · bornWeights = ‖A ψ‖²). The ontic ↔ spectral identity is a genuine measure-theoretic theorem (per-region carving + linearity of integration). Both ends meet at the same value via structurally distinct machinery.

Axiom posture

Foundational triple only.

Phase F.1 — Hilbert variance helpers

theorem CSD.LF4.inner_eigenvector_image {N : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) (ψ : EuclideanSpace ℂ (Fin N)) (i : Fin N) : inner ℂ (hA.eigenvectorBasis i) ((Matrix.toEuclideanLin A) ψ) = ↑(hA.eigenvalues i) * inner ℂ (hA.eigenvectorBasis i) ψ

The eigenvalue equation projected onto an inner product: for Hermitian A and eigenvector uᵢ (of eigenvalue λᵢ), ⟨uᵢ, A ψ⟩ = (λᵢ : ℂ) · ⟨uᵢ, ψ⟩. Extracted from SpectralExpansion.lean's proof of hermitian_inner_spectral_expansion.

theorem CSD.LF4.hilbert_norm_sq_apply_hermitian {N : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) (ψ : EuclideanSpace ℂ (Fin N)) : ‖(Matrix.toEuclideanLin A) ψ‖ ^ 2 = ∑ i : Fin N, hA.eigenvalues i ^ 2 * bornWeights hA ψ i

Hilbert norm-squared spectral expansion: ‖A ψ‖² = ∑ᵢ λᵢ² · bornWeights i for any Hermitian A and any state ψ. Composes Parseval (OrthonormalBasis.sum_sq_norm_inner_right) with inner_eigenvector_image.

theorem CSD.LF4.hermitian_inner_spectral_expansion_re_bornWeights {N : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) (ψ : EuclideanSpace ℂ (Fin N)) : RCLike.re (inner ℂ ψ ((Matrix.toEuclideanLin A) ψ)) = ∑ i : Fin N, hA.eigenvalues i * bornWeights hA ψ i

bornWeights-form of the spectral expansion (the SpectralExpansion form uses the surface form ‖⟨uᵢ, ψ⟩‖²; this gives the bornWeights surface form, equal by definition, for ergonomics in proofs that mix the two).

Phase F.2 — Spectral variance and Hilbert match

noncomputable def CSD.LF4.spectralVariance {N : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) (ψ : EuclideanSpace ℂ (Fin N)) : ℝ

Spectral variance: the eigenvalue-deviation-squared sum weighted by the Born probabilities. By spectralVariance_eq_hilbert_norm_sq_diff this equals ‖A ψ‖² − ⟨A⟩², the standard QM variance ⟨A²⟩ − ⟨A⟩² for self-adjoint A.

Equations

• CSD.LF4.spectralVariance hA ψ = ∑ i : Fin N, (hA.eigenvalues i - RCLike.re (inner ℂ ψ ((Matrix.toEuclideanLin A) ψ))) ^ 2 * CSD.LF4.bornWeights hA ψ i

theorem CSD.LF4.spectralVariance_nonneg {N : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) (ψ : EuclideanSpace ℂ (Fin N)) : 0 ≤ spectralVariance hA ψ

theorem CSD.LF4.spectralVariance_eq_hilbert_norm_sq_diff {N : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ‖ψ‖ = 1) : spectralVariance hA ψ = ‖(Matrix.toEuclideanLin A) ψ‖ ^ 2 - RCLike.re (inner ℂ ψ ((Matrix.toEuclideanLin A) ψ)) ^ 2

Hilbert ↔ spectral variance identity: for any Hermitian A and unit ψ, spectralVariance hA ψ = ‖A ψ‖² − ⟨A⟩². The standard QM variance ⟨A²⟩ − ⟨A⟩² reduces to ‖A ψ‖² − ⟨A⟩² via ⟨ψ, A² ψ⟩ = ⟨A ψ, A ψ⟩ for self-adjoint A.

Phase F.3 — Ontic variance observable and integration headline

noncomputable def CSD.LF4.spectralOnticCentered {N M : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) (ψ : EuclideanSpace ℂ (Fin N)) : KSigma M → ℝ

Ontic centered spectral observable: the deviation-squared eigenvalue-weighted indicator sum over the N spectral outcome regions. Equals (spectralOntic hA ψ σ − ⟨A⟩)² for σ ∈ ⋃ᵢ R_i (which has full μψ-measure under hψ : ‖ψ‖ = 1); the integration identity below holds without invoking that a.e. equivalence.

Equations

• One or more equations did not get rendered due to their size.

theorem CSD.LF4.spectralOnticCentered_measurable {N M : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) (ψ : EuclideanSpace ℂ (Fin N)) : Measurable (spectralOnticCentered hA ψ)

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

§14.2 ontic ↔ Hilbert-spectral variance correspondence at the integration level: for any Hermitian A : Matrix (Fin N) (Fin N) ℂ and unit ψ : EuclideanSpace ℂ (Fin N), on any Kähler instance KSigma M with preparation (Dirac p₀) × vol_T²,

∫ spectralOnticCentered dμψ = spectralVariance hA ψ.

Composes diracProd_spectralRegion (per-region carving) with linearity of the Lebesgue integral over the finite eigenvalue sum. Combined with spectralVariance_eq_hilbert_norm_sq_diff, this gives the full Hilbert variance ↔ ontic variance correspondence on the Kähler instance.

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

Composite headline: under unit ψ, the integrated centered ontic observable matches the standard QM variance ‖A ψ‖² − ⟨A⟩².