Gleason's theorem for real Hilbert spaces

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #58, the A4 reduction of specs/gleason-feasibility.md: the real-space corollary of the core lemma proved in #57.

★★★ RealProjectionPackage.real_gleason_representation: for N ≥ 3, every assignment p on the orthogonal projections of ℝᴺ that is nonnegative, normalised and additive on orthogonal pairs is P ↦ Tr(ρ P) for a unique real density matrix ρ. The complex theorem (Gleason/Core.lean, #57) does not contain this one: a real inner product space is not a complex one, and the reduction runs through real 3-spaces rather than completely real planes.

The route

The real side mirrors the complex layers, which is cheaper than it looks because the Gram section of Gleason/ProjectionPackage.lean is already generic over RCLike:

• rankOneR, RealProjectionPackage, p_sum, frame and A1 (sum_frame_orthonormalBasis: the frame function sums to 1 over every real orthonormal basis);
• A2, isFrameFunction_restrictR: for an orthonormal family e in ℝᴺ the restriction x ↦ frame (∑ᵢ xᵢ eᵢ) is a frame function on ℝᵏ of weight p (∑ᵢ |eᵢ⟩⟨eᵢ|) — the weight is basis independent because the rank-one projections of a transported orthonormal basis sum to the same matrix (sum_rankOneR_combR, the Gram identity E B Bᵀ Eᵀ = E Eᵀ). For k = 3 the core lemma applies: ★ exists_isSymm_restrictR;
• the degree-2 extension extOf f v = ‖v‖² f (v/‖v‖), which is the quadratic form of the core lemma's matrix on the whole span of a triple (extOf_combR), hence a quadratic form on every plane (★ exists_extOf_plane, extending the plane's orthonormal pair to a triple with exists_orthonormal_tripleR), hence ★★ extOf_parallelogramR — the parallelogram law on ℝᴺ, by Gram–Schmidt on any two vectors;
• the real Jordan–von Neumann engine (IsQuadraticLikeR, polarR, polarMatrixR, ★ IsQuadraticLikeR.eq_dotProduct), giving ★★ exists_isSymm_sphere: A4, the frame function is the quadratic form of a symmetric matrix on the unit sphere;
• the descent: posSemidef_of_sphere_nonnegR, trace_eq_sum_sphereR, eq_of_sphere_quadForm_eqR, packaged as ★ quadraticForm_on_sphere_to_densityR, and the spectral step ★ p_eq_trace (eq_sum_eigenvalues_smul_rankOneR, eigenvalues_eq_zero_or_oneR), giving ★★ existsUnique_density_of_frame_quadraticR and the theorem.

Done differently from the plan's sketch. gleason-feasibility.md §2 priced A4 as "any u, u', v lie in a 3-space, so the polarisation is bilinear without any Cauchy equation". The proof here does not take that route: it mirrors the complex assembly, where the Cauchy step (additive_bounded_linear, whose local bound is 0 ≤ q ≤ ‖·‖²) is already proved and generic, and where only pairs — not triples — need to be placed inside an orthonormal triple. Reusing the engine is shorter than a locality argument for every instance of bilinearity, and the three-vector observation is not needed at all.

Honest scope

⚠️ The statement is for a projection package, as in the complex theorem. Gleason's own formulation is for a bare frame function; that version landed 2026-09-28 in Gleason/RealFrame.lean (BACKLOG #87), where the weight of a 3-space is shown basis-independent without a p on projections, by completing the triple with a fixed family of the orthogonal complement. The middle layer of this file is stated for any function quadratic on triples (exists_isSymm_sphere_of_quad) precisely so that both consumers share it. ⚠️ Finite dimensions only, N ≥ 3, as in #57. N = 2 is false for Gleason's theorem (the counterexamples are the classic ones) and nothing here suggests otherwise. ⚠️ The real layer duplicates the shape of the complex one rather than generalising it over RCLike: the complex ProjectionPackage and its twelve modules are pinned and consumed by LF2, and genericising them would ripple through the whole directory. The genuinely shared parts (the Gram section, additive_bounded_linear) are used, not copied.

Source

A. Gleason, Measures on the closed subspaces of a Hilbert space, J. Math. Mech. 6 (1957) 885 (§1 frame functions, the real theorem); R. Cooke, M. Keane, W. Moran, Math. Proc. Cambridge Philos. Soc. 98 (1985) 117; Gleason/Core.lean (#57, the core lemma), Gleason/ProjectionPackage.lean (the Gram section and IsFrameFunction), Gleason/Polarization.lean (additive_bounded_linear); specs/gleason-feasibility.md §2 (A4); specs/BACKLOG.md #58; specs/future-work.md.

Rank-one projections over ℝ

def Gleason.rankOneR {N : ℕ} (v : EuclideanSpace ℝ (Fin N)) : Matrix (Fin N) (Fin N) ℝ

The real rank-one projection onto v (a projection when ‖v‖ = 1).

Equations

• Gleason.rankOneR v = Matrix.vecMulVec v.ofLp (star v.ofLp)

theorem Gleason.rankOneR_apply {N : ℕ} (v : EuclideanSpace ℝ (Fin N)) (a c : Fin N) : rankOneR v a c = v.ofLp a * v.ofLp c

theorem Gleason.rankOneR_isHermitian {N : ℕ} (v : EuclideanSpace ℝ (Fin N)) : (rankOneR v).IsHermitian

theorem Gleason.rankOneR_isSymm {N : ℕ} (v : EuclideanSpace ℝ (Fin N)) : (rankOneR v).IsSymm

theorem Gleason.rankOneR_mul_rankOneR {N : ℕ} (v w : EuclideanSpace ℝ (Fin N)) : rankOneR v * rankOneR w = inner ℝ v w • Matrix.vecMulVec v.ofLp (star w.ofLp)

|v⟩⟨v| |w⟩⟨w| = ⟪v, w⟫ |v⟩⟨w|.

theorem Gleason.rankOneR_mul_self {N : ℕ} {v : EuclideanSpace ℝ (Fin N)} (hv : ‖v‖ = 1) : rankOneR v * rankOneR v = rankOneR v

theorem Gleason.rankOneR_mul_rankOneR_of_inner_eq_zero {N : ℕ} {v w : EuclideanSpace ℝ (Fin N)} (h : inner ℝ v w = 0) : rankOneR v * rankOneR w = 0

theorem Gleason.isStarProjection_rankOneR {N : ℕ} {v : EuclideanSpace ℝ (Fin N)} (hv : ‖v‖ = 1) : IsStarProjection (rankOneR v)

The real rank-one projection is an orthogonal projection for every unit vector.

theorem Gleason.rankOneR_smul {N : ℕ} (c : ℝ) (v : EuclideanSpace ℝ (Fin N)) : rankOneR (c • v) = c ^ 2 • rankOneR v

Scaling the vector scales the rank-one matrix by the square.

theorem Gleason.rankOneR_neg {N : ℕ} (v : EuclideanSpace ℝ (Fin N)) : rankOneR (-v) = rankOneR v

theorem Gleason.rankOneR_mul_rankOneR_of_orthonormal {N k : ℕ} {e : Fin k → EuclideanSpace ℝ (Fin N)} (he : Orthonormal ℝ e) {i j : Fin k} (hij : i ≠ j) : rankOneR (e i) * rankOneR (e j) = 0

theorem Gleason.sum_rankOneR_eq {N k : ℕ} (e : Fin k → EuclideanSpace ℝ (Fin N)) : ∑ i : Fin k, rankOneR (e i) = colMatrix e * (colMatrix e).conjTranspose

theorem Gleason.sum_rankOneR_orthonormalBasis {N : ℕ} (b : OrthonormalBasis (Fin N) ℝ (EuclideanSpace ℝ (Fin N))) : ∑ i : Fin N, rankOneR (b i) = 1

Resolution of the identity over a real orthonormal basis.

The real projection package

structure Gleason.RealProjectionPackage (N : ℕ) : Type

A real projection package on ℝᴺ: a nonnegative, normalised, orthogonally additive assignment on the orthogonal projections of a real inner product space.

• p : Matrix (Fin N) (Fin N) ℝ → ℝ

  The assignment.

• nonneg (P : Matrix (Fin N) (Fin N) ℝ) : IsStarProjection P → 0 ≤ self.p P

  0 ≤ p P for every projection.

• total_one : self.p 1 = 1

  p 1 = 1.

• additive (P Q : Matrix (Fin N) (Fin N) ℝ) : IsStarProjection P → IsStarProjection Q → P * Q = 0 → self.p (P + Q) = self.p P + self.p Q

  p (P + Q) = p P + p Q for orthogonal projections.

theorem Gleason.RealProjectionPackage.p_zero {N : ℕ} (OP : RealProjectionPackage N) : OP.p 0 = 0

theorem Gleason.RealProjectionPackage.p_le_one {N : ℕ} (OP : RealProjectionPackage N) {P : Matrix (Fin N) (Fin N) ℝ} (hP : IsStarProjection P) : OP.p P ≤ 1

theorem Gleason.RealProjectionPackage.isStarProjection_sum {N : ℕ} {ι : Type u_1} (P : ι → Matrix (Fin N) (Fin N) ℝ) (hP : ∀ (i : ι), IsStarProjection (P i)) (horth : ∀ (i j : ι), i ≠ j → P i * P j = 0) (s : Finset ι) : IsStarProjection (∑ i ∈ s, P i)

A finite sum of pairwise-orthogonal projections is a projection.

theorem Gleason.RealProjectionPackage.p_sum {N : ℕ} (OP : RealProjectionPackage N) {ι : Type u_1} (P : ι → Matrix (Fin N) (Fin N) ℝ) (hP : ∀ (i : ι), IsStarProjection (P i)) (horth : ∀ (i j : ι), i ≠ j → P i * P j = 0) (s : Finset ι) : OP.p (∑ i ∈ s, P i) = ∑ i ∈ s, OP.p (P i)

Additivity over any finite family of pairwise-orthogonal projections.

def Gleason.RealProjectionPackage.frame {N : ℕ} (OP : RealProjectionPackage N) (v : EuclideanSpace ℝ (Fin N)) : ℝ

The frame function of a real package.

Equations

• OP.frame v = OP.p (Gleason.rankOneR v)

theorem Gleason.RealProjectionPackage.frame_nonneg {N : ℕ} (OP : RealProjectionPackage N) {v : EuclideanSpace ℝ (Fin N)} (hv : ‖v‖ = 1) : 0 ≤ OP.frame v

theorem Gleason.RealProjectionPackage.frame_le_one {N : ℕ} (OP : RealProjectionPackage N) {v : EuclideanSpace ℝ (Fin N)} (hv : ‖v‖ = 1) : OP.frame v ≤ 1

theorem Gleason.RealProjectionPackage.frame_neg {N : ℕ} (OP : RealProjectionPackage N) (v : EuclideanSpace ℝ (Fin N)) : OP.frame (-v) = OP.frame v

theorem Gleason.RealProjectionPackage.p_sum_rankOneR {N : ℕ} (OP : RealProjectionPackage N) {k : ℕ} {e : Fin k → EuclideanSpace ℝ (Fin N)} (he : Orthonormal ℝ e) : OP.p (∑ i : Fin k, rankOneR (e i)) = ∑ i : Fin k, OP.frame (e i)

Additivity over the rank-one projections of an orthonormal family.

theorem Gleason.RealProjectionPackage.sum_frame_orthonormalBasis {N : ℕ} (OP : RealProjectionPackage N) (b : OrthonormalBasis (Fin N) ℝ (EuclideanSpace ℝ (Fin N))) : ∑ i : Fin N, OP.frame (b i) = 1

A1 over ℝ. The frame function sums to 1 over every real orthonormal basis.

theorem Gleason.RealProjectionPackage.isFrameFunction_frame {N : ℕ} (OP : RealProjectionPackage N) : IsFrameFunction ℝ OP.frame 1

Restriction to the span of an orthonormal family

def Gleason.combR {N k : ℕ} (e : Fin k → EuclideanSpace ℝ (Fin N)) (x : EuclideanSpace ℝ (Fin k)) : EuclideanSpace ℝ (Fin N)

The point of ℝᴺ with coordinates x in the family e.

Equations

• Gleason.combR e x = ∑ i : Fin k, x.ofLp i • e i

theorem Gleason.colMatrix_combR {N k : ℕ} (e : Fin k → EuclideanSpace ℝ (Fin N)) (b : Fin k → EuclideanSpace ℝ (Fin k)) : (colMatrix fun (j : Fin k) => combR e (b j)) = colMatrix e * colMatrix b

theorem Gleason.orthonormal_combR {N k : ℕ} {e : Fin k → EuclideanSpace ℝ (Fin N)} (he : Orthonormal ℝ e) {b : Fin k → EuclideanSpace ℝ (Fin k)} (hb : Orthonormal ℝ b) : Orthonormal ℝ fun (j : Fin k) => combR e (b j)

Transporting a real orthonormal family through an orthonormal e gives an orthonormal family: Gram = Bᵀ (Eᵀ E) B = Bᵀ B = 1.

theorem Gleason.sum_rankOneR_combR {N k : ℕ} (e : Fin k → EuclideanSpace ℝ (Fin N)) (b : OrthonormalBasis (Fin k) ℝ (EuclideanSpace ℝ (Fin k))) : ∑ j : Fin k, rankOneR (combR e (b j)) = ∑ i : Fin k, rankOneR (e i)

The rank-one projections of a transported orthonormal basis sum to those of e.

theorem Gleason.norm_combR {N k : ℕ} {e : Fin k → EuclideanSpace ℝ (Fin N)} (he : Orthonormal ℝ e) {x : EuclideanSpace ℝ (Fin k)} (hx : ‖x‖ = 1) : ‖combR e x‖ = 1

A unit vector of coordinates gives a unit vector of ℝᴺ.

def Gleason.RealProjectionPackage.restrictR {N : ℕ} (OP : RealProjectionPackage N) {k : ℕ} (e : Fin k → EuclideanSpace ℝ (Fin N)) (x : EuclideanSpace ℝ (Fin k)) : ℝ

The restriction of the frame function to the span of an orthonormal family.

Equations

• OP.restrictR e x = OP.frame (Gleason.combR e x)

theorem Gleason.RealProjectionPackage.isFrameFunction_restrictR {N : ℕ} (OP : RealProjectionPackage N) {k : ℕ} {e : Fin k → EuclideanSpace ℝ (Fin N)} (he : Orthonormal ℝ e) : IsFrameFunction ℝ (OP.restrictR e) (OP.p (∑ i : Fin k, rankOneR (e i)))

A2 over ℝ. The restriction is a real frame function of weight p (∑ᵢ |eᵢ⟩⟨eᵢ|).

theorem Gleason.RealProjectionPackage.restrictR_nonneg {N : ℕ} (OP : RealProjectionPackage N) {k : ℕ} {e : Fin k → EuclideanSpace ℝ (Fin N)} (he : Orthonormal ℝ e) {x : EuclideanSpace ℝ (Fin k)} (hx : ‖x‖ = 1) : 0 ≤ OP.restrictR e x

theorem Gleason.RealProjectionPackage.exists_isSymm_restrictR {N : ℕ} (OP : RealProjectionPackage N) {e : Fin 3 → EuclideanSpace ℝ (Fin N)} (he : Orthonormal ℝ e) : ∃ (A : Matrix (Fin 3) (Fin 3) ℝ), A.IsSymm ∧ ∀ (x : EuclideanSpace ℝ (Fin 3)), ‖x‖ = 1 → OP.frame (combR e x) = x.ofLp ⬝ᵥ A.mulVec x.ofLp

★ The core lemma, applied to a triple: the frame function of a real package is a symmetric quadratic form on the unit sphere of the span of every orthonormal triple.

The real polarisation engine

structure Gleason.IsQuadraticLikeR {N : ℕ} (q : EuclideanSpace ℝ (Fin N) → ℝ) : Prop

A real quadratic-like function on ℝᴺ: degree-2 homogeneous, obeying the parallelogram law, and squeezed between 0 and ‖·‖². The last two conditions replace continuity in the Jordan–von Neumann argument (polarR_smul_left).

• smul (c : ℝ) (v : EuclideanSpace ℝ (Fin N)) : q (c • v) = c ^ 2 * q v

  q (c • v) = c² q v.

• parallelogram (u v : EuclideanSpace ℝ (Fin N)) : q (u + v) + q (u - v) = 2 * q u + 2 * q v

  The parallelogram law.

• nonneg (v : EuclideanSpace ℝ (Fin N)) : 0 ≤ q v

  0 ≤ q.

• le_normSq (v : EuclideanSpace ℝ (Fin N)) : q v ≤ ‖v‖ ^ 2

  q v ≤ ‖v‖².

def Gleason.polarR {N : ℕ} (q : EuclideanSpace ℝ (Fin N) → ℝ) (u v : EuclideanSpace ℝ (Fin N)) : ℝ

The real polarisation difference polarR q u v = q (u + v) − q (u − v), four times the symmetric bilinear form being reconstructed.

Equations

• Gleason.polarR q u v = q (u + v) - q (u - v)

noncomputable def Gleason.polarMatrixR {N : ℕ} (q : EuclideanSpace ℝ (Fin N) → ℝ) : Matrix (Fin N) (Fin N) ℝ

The matrix of the polarised form on the standard basis.

Equations

• Gleason.polarMatrixR q = Matrix.of fun (j k : Fin N) => Gleason.polarR q (EuclideanSpace.single j 1) (EuclideanSpace.single k 1) / 4

theorem Gleason.euclidean_sum_singleR {N : ℕ} (v : EuclideanSpace ℝ (Fin N)) : ∑ i : Fin N, v.ofLp i • EuclideanSpace.single i 1 = v

Standard-basis expansion in a real EuclideanSpace.

theorem Gleason.IsQuadraticLikeR.zero {N : ℕ} {q : EuclideanSpace ℝ (Fin N) → ℝ} (hq : IsQuadraticLikeR q) : q 0 = 0

theorem Gleason.IsQuadraticLikeR.neg {N : ℕ} {q : EuclideanSpace ℝ (Fin N) → ℝ} (hq : IsQuadraticLikeR q) (v : EuclideanSpace ℝ (Fin N)) : q (-v) = q v

theorem Gleason.IsQuadraticLikeR.polarR_symm {N : ℕ} {q : EuclideanSpace ℝ (Fin N) → ℝ} (hq : IsQuadraticLikeR q) (u v : EuclideanSpace ℝ (Fin N)) : polarR q u v = polarR q v u

theorem Gleason.IsQuadraticLikeR.polarR_zero_left {N : ℕ} {q : EuclideanSpace ℝ (Fin N) → ℝ} (hq : IsQuadraticLikeR q) (v : EuclideanSpace ℝ (Fin N)) : polarR q 0 v = 0

theorem Gleason.IsQuadraticLikeR.polarR_add_half {N : ℕ} {q : EuclideanSpace ℝ (Fin N) → ℝ} (hq : IsQuadraticLikeR q) (u w v : EuclideanSpace ℝ (Fin N)) : polarR q u v + polarR q w v = 2 * polarR q (2⁻¹ • (u + w)) v

The halving identity (Jordan–von Neumann core).

theorem Gleason.IsQuadraticLikeR.polarR_add_left {N : ℕ} {q : EuclideanSpace ℝ (Fin N) → ℝ} (hq : IsQuadraticLikeR q) (u w v : EuclideanSpace ℝ (Fin N)) : polarR q (u + w) v = polarR q u v + polarR q w v

Additivity of polarR in the first slot.

theorem Gleason.IsQuadraticLikeR.polarR_smul_left {N : ℕ} {q : EuclideanSpace ℝ (Fin N) → ℝ} (hq : IsQuadraticLikeR q) (t : ℝ) (u v : EuclideanSpace ℝ (Fin N)) : polarR q (t • u) v = t * polarR q u v

Real homogeneity of polarR in the first slot, through additive_bounded_linear.

theorem Gleason.IsQuadraticLikeR.polarR_add_right {N : ℕ} {q : EuclideanSpace ℝ (Fin N) → ℝ} (hq : IsQuadraticLikeR q) (u v w : EuclideanSpace ℝ (Fin N)) : polarR q u (v + w) = polarR q u v + polarR q u w

theorem Gleason.IsQuadraticLikeR.polarR_smul_right {N : ℕ} {q : EuclideanSpace ℝ (Fin N) → ℝ} (hq : IsQuadraticLikeR q) (t : ℝ) (u v : EuclideanSpace ℝ (Fin N)) : polarR q u (t • v) = t * polarR q u v

theorem Gleason.IsQuadraticLikeR.polarR_self {N : ℕ} {q : EuclideanSpace ℝ (Fin N) → ℝ} (hq : IsQuadraticLikeR q) (v : EuclideanSpace ℝ (Fin N)) : polarR q v v = 4 * q v

polarR q v v = 4 q v.

theorem Gleason.IsQuadraticLikeR.polarR_sum_left {N : ℕ} {q : EuclideanSpace ℝ (Fin N) → ℝ} (hq : IsQuadraticLikeR q) {ι : Type u_1} (s : Finset ι) (c : ι → ℝ) (f : ι → EuclideanSpace ℝ (Fin N)) (v : EuclideanSpace ℝ (Fin N)) : polarR q (∑ i ∈ s, c i • f i) v = ∑ i ∈ s, c i * polarR q (f i) v

theorem Gleason.IsQuadraticLikeR.polarR_sum_right {N : ℕ} {q : EuclideanSpace ℝ (Fin N) → ℝ} (hq : IsQuadraticLikeR q) {ι : Type u_1} (s : Finset ι) (c : ι → ℝ) (f : ι → EuclideanSpace ℝ (Fin N)) (v : EuclideanSpace ℝ (Fin N)) : polarR q v (∑ i ∈ s, c i • f i) = ∑ i ∈ s, c i * polarR q v (f i)

theorem Gleason.IsQuadraticLikeR.polarMatrixR_isSymm {N : ℕ} {q : EuclideanSpace ℝ (Fin N) → ℝ} (hq : IsQuadraticLikeR q) : (polarMatrixR q).IsSymm

theorem Gleason.IsQuadraticLikeR.eq_dotProduct {N : ℕ} {q : EuclideanSpace ℝ (Fin N) → ℝ} (hq : IsQuadraticLikeR q) (v : EuclideanSpace ℝ (Fin N)) : q v = v.ofLp ⬝ᵥ (polarMatrixR q).mulVec v.ofLp

★ q is the quadratic form of polarMatrixR q.

The degree-2 extension of a function quadratic on triples

This layer is stated for a bare function f on the sphere and a hypothesis hquad saying that f is a symmetric quadratic form on the span of every orthonormal triple. Both consumers of the layer supply hquad from Gleason's core lemma: RealProjectionPackage.exists_isSymm_sphere for a projection package (exists_isSymm_restrictR), and Gleason/RealFrame.lean for a bare frame function (BACKLOG #87).

noncomputable def Gleason.extOf {N : ℕ} (f : EuclideanSpace ℝ (Fin N) → ℝ) (v : EuclideanSpace ℝ (Fin N)) : ℝ

The degree-2 extension of a function on the sphere: extOf f v = ‖v‖² f (v / ‖v‖), and 0 at 0 (the factor ‖v‖² kills it).

Equations

• Gleason.extOf f v = ‖v‖ ^ 2 * f (‖v‖⁻¹ • v)

theorem Gleason.extOf_of_norm_one {N : ℕ} (f : EuclideanSpace ℝ (Fin N) → ℝ) {v : EuclideanSpace ℝ (Fin N)} (hv : ‖v‖ = 1) : extOf f v = f v

@[simp]

theorem Gleason.extOf_zero {N : ℕ} (f : EuclideanSpace ℝ (Fin N) → ℝ) : extOf f 0 = 0

theorem Gleason.norm_inv_smul_selfR {N : ℕ} {v : EuclideanSpace ℝ (Fin N)} (hv : v ≠ 0) : ‖‖v‖⁻¹ • v‖ = 1

theorem Gleason.extOf_smul {N : ℕ} {f : EuclideanSpace ℝ (Fin N) → ℝ} (hneg : ∀ (u : EuclideanSpace ℝ (Fin N)), ‖u‖ = 1 → f (-u) = f u) (c : ℝ) (v : EuclideanSpace ℝ (Fin N)) : extOf f (c • v) = c ^ 2 * extOf f v

extOf f is degree-2 homogeneous, given that f is even on the sphere.

theorem Gleason.extOf_nonneg {N : ℕ} {f : EuclideanSpace ℝ (Fin N) → ℝ} (h0 : ∀ (v : EuclideanSpace ℝ (Fin N)), ‖v‖ = 1 → 0 ≤ f v) (v : EuclideanSpace ℝ (Fin N)) : 0 ≤ extOf f v

theorem Gleason.extOf_le_normSq {N : ℕ} {f : EuclideanSpace ℝ (Fin N) → ℝ} (hub : ∀ (v : EuclideanSpace ℝ (Fin N)), ‖v‖ = 1 → f v ≤ 1) (v : EuclideanSpace ℝ (Fin N)) : extOf f v ≤ ‖v‖ ^ 2

The extension on the span of an orthonormal triple

theorem Gleason.combR_smul {N k : ℕ} (e : Fin k → EuclideanSpace ℝ (Fin N)) (c : ℝ) (x : EuclideanSpace ℝ (Fin k)) : combR e (c • x) = c • combR e x

theorem Gleason.dotProduct_mulVec_smulR {k : ℕ} (A : Matrix (Fin k) (Fin k) ℝ) (c : ℝ) (x : Fin k → ℝ) : c • x ⬝ᵥ A.mulVec (c • x) = c ^ 2 * x ⬝ᵥ A.mulVec x

theorem Gleason.extOf_combR {N : ℕ} {f : EuclideanSpace ℝ (Fin N) → ℝ} (hneg : ∀ (u : EuclideanSpace ℝ (Fin N)), ‖u‖ = 1 → f (-u) = f u) {k : ℕ} {e : Fin k → EuclideanSpace ℝ (Fin N)} (he : Orthonormal ℝ e) {A : Matrix (Fin k) (Fin k) ℝ} (hA : ∀ (x : EuclideanSpace ℝ (Fin k)), ‖x‖ = 1 → f (combR e x) = x.ofLp ⬝ᵥ A.mulVec x.ofLp) (x : EuclideanSpace ℝ (Fin k)) : extOf f (combR e x) = x.ofLp ⬝ᵥ A.mulVec x.ofLp

The extension on the span of an orthonormal family is the quadratic form the core lemma gives, now at every point and not only on the sphere.

Extending an orthonormal pair to a triple

theorem Gleason.exists_orthonormal_tripleR {N : ℕ} (hN : 3 ≤ N) {x y : EuclideanSpace ℝ (Fin N)} (hxy : Orthonormal ℝ ![x, y]) : ∃ (z : EuclideanSpace ℝ (Fin N)), Orthonormal ℝ ![x, y, z]

An orthonormal pair in ℝᴺ, N ≥ 3, extends to an orthonormal triple.

theorem Gleason.combR_two {N : ℕ} (e : Fin 3 → EuclideanSpace ℝ (Fin N)) (a b : ℝ) : combR e !₂[a, b, 0] = a • e 0 + b • e 1

The coordinates (a, b, 0) of a plane vector inside a triple.

theorem Gleason.exists_extOf_plane {N : ℕ} {f : EuclideanSpace ℝ (Fin N) → ℝ} (hquad : ∀ (e : Fin 3 → EuclideanSpace ℝ (Fin N)), Orthonormal ℝ e → ∃ (A : Matrix (Fin 3) (Fin 3) ℝ), A.IsSymm ∧ ∀ (x : EuclideanSpace ℝ (Fin 3)), ‖x‖ = 1 → f (combR e x) = x.ofLp ⬝ᵥ A.mulVec x.ofLp) (hneg : ∀ (u : EuclideanSpace ℝ (Fin N)), ‖u‖ = 1 → f (-u) = f u) (hN : 3 ≤ N) {x y : EuclideanSpace ℝ (Fin N)} (hxy : Orthonormal ℝ ![x, y]) : ∃ (c₀ : ℝ) (c₁ : ℝ) (c₂ : ℝ), ∀ (a b : ℝ), extOf f (a • x + b • y) = c₀ * a ^ 2 + c₁ * a * b + c₂ * b ^ 2

The extension is a quadratic form on every plane spanned by an orthonormal pair: extend the pair to a triple (N ≥ 3) and read off the core lemma's matrix.

theorem Gleason.extOf_parallelogramR {N : ℕ} {f : EuclideanSpace ℝ (Fin N) → ℝ} (hquad : ∀ (e : Fin 3 → EuclideanSpace ℝ (Fin N)), Orthonormal ℝ e → ∃ (A : Matrix (Fin 3) (Fin 3) ℝ), A.IsSymm ∧ ∀ (x : EuclideanSpace ℝ (Fin 3)), ‖x‖ = 1 → f (combR e x) = x.ofLp ⬝ᵥ A.mulVec x.ofLp) (hneg : ∀ (u : EuclideanSpace ℝ (Fin N)), ‖u‖ = 1 → f (-u) = f u) (hN : 3 ≤ N) (u v : EuclideanSpace ℝ (Fin N)) : extOf f (u + v) + extOf f (u - v) = 2 * extOf f u + 2 * extOf f v

The parallelogram law on ℝᴺ. Any two vectors lie in a plane spanned by an orthonormal pair (Gram–Schmidt), and every such plane sits inside an orthonormal triple, where the core lemma makes the extension a quadratic form.

theorem Gleason.isQuadraticLikeR_extOf {N : ℕ} {f : EuclideanSpace ℝ (Fin N) → ℝ} (hquad : ∀ (e : Fin 3 → EuclideanSpace ℝ (Fin N)), Orthonormal ℝ e → ∃ (A : Matrix (Fin 3) (Fin 3) ℝ), A.IsSymm ∧ ∀ (x : EuclideanSpace ℝ (Fin 3)), ‖x‖ = 1 → f (combR e x) = x.ofLp ⬝ᵥ A.mulVec x.ofLp) (hneg : ∀ (u : EuclideanSpace ℝ (Fin N)), ‖u‖ = 1 → f (-u) = f u) (h0 : ∀ (v : EuclideanSpace ℝ (Fin N)), ‖v‖ = 1 → 0 ≤ f v) (hub : ∀ (v : EuclideanSpace ℝ (Fin N)), ‖v‖ = 1 → f v ≤ 1) (hN : 3 ≤ N) : IsQuadraticLikeR (extOf f)

The extension is quadratic-like: the four hypotheses of the Jordan–von Neumann engine.

theorem Gleason.exists_isSymm_sphere_of_quad {N : ℕ} {f : EuclideanSpace ℝ (Fin N) → ℝ} (hquad : ∀ (e : Fin 3 → EuclideanSpace ℝ (Fin N)), Orthonormal ℝ e → ∃ (A : Matrix (Fin 3) (Fin 3) ℝ), A.IsSymm ∧ ∀ (x : EuclideanSpace ℝ (Fin 3)), ‖x‖ = 1 → f (combR e x) = x.ofLp ⬝ᵥ A.mulVec x.ofLp) (hneg : ∀ (u : EuclideanSpace ℝ (Fin N)), ‖u‖ = 1 → f (-u) = f u) (h0 : ∀ (v : EuclideanSpace ℝ (Fin N)), ‖v‖ = 1 → 0 ≤ f v) (hub : ∀ (v : EuclideanSpace ℝ (Fin N)), ‖v‖ = 1 → f v ≤ 1) (hN : 3 ≤ N) : ∃ (A : Matrix (Fin N) (Fin N) ℝ), A.IsSymm ∧ ∀ (v : EuclideanSpace ℝ (Fin N)), ‖v‖ = 1 → f v = v.ofLp ⬝ᵥ A.mulVec v.ofLp

★★ A4, the real reduction. A function on the unit sphere of ℝᴺ (N ≥ 3) that is even, between 0 and 1, and a symmetric quadratic form on the span of every orthonormal triple, is the quadratic form of a single symmetric matrix.

theorem Gleason.RealProjectionPackage.exists_isSymm_sphere {N : ℕ} (OP : RealProjectionPackage N) (hN : 3 ≤ N) : ∃ (A : Matrix (Fin N) (Fin N) ℝ), A.IsSymm ∧ ∀ (v : EuclideanSpace ℝ (Fin N)), ‖v‖ = 1 → OP.frame v = v.ofLp ⬝ᵥ A.mulVec v.ofLp

★★ A4 for a projection package. For N ≥ 3 the frame function of a real projection package is the quadratic form of a symmetric matrix on the unit sphere.

Matrix facts for the real descent

theorem Gleason.isHermitian_of_isSymmR {N : ℕ} {A : Matrix (Fin N) (Fin N) ℝ} (hA : A.IsSymm) : A.IsHermitian

theorem Gleason.isSymm_of_isHermitianR {N : ℕ} {A : Matrix (Fin N) (Fin N) ℝ} (hA : A.IsHermitian) : A.IsSymm

theorem Gleason.dotProduct_mulVec_singleR {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ) (i : Fin N) : (EuclideanSpace.single i 1).ofLp ⬝ᵥ A.mulVec (EuclideanSpace.single i 1).ofLp = A i i

The quadratic form at a standard basis vector is the diagonal entry.

theorem Gleason.trace_eq_sum_sphereR {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ) : A.trace = ∑ i : Fin N, (EuclideanSpace.single i 1).ofLp ⬝ᵥ A.mulVec (EuclideanSpace.single i 1).ofLp

The trace is the sum of the quadratic form over the standard basis.

theorem Gleason.exists_norm_one_smul_eqR {N : ℕ} {x : Fin N → ℝ} (hx : x ≠ 0) : ∃ (r : ℝ) (v : EuclideanSpace ℝ (Fin N)), 0 < r ∧ ‖v‖ = 1 ∧ x = r • v.ofLp

A nonzero real coordinate vector is a positive multiple of a unit vector.

theorem Gleason.posSemidef_of_sphere_nonnegR {N : ℕ} {A : Matrix (Fin N) (Fin N) ℝ} (hA : A.IsHermitian) (h : ∀ (v : EuclideanSpace ℝ (Fin N)), ‖v‖ = 1 → 0 ≤ v.ofLp ⬝ᵥ A.mulVec v.ofLp) : A.PosSemidef

A symmetric matrix with nonnegative quadratic form on the unit sphere is positive semidefinite.

theorem Gleason.eq_of_sphere_quadForm_eqR {N : ℕ} {A B : Matrix (Fin N) (Fin N) ℝ} (hA : A.IsSymm) (hB : B.IsSymm) (h : ∀ (v : EuclideanSpace ℝ (Fin N)), ‖v‖ = 1 → v.ofLp ⬝ᵥ A.mulVec v.ofLp = v.ofLp ⬝ᵥ B.mulVec v.ofLp) : A = B

A real symmetric matrix is determined by its quadratic form on the unit sphere.

theorem Gleason.quadraticForm_on_sphere_to_densityR {N : ℕ} {A : Matrix (Fin N) (Fin N) ℝ} (hA : A.IsSymm) {f : EuclideanSpace ℝ (Fin N) → ℝ} (hf : ∀ (v : EuclideanSpace ℝ (Fin N)), ‖v‖ = 1 → f v = v.ofLp ⬝ᵥ A.mulVec v.ofLp) (h0 : ∀ (v : EuclideanSpace ℝ (Fin N)), ‖v‖ = 1 → 0 ≤ f v) (h1 : ∑ i : Fin N, f (EuclideanSpace.single i 1) = 1) : A.PosSemidef ∧ A.trace = 1 ∧ ∀ (B : Matrix (Fin N) (Fin N) ℝ), B.IsSymm → (∀ (v : EuclideanSpace ℝ (Fin N)), ‖v‖ = 1 → f v = v.ofLp ⬝ᵥ B.mulVec v.ofLp) → B = A

★ From a quadratic form on the sphere to a real density matrix.

theorem Matrix.IsHermitian.eq_sum_eigenvalues_smul_rankOneR {N : ℕ} {A : Matrix (Fin N) (Fin N) ℝ} (hA : A.IsHermitian) : A = ∑ i : Fin N, hA.eigenvalues i • Gleason.rankOneR (hA.eigenvectorBasis i)

Spectral resolution as a sum of real rank-ones.

theorem Gleason.eigenvalues_eq_zero_or_oneR {N : ℕ} {P : Matrix (Fin N) (Fin N) ℝ} (hP : IsStarProjection P) (hPh : P.IsHermitian) (i : Fin N) : hPh.eigenvalues i = 0 ∨ hPh.eigenvalues i = 1

The eigenvalues of a real orthogonal projection are 0 or 1.

theorem Gleason.trace_mul_rankOneR {N : ℕ} (R : Matrix (Fin N) (Fin N) ℝ) (v : EuclideanSpace ℝ (Fin N)) : (R * rankOneR v).trace = v.ofLp ⬝ᵥ R.mulVec v.ofLp

Tr(R · |v⟩⟨v|) = ⟪v, R v⟫ over ℝ.

theorem Gleason.RealProjectionPackage.isStarProjection_smul_rankOneR {N : ℕ} {l : ℝ} (hl : l = 0 ∨ l = 1) {b : EuclideanSpace ℝ (Fin N)} (hb : ‖b‖ = 1) : IsStarProjection (l • rankOneR b)

The weighted rank-one λ • |b⟩⟨b| with λ ∈ {0, 1} is a projection.

theorem Gleason.RealProjectionPackage.p_smul_rankOneR {N : ℕ} (OP : RealProjectionPackage N) {l : ℝ} (hl : l = 0 ∨ l = 1) (b : EuclideanSpace ℝ (Fin N)) : OP.p (l • rankOneR b) = l * OP.frame b

p (λ • |b⟩⟨b|) = λ · frame b for λ ∈ {0, 1}.

theorem Gleason.RealProjectionPackage.p_eq_trace {N : ℕ} (OP : RealProjectionPackage N) {A : Matrix (Fin N) (Fin N) ℝ} (hf : ∀ (v : EuclideanSpace ℝ (Fin N)), ‖v‖ = 1 → OP.frame v = v.ofLp ⬝ᵥ A.mulVec v.ofLp) {P : Matrix (Fin N) (Fin N) ℝ} (hP : IsStarProjection P) : OP.p P = (A * P).trace

The projection descent over ℝ. If the frame function is the quadratic form of A on the unit sphere, then p P = Tr(A P) for every orthogonal projection P.

theorem Gleason.RealProjectionPackage.existsUnique_density_of_frame_quadraticR {N : ℕ} (OP : RealProjectionPackage N) {A : Matrix (Fin N) (Fin N) ℝ} (hA : A.IsSymm) (hf : ∀ (v : EuclideanSpace ℝ (Fin N)), ‖v‖ = 1 → OP.frame v = v.ofLp ⬝ᵥ A.mulVec v.ofLp) : ∃! ρ : Matrix (Fin N) (Fin N) ℝ, ρ.PosSemidef ∧ ρ.trace = 1 ∧ ∀ (P : Matrix (Fin N) (Fin N) ℝ), IsStarProjection P → OP.p P = (ρ * P).trace

★★ Gleason's conclusion over ℝ from the quadratic-form hypothesis.

theorem Gleason.RealProjectionPackage.real_gleason_representation {N : ℕ} (OP : RealProjectionPackage N) (hN : 3 ≤ N) : ∃! ρ : Matrix (Fin N) (Fin N) ℝ, ρ.PosSemidef ∧ ρ.trace = 1 ∧ ∀ (P : Matrix (Fin N) (Fin N) ℝ), IsStarProjection P → OP.p P = (ρ * P).trace

★★★ Gleason's theorem for real Hilbert spaces, N ≥ 3. Every real projection package is P ↦ Tr(ρ P) for a unique real density matrix ρ. The reduction to the core lemma is the three-vector argument: any two vectors lie in a plane, every plane sits inside an orthonormal triple, and the frame function restricted to the span of a triple is a frame function on ℝ³ (isFrameFunction_restrictR), where the core lemma of #57 applies.