Gleason's theorem, finite-dimensional: the core lemma — every nonnegative frame function on

S² is a quadratic form

Category: 1-Mathlib (CSD-free; staged for upstream). specs/gleason-feasibility.md, stage 57(e): Cooke–Keane–Moran §7, the general case, and with it Gleason's core lemma ★★ frameFunction_regular_sphere.

The argument. Let f be a frame function on S² ⊂ ℝ³, nonnegative (hence bounded by its weight W). By stage (d) it attains its supremum M at some p; a minimiser of f + ⟪p, ·⟫² is a point r ⟂ p where f attains its infimum m. With q = r × p this is a frame; put α = f q, so M + α + m = W, and let g s = M ⟪p,s⟫² + α ⟪q,s⟫² + m ⟪r,s⟫² — the quadratic form f ought to be.

• The pole identities. f + f ∘ rot p attains its supremum 2M at p and is constant on the equator of p, so the simple-frame-function theorem (stage (c)) gives f s + f (rot p s) = (W − M) + (3M − W)⟪p,s⟫² (IsFrameFunction.add_rot_of_forall_le); likewise at the minimum r, applied to −f (add_rot_of_forall_ge). The quadratic form g satisfies the same two identities (a computation in the frame, quadFrame_add_rot_p, quadFrame_add_rot_r), so h = g − f satisfies h (rot p s) = −h s, h (rot r s) = −h s and h (−s) = h s.
• The symmetries. Since rot p ∘ rot p is the half-turn about p, the reflection in each coordinate plane preserves h (flip_p, flip_q, flip_r); composing with rot p and rot r, the reflections in the planes x = ±y and y = ±z negate h, so h vanishes on those four great circles (vanish_p_eq_q, …).
• The endgame (this replaces the paper's count of zeros on great circles). If h ≠ 0, its supremum M' > 0 is attained at some p' (stage (d)) and the pole identity for h reads h s + h (rot p' s) = M'(3⟪p',s⟫² − 1). On a great circle with unit normal n on which h vanishes there is a point t with rot p' t on the same circle, hence ⟪p',t⟫² = 1/3, and the geometry of t forces ⟪p', n⟫² = 1/2 (inner_sq_eq_half_of_vanish). For the four normals (p ± q)/√2, (q ± r)/√2 this gives ⟪p',p⟫² + ⟪p',q⟫² = 1 = ⟪p',q⟫² + ⟪p',r⟫², so with Parseval p' = ±q; but h q = α − α = 0, contradicting M' > 0. Hence f = g.

With Gleason/Reduction.lean this proves the finite-dimensional Gleason theorem (Gleason/Core.lean).

Source

Cooke, Keane, Moran 1985, Math. Proc. Cambridge Philos. Soc. 98, 117–128, §7 (the choice of p, r, q, the target form, the identities (*) and the Claim); the endgame is different from the paper's.

Cross-product algebra

theorem Gleason.ext_coe {x y : EuclideanSpace ℝ (Fin 3)} (h : x.ofLp = y.ofLp) : x = y

theorem Gleason.inner_cross_perm (u v w : EuclideanSpace ℝ (Fin 3)) : inner ℝ u (cross v w) = inner ℝ w (cross u v)

The cyclic symmetry of the scalar triple product: ⟪u, v × w⟫ = ⟪w, u × v⟫.

theorem Gleason.cross_eq_neg_cross (x y : EuclideanSpace ℝ (Fin 3)) : cross x y = -cross y x

theorem Gleason.cross_cross_left (u v w : EuclideanSpace ℝ (Fin 3)) : cross (cross u v) w = inner ℝ u w • v - inner ℝ v w • u

The vector triple product (u × v) × w = ⟪u,w⟫ v − ⟪v,w⟫ u.

A frame (p, q, r) with q = r × p, and its table

structure Gleason.Frame (p q r : EuclideanSpace ℝ (Fin 3)) : Prop

A right-handed frame: p, r orthonormal and q = r × p.

• hp : ‖p‖ = 1

  ‖p‖ = 1.

• hr : ‖r‖ = 1

  ‖r‖ = 1.

• hpr : inner ℝ p r = 0

  p ⟂ r.

• hq : q = cross r p

  q = r × p.

theorem Gleason.Frame.hrp {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) : inner ℝ r p = 0

theorem Gleason.Frame.hq1 {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) : ‖q‖ = 1

theorem Gleason.Frame.hpq {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) : inner ℝ p q = 0

theorem Gleason.Frame.hqr {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) : inner ℝ q r = 0

theorem Gleason.Frame.hqp {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) : inner ℝ q p = 0

theorem Gleason.Frame.hrq {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) : inner ℝ r q = 0

theorem Gleason.Frame.hpp {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) : inner ℝ p p = 1

theorem Gleason.Frame.hqq {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) : inner ℝ q q = 1

theorem Gleason.Frame.hrr {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) : inner ℝ r r = 1

theorem Gleason.Frame.orthonormal {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) : Orthonormal ℝ ![p, q, r]

theorem Gleason.Frame.cross_q_p {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) : cross q p = -r

The table: q × p = −r.

theorem Gleason.Frame.cross_q_r {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) : cross q r = p

theorem Gleason.Frame.cross_p_r {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) : cross p r = -q

theorem Gleason.Frame.expand {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) (s : EuclideanSpace ℝ (Fin 3)) : s = inner ℝ p s • p + inner ℝ q s • q + inner ℝ r s • r

The expansion s = ⟪p,s⟫ p + ⟪q,s⟫ q + ⟪r,s⟫ r.

theorem Gleason.Frame.eq_of_inner {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) {a b : EuclideanSpace ℝ (Fin 3)} (h1 : inner ℝ p a = inner ℝ p b) (h2 : inner ℝ q a = inner ℝ q b) (h3 : inner ℝ r a = inner ℝ r b) : a = b

Two vectors with the same frame coordinates are equal.

theorem Gleason.Frame.sum_sq {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) (s : EuclideanSpace ℝ (Fin 3)) : inner ℝ p s ^ 2 + inner ℝ q s ^ 2 + inner ℝ r s ^ 2 = ‖s‖ ^ 2

Parseval: ⟪p,s⟫² + ⟪q,s⟫² + ⟪r,s⟫² = ‖s‖².

theorem Gleason.Frame.inner_p_rot_p {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) (s : EuclideanSpace ℝ (Fin 3)) : inner ℝ p (rot p s) = inner ℝ p s

The rotation about p in frame coordinates: (x, y, z) ↦ (x, −z, y).

theorem Gleason.Frame.inner_q_rot_p {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) (s : EuclideanSpace ℝ (Fin 3)) : inner ℝ q (rot p s) = -inner ℝ r s

theorem Gleason.Frame.inner_r_rot_p {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) (s : EuclideanSpace ℝ (Fin 3)) : inner ℝ r (rot p s) = inner ℝ q s

theorem Gleason.Frame.inner_p_rot_r {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) (s : EuclideanSpace ℝ (Fin 3)) : inner ℝ p (rot r s) = -inner ℝ q s

The rotation about r in frame coordinates: (x, y, z) ↦ (−y, x, z).

theorem Gleason.Frame.inner_q_rot_r {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) (s : EuclideanSpace ℝ (Fin 3)) : inner ℝ q (rot r s) = inner ℝ p s

theorem Gleason.Frame.inner_r_rot_r {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) (s : EuclideanSpace ℝ (Fin 3)) : inner ℝ r (rot r s) = inner ℝ r s

The inverse rotation, as an adjoint

noncomputable def Gleason.rotInv (p n : EuclideanSpace ℝ (Fin 3)) : EuclideanSpace ℝ (Fin 3)

The rotation by −90° about p: n ↦ ⟪p, n⟫ p − p × n.

Equations

• Gleason.rotInv p n = inner ℝ p n • p - Gleason.cross p n

theorem Gleason.inner_rot_eq_inner_rotInv (p n s : EuclideanSpace ℝ (Fin 3)) : inner ℝ n (rot p s) = inner ℝ (rotInv p n) s

⟪n, rot p s⟫ = ⟪rotInv p n, s⟫.

theorem Gleason.norm_rotInv {p n : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) (hn : ‖n‖ = 1) : ‖rotInv p n‖ = 1

The pole identities

theorem Gleason.IsFrameFunction.add_rot_of_forall_le {f : EuclideanSpace ℝ (Fin 3) → ℝ} {W : ℝ} {p : EuclideanSpace ℝ (Fin 3)} (hf : IsFrameFunction ℝ f W) (hp : ‖p‖ = 1) (hM : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f u ≤ f p) (s : EuclideanSpace ℝ (Fin 3)) : ‖s‖ = 1 → f s + f (rot p s) = W - f p + (3 * f p - W) * latitude p s

The pole identity at a maximum. If f attains its supremum at p, then f s + f (rot p s) = (W − f p) + (3 f p − W) ⟪p, s⟫² for every unit s.

theorem Gleason.IsFrameFunction.add_rot_of_forall_ge {f : EuclideanSpace ℝ (Fin 3) → ℝ} {W : ℝ} (hf : IsFrameFunction ℝ f W) {r : EuclideanSpace ℝ (Fin 3)} (hr : ‖r‖ = 1) (hm : ∀ (u : EuclideanSpace ℝ (Fin 3)), ‖u‖ = 1 → f r ≤ f u) (s : EuclideanSpace ℝ (Fin 3)) : ‖s‖ = 1 → f s + f (rot r s) = W - f r - (W - 3 * f r) * latitude r s

The pole identity at a minimum. If f attains its infimum at r, then f s + f (rot r s) = (W − f r) − (W − 3 f r) ⟪r, s⟫² for every unit s.

The target quadratic form

noncomputable def Gleason.quadFrame (M α m : ℝ) (p q r s : EuclideanSpace ℝ (Fin 3)) : ℝ

The quadratic form M ⟪p,s⟫² + α ⟪q,s⟫² + m ⟪r,s⟫².

Equations

• Gleason.quadFrame M α m p q r s = M * inner ℝ p s ^ 2 + α * inner ℝ q s ^ 2 + m * inner ℝ r s ^ 2

theorem Gleason.isFrameFunction_quadFrame {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) {M α m : ℝ} : IsFrameFunction ℝ (quadFrame M α m p q r) (M + α + m)

theorem Gleason.quadFrame_neg {p q r : EuclideanSpace ℝ (Fin 3)} {M α m : ℝ} (s : EuclideanSpace ℝ (Fin 3)) : quadFrame M α m p q r (-s) = quadFrame M α m p q r s

theorem Gleason.quadFrame_add_rot_p {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) {M α m : ℝ} (s : EuclideanSpace ℝ (Fin 3)) (hs : ‖s‖ = 1) : quadFrame M α m p q r s + quadFrame M α m p q r (rot p s) = α + m + (2 * M - (α + m)) * latitude p s

The pole identity for the quadratic form at p.

theorem Gleason.quadFrame_add_rot_r {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) {M α m : ℝ} (s : EuclideanSpace ℝ (Fin 3)) (hs : ‖s‖ = 1) : quadFrame M α m p q r s + quadFrame M α m p q r (rot r s) = M + α - (M + α - 2 * m) * latitude r s

The pole identity for the quadratic form at r.

theorem Gleason.quadFrame_nonneg {p q r : EuclideanSpace ℝ (Fin 3)} {M α m : ℝ} (hM : 0 ≤ M) (hα : 0 ≤ α) (hm : 0 ≤ m) (s : EuclideanSpace ℝ (Fin 3)) : 0 ≤ quadFrame M α m p q r s

theorem Gleason.quadFrame_le {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) {M α m W : ℝ} (hM : M ≤ W) (hα : α ≤ W) (hm : m ≤ W) (s : EuclideanSpace ℝ (Fin 3)) (hs : ‖s‖ = 1) : quadFrame M α m p q r s ≤ W

theorem Gleason.quadFrame_eq_dotProduct {p q r : EuclideanSpace ℝ (Fin 3)} {M α m : ℝ} (s : EuclideanSpace ℝ (Fin 3)) : quadFrame M α m p q r s = s.ofLp ⬝ᵥ (M • Matrix.vecMulVec p.ofLp p.ofLp + α • Matrix.vecMulVec q.ofLp q.ofLp + m • Matrix.vecMulVec r.ofLp r.ofLp).mulVec s.ofLp

The quadratic form as a matrix: s ⬝ A s with A = M p pᵀ + α q qᵀ + m r rᵀ.

The circle lemma

theorem Gleason.inner_sq_eq_half_of_vanish {h : EuclideanSpace ℝ (Fin 3) → ℝ} {p' n : EuclideanSpace ℝ (Fin 3)} {M' : ℝ} (hp' : ‖p'‖ = 1) (hM' : M' ≠ 0) (hid : ∀ (s : EuclideanSpace ℝ (Fin 3)), ‖s‖ = 1 → h s + h (rot p' s) = M' * (3 * inner ℝ p' s ^ 2 - 1)) (hn : ‖n‖ = 1) (hz : ∀ (s : EuclideanSpace ℝ (Fin 3)), ‖s‖ = 1 → inner ℝ n s = 0 → h s = 0) : inner ℝ p' n ^ 2 = 1 / 2

A great circle of zeros sits at latitude 1/2 from the pole of the identity. If h s + h (rot p' s) = M'(3⟪p',s⟫² − 1) on the sphere with M' ≠ 0, and h vanishes on the great circle with unit normal n, then ⟪p', n⟫² = 1/2.

The reflections, and the four circles of zeros

noncomputable def Gleason.reflect (a s : EuclideanSpace ℝ (Fin 3)) : EuclideanSpace ℝ (Fin 3)

For unit a, the reflection in the plane orthogonal to a.

Equations

• Gleason.reflect a s = s - (2 * inner ℝ a s) • a

theorem Gleason.rot_rot_p {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) (s : EuclideanSpace ℝ (Fin 3)) : rot p (rot p s) = (2 * inner ℝ p s) • p - s

The half-turn about p: rot p (rot p s) = 2⟪p,s⟫ p − s.

theorem Gleason.rot_rot_r {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) (s : EuclideanSpace ℝ (Fin 3)) : rot r (rot r s) = (2 * inner ℝ r s) • r - s

theorem Gleason.flip_p {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) {h : EuclideanSpace ℝ (Fin 3) → ℝ} (heven : ∀ (s : EuclideanSpace ℝ (Fin 3)), ‖s‖ = 1 → h (-s) = h s) (hrotp : ∀ (s : EuclideanSpace ℝ (Fin 3)), ‖s‖ = 1 → h (rot p s) = -h s) (s : EuclideanSpace ℝ (Fin 3)) (hs : ‖s‖ = 1) : h (reflect p s) = h s

The reflection in p^⊥ preserves h.

theorem Gleason.flip_r {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) {h : EuclideanSpace ℝ (Fin 3) → ℝ} (heven : ∀ (s : EuclideanSpace ℝ (Fin 3)), ‖s‖ = 1 → h (-s) = h s) (hrotr : ∀ (s : EuclideanSpace ℝ (Fin 3)), ‖s‖ = 1 → h (rot r s) = -h s) (s : EuclideanSpace ℝ (Fin 3)) (hs : ‖s‖ = 1) : h (reflect r s) = h s

The reflection in r^⊥ preserves h.

theorem Gleason.flip_q {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) {h : EuclideanSpace ℝ (Fin 3) → ℝ} (heven : ∀ (s : EuclideanSpace ℝ (Fin 3)), ‖s‖ = 1 → h (-s) = h s) (hrotp : ∀ (s : EuclideanSpace ℝ (Fin 3)), ‖s‖ = 1 → h (rot p s) = -h s) (hrotr : ∀ (s : EuclideanSpace ℝ (Fin 3)), ‖s‖ = 1 → h (rot r s) = -h s) (s : EuclideanSpace ℝ (Fin 3)) (hs : ‖s‖ = 1) : h (reflect q s) = h s

The reflection in q^⊥ preserves h: it is the reflection in r^⊥ composed with the half-turn about p.

theorem Gleason.vanish_p_eq_q {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) {h : EuclideanSpace ℝ (Fin 3) → ℝ} (heven : ∀ (s : EuclideanSpace ℝ (Fin 3)), ‖s‖ = 1 → h (-s) = h s) (hrotp : ∀ (s : EuclideanSpace ℝ (Fin 3)), ‖s‖ = 1 → h (rot p s) = -h s) (hrotr : ∀ (s : EuclideanSpace ℝ (Fin 3)), ‖s‖ = 1 → h (rot r s) = -h s) (s : EuclideanSpace ℝ (Fin 3)) (hs : ‖s‖ = 1) (hpq : inner ℝ p s = inner ℝ q s) : h s = 0

h vanishes on the great circle ⟪p, s⟫ = ⟪q, s⟫.

theorem Gleason.vanish_p_eq_neg_q {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) {h : EuclideanSpace ℝ (Fin 3) → ℝ} (heven : ∀ (s : EuclideanSpace ℝ (Fin 3)), ‖s‖ = 1 → h (-s) = h s) (hrotp : ∀ (s : EuclideanSpace ℝ (Fin 3)), ‖s‖ = 1 → h (rot p s) = -h s) (hrotr : ∀ (s : EuclideanSpace ℝ (Fin 3)), ‖s‖ = 1 → h (rot r s) = -h s) (s : EuclideanSpace ℝ (Fin 3)) (hs : ‖s‖ = 1) (hpq : inner ℝ p s = -inner ℝ q s) : h s = 0

h vanishes on the great circle ⟪p, s⟫ = −⟪q, s⟫.

theorem Gleason.vanish_q_eq_r {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) {h : EuclideanSpace ℝ (Fin 3) → ℝ} (heven : ∀ (s : EuclideanSpace ℝ (Fin 3)), ‖s‖ = 1 → h (-s) = h s) (hrotp : ∀ (s : EuclideanSpace ℝ (Fin 3)), ‖s‖ = 1 → h (rot p s) = -h s) (hrotr : ∀ (s : EuclideanSpace ℝ (Fin 3)), ‖s‖ = 1 → h (rot r s) = -h s) (s : EuclideanSpace ℝ (Fin 3)) (hs : ‖s‖ = 1) (hqr : inner ℝ q s = inner ℝ r s) : h s = 0

h vanishes on the great circle ⟪q, s⟫ = ⟪r, s⟫.

theorem Gleason.vanish_q_eq_neg_r {p q r : EuclideanSpace ℝ (Fin 3)} (F : Frame p q r) {h : EuclideanSpace ℝ (Fin 3) → ℝ} (heven : ∀ (s : EuclideanSpace ℝ (Fin 3)), ‖s‖ = 1 → h (-s) = h s) (hrotp : ∀ (s : EuclideanSpace ℝ (Fin 3)), ‖s‖ = 1 → h (rot p s) = -h s) (hrotr : ∀ (s : EuclideanSpace ℝ (Fin 3)), ‖s‖ = 1 → h (rot r s) = -h s) (s : EuclideanSpace ℝ (Fin 3)) (hs : ‖s‖ = 1) (hqr : inner ℝ q s = -inner ℝ r s) : h s = 0

h vanishes on the great circle ⟪q, s⟫ = −⟪r, s⟫.

The core lemma

theorem Gleason.frameFunction_regular_sphere (f : EuclideanSpace ℝ (Fin 3) → ℝ) {W : ℝ} (hf : IsFrameFunction ℝ f W) (h0 : ∀ (x : EuclideanSpace ℝ (Fin 3)), ‖x‖ = 1 → 0 ≤ f x) : ∃ (A : Matrix (Fin 3) (Fin 3) ℝ), A.IsSymm ∧ ∀ (x : EuclideanSpace ℝ (Fin 3)), ‖x‖ = 1 → f x = x.ofLp ⬝ᵥ A.mulVec x.ofLp

★★ Gleason's core lemma (CKM, the Theorem of §3). Every nonnegative frame function on the unit sphere of ℝ³ is the restriction of a symmetric quadratic form.