LF4 §14.2 general N×N spectral expansion of the Hilbert expectation

Category: 3-Local (LF4 §14.2 — general Hermitian observable spectral expansion at the Hilbert level).

For any Hermitian matrix A : Matrix (Fin N) (Fin N) ℂ and any state ψ : EuclideanSpace ℂ (Fin N), the expectation ⟨ψ, A ψ⟩ decomposes as

⟨ψ, A ψ⟩ = ∑ᵢ λᵢ · ‖⟨uᵢ, ψ⟩‖²

where λᵢ : ℝ are the eigenvalues of A and uᵢ : EuclideanSpace ℂ (Fin N) are an orthonormal eigenbasis (both provided by Mathlib's Matrix.IsHermitian.eigenvalues and Matrix.IsHermitian.eigenvectorBasis).

This is the Hilbert side of the LF4 §14.2 general N×N observable correspondence. The ontic side carves N outcome regions of measure ‖⟨uᵢ, ψ⟩‖² (one per eigenvector) and integrates the eigenvalue-weighted indicator sum — that construction is per-state and built on top of this spectral identity. The headline result here is hermitian_inner_spectral_expansion.

What §14.2 General unlocks

• Variance identity: Var_ψ(A) = ∑ᵢ (λᵢ − ⟨A⟩)² · ‖⟨uᵢ, ψ⟩‖² follows by applying the spectral expansion to both ⟨A⟩ and ⟨A²⟩. The full Robertson–uncertainty bundle's per-observable §14 correspondence (matching ∫ A_ontic dμψ = ⟨ψ, A ψ⟩ AND ∫ (A_ontic − ⟨A⟩)² dμψ = Var(A)) composes via this identity plus the per-eigenvector carving.

• Multi-eigenvalue Hardy / Mermin–Peres lifts: observables that are NOT ±1-valued (e.g. spin-1, GHZ stabiliser generators, generic Hermitian operators) get their ontic counterparts via this same spectral pattern.

Proof route

Uses Mathlib's Matrix.IsHermitian.mulVec_eigenvectorBasis (eigenvalue equation A uᵢ = λᵢ • uᵢ), Matrix.isSymmetric_toEuclideanLin_iff.symm (self-adjointness of the linear-map action), and OrthonormalBasis.sum_inner_mul_inner (Parseval). The chain:

1. ⟨ψ, A ψ⟩ = ∑ᵢ ⟨ψ, uᵢ⟩ · ⟨uᵢ, A ψ⟩ (Parseval on the eigenbasis).
2. ⟨uᵢ, A ψ⟩ = ⟨A uᵢ, ψ⟩ = ⟨λᵢ • uᵢ, ψ⟩ = (λᵢ : ℂ) · ⟨uᵢ, ψ⟩ (self-adjoint + eigenequation; λᵢ real).
3. ⟨ψ, uᵢ⟩ · (λᵢ : ℂ) · ⟨uᵢ, ψ⟩ = (λᵢ : ℂ) · conj(⟨uᵢ, ψ⟩) · ⟨uᵢ, ψ⟩ = (λᵢ : ℂ) · ‖⟨uᵢ, ψ⟩‖².

Axiom posture

Foundational triple only.

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

§14.2 general N×N spectral expansion of the Hilbert expectation.

For any Hermitian A : Matrix (Fin N) (Fin N) ℂ and any ψ : EuclideanSpace ℂ (Fin N),

⟨ψ, A ψ⟩ = ∑ᵢ (λᵢ : ℂ) · ‖⟨uᵢ, ψ⟩‖²

where λᵢ = hA.eigenvalues i and uᵢ = hA.eigenvectorBasis i.

The action of A on ψ is taken through Matrix.toEuclideanLin (the canonical bounded linear map associated with the matrix on the EuclideanSpace L² model).

theorem CSD.LF4.hermitian_inner_spectral_expansion_re {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 * ‖inner ℂ (hA.eigenvectorBasis i) ψ‖ ^ 2

§14.2 general N×N spectral expansion: real-valued form.

The expectation ⟨ψ, A ψ⟩ of a Hermitian observable is a real number (its imaginary part vanishes), and admits the real spectral expansion

re ⟨ψ, A ψ⟩ = ∑ᵢ λᵢ · ‖⟨uᵢ, ψ⟩‖².

Real form is what variance/expectation/uncertainty arguments consume.