Gleason's theorem, finite-dimensional: the complex reduction (Layer A3)

Category: 1-Mathlib (CSD-free; staged for upstream). specs/gleason-feasibility.md, Layer A3: a frame function on ℂᴺ that is a quadratic form on every completely real plane is the quadratic form of a Hermitian matrix. This is Gleason's §3 reduction of the complex case to the real one, done without spherical harmonics.

For a projection package OP with frame function f = OP.frame:

• IsRealPlaneRegular f — for every complex-orthonormal pair (x, y) and real unit (α, β), f (α x + β y) = f x α² + f y β² + 2 α β · crossTerm f x y, where crossTerm f x y = f ((x + y)/√2) − (f x + f y)/2 (the off-diagonal entry of the 2 × 2 form; this is what "quadratic on the completely real plane span_ℝ {x, y}" means once the diagonal is pinned by f x and f y);
• ProjectionPackage.frame_add_frame_eq — two orthonormal pairs spanning the same complex plane have the same weight (additivity, through a matrix identity);
• ProjectionPackage.crossTerm_phase — the key computation: on the "equator" pair w = (x + y)/√2, w' = i(x − y)/√2 regularity forces crossTerm f x (e • y) = β₁ Re e + β₂ Im e for every unit phase e, so the phase dependence of the cross term is a first-degree trigonometric polynomial;
• ProjectionPackage.frame_plane_unit, ProjectionPackage.ext_plane — hence on the complex plane span_ℂ {x, y} the frame function is a Hermitian form: f (a x + b y) = f x |a|² + f y |b|² + 2 Re (conj a · b · S);
• ProjectionPackage.isQuadraticLike_ext — the degree-2 extension ext f v = ‖v‖² f (v/‖v‖) satisfies the parallelogram law on all of ℂᴺ (any two vectors lie in a complex plane), so the Jordan–von Neumann engine (Gleason/Polarization.lean) applies;
• ★ ProjectionPackage.exists_isHermitian_of_isRealPlaneRegular — A3: a Hermitian A with f v = Re ⟪v, A v⟫ on the unit sphere;
• ProjectionPackage.isRealPlaneRegular_of_triples — the bridge from what Gleason's core lemma delivers through A2 (a symmetric 3 × 3 form on every completely real 3-space, N ≥ 3) to the plane hypothesis.

With Gleason/Descent.lean this reduces Gleason's theorem for ℂᴺ, N ≥ 3, to the core lemma on the real sphere S² (specs/gleason-feasibility.md, Layer B).

Source

Gleason 1957, J. Math. Mech. 6, 885, §3 (the completely real subspaces); the equator computation is the one Gleason makes for Lemma 3.3 read through Bloch coordinates.

noncomputable def Gleason.invSqrtTwo : ℂ

The real scalar 1/√2, as a complex number.

Equations

• Gleason.invSqrtTwo = ↑(√2)⁻¹

@[simp]

theorem Gleason.invSqrtTwo_re : invSqrtTwo.re = (√2)⁻¹

@[simp]

theorem Gleason.invSqrtTwo_im : invSqrtTwo.im = 0

@[simp]

theorem Gleason.conj_invSqrtTwo : (starRingEnd ℂ) invSqrtTwo = invSqrtTwo

theorem Gleason.invSqrtTwo_mul_self : invSqrtTwo * invSqrtTwo = 1 / 2

theorem Gleason.norm_invSqrtTwo : ‖invSqrtTwo‖ = (√2)⁻¹

Regularity on completely real planes

noncomputable def Gleason.crossTerm {N : ℕ} (f : EuclideanSpace ℂ (Fin N) → ℝ) (x y : EuclideanSpace ℂ (Fin N)) : ℝ

The off-diagonal entry of the 2 × 2 form of f on the completely real plane of an orthonormal pair: crossTerm f x y = f ((x + y)/√2) − (f x + f y)/2.

Equations

• Gleason.crossTerm f x y = f (Gleason.invSqrtTwo • (x + y)) - (f x + f y) / 2

def Gleason.IsRealPlaneRegular {N : ℕ} (f : EuclideanSpace ℂ (Fin N) → ℝ) : Prop

Regularity on completely real planes: for every complex-orthonormal pair and real unit (α, β), f (α x + β y) = f x α² + f y β² + 2 α β · crossTerm f x y.

Equations

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

Orthonormal pairs

theorem Gleason.norm_eq_one_of_inner_self {N : ℕ} {v : EuclideanSpace ℂ (Fin N)} (h : inner ℂ v v = 1) : ‖v‖ = 1

A vector with ⟪v, v⟫ = 1 is a unit vector.

theorem Gleason.orthonormal_pair_iff {N : ℕ} {x y : EuclideanSpace ℂ (Fin N)} : Orthonormal ℂ ![x, y] ↔ ‖x‖ = 1 ∧ ‖y‖ = 1 ∧ inner ℂ x y = 0

An orthonormal pair, unpacked.

theorem Gleason.orthonormal_pair_smul {N : ℕ} {x y : EuclideanSpace ℂ (Fin N)} (h : Orthonormal ℂ ![x, y]) {e : ℂ} (he : ‖e‖ = 1) : Orthonormal ℂ ![x, e • y]

Rotating the second vector of an orthonormal pair by a phase keeps it orthonormal.

theorem Gleason.orthonormal_equator {N : ℕ} {x y : EuclideanSpace ℂ (Fin N)} (h : Orthonormal ℂ ![x, y]) : Orthonormal ℂ ![invSqrtTwo • (x + y), invSqrtTwo • Complex.I • (x - y)]

The "equator" pair w = (x + y)/√2, w' = i (x − y)/√2 of an orthonormal pair.

The weight of a complex plane is basis independent

theorem Gleason.rankOne_add_add_rankOne_sub {N : ℕ} (u v : EuclideanSpace ℂ (Fin N)) : rankOne (u + v) + rankOne (u - v) = 2 • rankOne u + 2 • rankOne v

The parallelogram identity for rank-one projectors: |u+v⟩⟨u+v| + |u−v⟩⟨u−v| = 2 |u⟩⟨u| + 2 |v⟩⟨v|.

theorem Gleason.rankOne_real_smul {N : ℕ} (r : ℝ) (v : EuclideanSpace ℂ (Fin N)) : rankOne (↑r • v) = ↑(r ^ 2) • rankOne v

Real scaling of a rank-one projector: |r v⟩⟨r v| = r² |v⟩⟨v|.

theorem Gleason.rankOne_equator {N : ℕ} (x y : EuclideanSpace ℂ (Fin N)) : rankOne (invSqrtTwo • (x + y)) + rankOne (invSqrtTwo • Complex.I • (x - y)) = rankOne x + rankOne y

The equator pair spans the same projector as (x, y): |w⟩⟨w| + |w'⟩⟨w'| = |x⟩⟨x| + |y⟩⟨y|.

theorem Gleason.ProjectionPackage.p_rankOne_add_rankOne {N : ℕ} (OP : ProjectionPackage N) {x y : EuclideanSpace ℂ (Fin N)} (h : Orthonormal ℂ ![x, y]) : OP.p (rankOne x + rankOne y) = OP.frame x + OP.frame y

p (|x⟩⟨x| + |y⟩⟨y|) = f x + f y for an orthonormal pair.

theorem Gleason.ProjectionPackage.frame_add_frame_eq {N : ℕ} (OP : ProjectionPackage N) {x y w w' : EuclideanSpace ℂ (Fin N)} (hxy : Orthonormal ℂ ![x, y]) (hww : Orthonormal ℂ ![w, w']) (h : rankOne w + rankOne w' = rankOne x + rankOne y) : OP.frame w + OP.frame w' = OP.frame x + OP.frame y

Two orthonormal pairs with the same projector have the same weight.

The phase dependence of the cross term

theorem Gleason.ProjectionPackage.exists_sq_eq_of_norm_one {e : ℂ} (he : ‖e‖ = 1) : ∃ (z : ℂ), ‖z‖ = 1 ∧ z ^ 2 = e

A unit complex number has a unit square root.

theorem Gleason.ProjectionPackage.equator_combination {N : ℕ} (x y : EuclideanSpace ℂ (Fin N)) {z : ℂ} (hz : ‖z‖ = 1) : ↑z.re • invSqrtTwo • (x + y) + ↑z.im • invSqrtTwo • Complex.I • (x - y) = z • invSqrtTwo • (x + (starRingEnd ℂ) z ^ 2 • y)

The vector identity behind the equator computation: for z = α + iβ of modulus one and e = conj z ^ 2, α w + β w' = z • ((x + e y)/√2).

theorem Gleason.ProjectionPackage.crossTerm_phase {N : ℕ} (OP : ProjectionPackage N) (hreg : IsRealPlaneRegular OP.frame) {x y : EuclideanSpace ℂ (Fin N)} (hxy : Orthonormal ℂ ![x, y]) {e : ℂ} (he : ‖e‖ = 1) : crossTerm OP.frame x (e • y) = (OP.frame (invSqrtTwo • (x + y)) - OP.frame (invSqrtTwo • Complex.I • (x - y))) / 2 * e.re - crossTerm OP.frame (invSqrtTwo • (x + y)) (invSqrtTwo • Complex.I • (x - y)) * e.im

The cross term is a first-degree trigonometric polynomial in the phase: for a unit e, crossTerm f x (e • y) = β₁ Re e + β₂ Im e with β₁ = (f w − f w')/2, β₂ = − crossTerm f w w' for the equator pair (w, w').

The frame function on a complex plane is a Hermitian form

noncomputable def Gleason.ProjectionPackage.planeCoeff {N : ℕ} (OP : ProjectionPackage N) (x y : EuclideanSpace ℂ (Fin N)) : ℂ

The off-diagonal coefficient of the Hermitian form on the plane of (x, y).

Equations

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

theorem Gleason.ProjectionPackage.frame_plane_unit {N : ℕ} (OP : ProjectionPackage N) (hreg : IsRealPlaneRegular OP.frame) {x y : EuclideanSpace ℂ (Fin N)} (hxy : Orthonormal ℂ ![x, y]) {a b : ℂ} (hab : ‖a‖ ^ 2 + ‖b‖ ^ 2 = 1) : OP.frame (a • x + b • y) = OP.frame x * ‖a‖ ^ 2 + OP.frame y * ‖b‖ ^ 2 + 2 * ((starRingEnd ℂ) a * b * OP.planeCoeff x y).re

The frame function on the unit circle of a complex plane: for |a|² + |b|² = 1, f (a x + b y) = f x |a|² + f y |b|² + 2 Re (conj a · b · S).

The degree-2 extension and the parallelogram law on ℂᴺ

noncomputable def Gleason.ProjectionPackage.ext {N : ℕ} (OP : ProjectionPackage N) (v : EuclideanSpace ℂ (Fin N)) : ℝ

The degree-2 extension of the frame function off the unit sphere: ext v = ‖v‖² f (v/‖v‖), with ext 0 = 0.

Equations

• OP.ext v = ‖v‖ ^ 2 * OP.frame (↑‖v‖⁻¹ • v)

theorem Gleason.ProjectionPackage.ext_of_norm_one {N : ℕ} (OP : ProjectionPackage N) {v : EuclideanSpace ℂ (Fin N)} (hv : ‖v‖ = 1) : OP.ext v = OP.frame v

@[simp]

theorem Gleason.ProjectionPackage.ext_zero {N : ℕ} (OP : ProjectionPackage N) : OP.ext 0 = 0

theorem Gleason.ProjectionPackage.norm_inv_smul_self {N : ℕ} {v : EuclideanSpace ℂ (Fin N)} (hv : v ≠ 0) : ‖↑‖v‖⁻¹ • v‖ = 1

The normalisation of a nonzero vector is a unit vector.

theorem Gleason.ProjectionPackage.ext_smul {N : ℕ} (OP : ProjectionPackage N) (c : ℂ) (v : EuclideanSpace ℂ (Fin N)) : OP.ext (c • v) = ‖c‖ ^ 2 * OP.ext v

Degree-2 homogeneity of the extension under complex scaling.

theorem Gleason.ProjectionPackage.ext_nonneg {N : ℕ} (OP : ProjectionPackage N) (v : EuclideanSpace ℂ (Fin N)) : 0 ≤ OP.ext v

theorem Gleason.ProjectionPackage.ext_le_normSq {N : ℕ} (OP : ProjectionPackage N) (v : EuclideanSpace ℂ (Fin N)) : OP.ext v ≤ ‖v‖ ^ 2

theorem Gleason.ProjectionPackage.norm_sq_smul_add_smul {N : ℕ} {x y : EuclideanSpace ℂ (Fin N)} (hxy : Orthonormal ℂ ![x, y]) (a b : ℂ) : ‖a • x + b • y‖ ^ 2 = ‖a‖ ^ 2 + ‖b‖ ^ 2

‖a x + b y‖² = |a|² + |b|² for an orthonormal pair.

theorem Gleason.ProjectionPackage.ext_plane {N : ℕ} (OP : ProjectionPackage N) (hreg : IsRealPlaneRegular OP.frame) {x y : EuclideanSpace ℂ (Fin N)} (hxy : Orthonormal ℂ ![x, y]) (a b : ℂ) : OP.ext (a • x + b • y) = OP.frame x * ‖a‖ ^ 2 + OP.frame y * ‖b‖ ^ 2 + 2 * ((starRingEnd ℂ) a * b * OP.planeCoeff x y).re

The extension on a complex plane is a Hermitian form: for an orthonormal pair (x, y) and all a b : ℂ, ext (a x + b y) = f x |a|² + f y |b|² + 2 Re (conj a · b · S).

theorem Gleason.ProjectionPackage.ext_parallelogram_plane {N : ℕ} (OP : ProjectionPackage N) (hreg : IsRealPlaneRegular OP.frame) {x y : EuclideanSpace ℂ (Fin N)} (hxy : Orthonormal ℂ ![x, y]) (a b a' b' : ℂ) : OP.ext ((a + a') • x + (b + b') • y) + OP.ext ((a - a') • x + (b - b') • y) = 2 * OP.ext (a • x + b • y) + 2 * OP.ext (a' • x + b' • y)

The parallelogram law on a complex plane.

theorem Gleason.ProjectionPackage.ext_parallelogram {N : ℕ} (OP : ProjectionPackage N) (hreg : IsRealPlaneRegular OP.frame) (u v : EuclideanSpace ℂ (Fin N)) : OP.ext (u + v) + OP.ext (u - v) = 2 * OP.ext u + 2 * OP.ext v

The parallelogram law on ℂᴺ. For linearly independent vectors, Gram–Schmidt reduces to an orthonormal pair, where ext is a Hermitian form. Zero vectors and linearly dependent pairs are handled by homogeneity.

theorem Gleason.ProjectionPackage.isQuadraticLike_ext {N : ℕ} (OP : ProjectionPackage N) (hreg : IsRealPlaneRegular OP.frame) : IsQuadraticLike OP.ext

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

theorem Gleason.ProjectionPackage.exists_isHermitian_of_isRealPlaneRegular {N : ℕ} (OP : ProjectionPackage N) (hreg : IsRealPlaneRegular OP.frame) : ∃ (A : Matrix (Fin N) (Fin N) ℂ), A.IsHermitian ∧ ∀ (v : EuclideanSpace ℂ (Fin N)), ‖v‖ = 1 → OP.frame v = (star v.ofLp ⬝ᵥ A.mulVec v.ofLp).re

★ A3 — the complex reduction. A frame function that is regular on every completely real plane is the quadratic form of a Hermitian matrix on the unit sphere.

From completely real 3-spaces to planes

theorem Gleason.ProjectionPackage.exists_orthonormal_triple {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.ProjectionPackage.realCombination_two {N : ℕ} (e : Fin 3 → EuclideanSpace ℂ (Fin N)) (α β : ℝ) : realCombination e !₂[α, β, 0] = ↑α • e 0 + ↑β • e 1

The real vector (α, β, 0) of ℝ³, transported.

theorem Gleason.ProjectionPackage.isRealPlaneRegular_of_triples {N : ℕ} (OP : ProjectionPackage N) (hN : 3 ≤ N) (h : ∀ (e : Fin 3 → EuclideanSpace ℂ (Fin N)), Orthonormal ℂ e → ∃ (A : Matrix (Fin 3) (Fin 3) ℝ), A.IsSymm ∧ ∀ (x : EuclideanSpace ℝ (Fin 3)), ‖x‖ = 1 → OP.realRestrict e x = x.ofLp ⬝ᵥ A.mulVec x.ofLp) : IsRealPlaneRegular OP.frame

The bridge from Gleason's core lemma to the plane hypothesis. If, for every complex-orthonormal triple e, the restriction of the frame function to the completely real 3-space of e is a symmetric quadratic form on the sphere of ℝ³, then the frame function is regular on every completely real plane (N ≥ 3).