Gleason's theorem, finite-dimensional: the reduction to the core lemma on S²

Category: 1-Mathlib (CSD-free; staged for upstream). The assembly of specs/gleason-feasibility.md: Layers A and C proved in this tree reduce Gleason's theorem for ℂᴺ, N ≥ 3, to one statement about the real sphere S² ⊂ ℝ³. That statement is proved in Gleason/General.lean (stage 57(e)); Gleason/Core.lean joins the two into the theorem.

• CoreLemma — Gleason's core lemma, as a proposition: every nonnegative frame function on S² is the restriction of a symmetric quadratic form. Gleason proved it with spherical harmonics (1957, §2); Cooke–Keane–Moran (1985) and Richman–Bridges (1999) proved it with elementary geometry of great circles. It is not proved in this file: the elementary proof is Gleason/Sphere.lean through Gleason/General.lean (frameFunction_regular_sphere), and Gleason/Core.lean supplies it here as coreLemma.
• ★★ ProjectionPackage.gleason_representation_of_core — Gleason's theorem from the core lemma: for N ≥ 3, every projection package on ℂᴺ is P ↦ Re Tr(ρ P) for a unique density matrix ρ. The chain: A2 restricts the frame function to every completely real 3-space (isFrameFunction_realRestrict); the core lemma makes each restriction a quadratic form; isRealPlaneRegular_of_triples transports that to every completely real plane; A3 (exists_isHermitian_of_isRealPlaneRegular) produces the Hermitian matrix; Layer C (existsUnique_density_of_frame_quadratic) makes it the unique density matrix.

This file on its own claims nothing: the theorem's only hypothesis beyond N ≥ 3 is CoreLemma, stated as a proposition so that the dependency is visible in the statement itself. The unconditional theorem is ProjectionPackage.gleason_representation in Gleason/Core.lean.

Source

Gleason 1957, J. Math. Mech. 6, 885; Cooke, Keane, Moran 1985, Math. Proc. Cambridge Philos. Soc. 98, 117; Richman, Bridges 1999, J. Funct. Anal. 162, 287.

def Gleason.CoreLemma : Prop

Gleason's core lemma, as a proposition. Every nonnegative frame function on the unit sphere of ℝ³ is the restriction of a symmetric quadratic form: for f with ∑ᵢ f (bᵢ) = W over every orthonormal basis and f ≥ 0 on the sphere, there is a symmetric A with f x = x ⬝ᵥ A x for every unit x.

Equations

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

theorem Gleason.ProjectionPackage.gleason_representation_of_core {N : ℕ} (hcore : CoreLemma) (hN : 3 ≤ N) (OP : ProjectionPackage N) : ∃! ρ : Matrix (Fin N) (Fin N) ℂ, ρ.PosSemidef ∧ ρ.trace = 1 ∧ ∀ (P : Matrix (Fin N) (Fin N) ℂ), IsStarProjection P → OP.p P = (ρ * P).trace.re

★★ Gleason's theorem for ℂᴺ, N ≥ 3, from the core lemma. For every projection package OP there is a unique density matrix ρ with OP.p P = Re Tr(ρ P) for every orthogonal projection P.