Gleason's theorem, finite-dimensional: latitudes, descents and Piron's geometric lemma

Category: 1-Mathlib (CSD-free; staged for upstream). specs/gleason-feasibility.md, stage 57(b): Cooke–Keane–Moran §4 (the vocabulary) and the geometric lemma of §5, due to Piron — the one step of the core lemma with no Mathlib support, and the decision point of the plan.

Fix a unit vector p, the north pole. For s ∈ northern p with s ≠ p:

• latitude p s = ⟪p, s⟫²; northern p is the closed northern hemisphere ⟪p, s⟫ ≥ 0, equator p its boundary;
• coldest p s is the unit vector orthogonal to s in the plane of p and s with latitude p (coldest p s) = 1 − latitude p s — the coldest vector orthogonal to s;
• descent p s = {t ∈ northern p : t ⟂ coldest p s} is the intersection of that great circle with the northern hemisphere (CKM's D_s). It is the whole equator when s lies on the equator.

The definitions are total: at s = p, coldest p p = 0 and descent p p = northern p.

The gnomonic dictionary. Projecting the open northern hemisphere from the origin onto the tangent plane at p sends s to ⟪p, s⟫⁻¹ s − p; conversely lift p v = (p + v)/‖p + v‖ for v ⟂ p. Latitude circles become circles centred at p, and lift p w ∈ descent p (lift p v) iff ⟪w, v⟫ = ‖v‖² for nonzero tangent v (lift_mem_descent_iff) — the descent through s is the tangent line to its latitude circle. Reading the tangent plane as ℂ through an orthonormal pair e₁, e₂ ⟂ p (tangent e₁ e₂ z = Re z • e₁ + Im z • e₂), the condition is Re (w · conj z) = ‖z‖².

Piron's geometric lemma (exists_descent_chain): if s, t ∈ northern p \ {p} and latitude p t < latitude p s, there is a finite chain s = c 0, c 1, …, c n = t with each c (i+1) ∈ descent p (c i). Proof, in the plane: the explicit spiral zₖ = z₀ (cos θ)⁻ᵏ e^{ikθ} with θ = δ/n turns by the angle δ from z₀ to the ray of ζ while growing by the factor (cos θ)⁻ⁿ, which tends to 1 (cos x ≥ 1 − x²/2 and Bernoulli), so for large n it stops short of ζ on its ray; two more steps along that ray reach ζ (descent_step_ray). A target on the equator is reached from any point orthogonal to it (mem_descent_of_equator), so the spiral is aimed at the direction perpendicular to t.

Source

Cooke, Keane, Moran 1985, Math. Proc. Cambridge Philos. Soc. 98, 117–128, §4 and the Geometric Lemma of §5 (with Figs. 1–3); Piron, Foundations of Quantum Physics (1976).

The pole, latitudes, the coldest vector, descents

noncomputable def Gleason.latitude (p s : EuclideanSpace ℝ (Fin 3)) : ℝ

The latitude of s seen from the pole p: cos² θ(p, s) = ⟪p, s⟫².

Equations

• Gleason.latitude p s = inner ℝ p s ^ 2

def Gleason.northern (p : EuclideanSpace ℝ (Fin 3)) : Set (EuclideanSpace ℝ (Fin 3))

The closed northern hemisphere.

Equations

• Gleason.northern p = {s : EuclideanSpace ℝ (Fin 3) | ‖s‖ = 1 ∧ 0 ≤ inner ℝ p s}

def Gleason.equator (p : EuclideanSpace ℝ (Fin 3)) : Set (EuclideanSpace ℝ (Fin 3))

The equator.

Equations

• Gleason.equator p = {s : EuclideanSpace ℝ (Fin 3) | ‖s‖ = 1 ∧ inner ℝ p s = 0}

noncomputable def Gleason.coldest (p s : EuclideanSpace ℝ (Fin 3)) : EuclideanSpace ℝ (Fin 3)

The normalization of p − ⟪p, s⟫ s. For unit p and s ∈ northern p with s ≠ p, this is a unit vector orthogonal to s. At s = p it is zero.

Equations

• Gleason.coldest p s = ‖p - inner ℝ p s • s‖⁻¹ • (p - inner ℝ p s • s)

def Gleason.descent (p s : EuclideanSpace ℝ (Fin 3)) : Set (EuclideanSpace ℝ (Fin 3))

The northern vectors orthogonal to coldest p s. For unit p and s ∈ northern p with s ≠ p, this is a great-circle intersection with the hemisphere. At an equatorial s it is the whole equator; at the pole it is the whole hemisphere.

Equations

• Gleason.descent p s = {t : EuclideanSpace ℝ (Fin 3) | t ∈ Gleason.northern p ∧ inner ℝ t (Gleason.coldest p s) = 0}

theorem Gleason.equator_subset_northern (p : EuclideanSpace ℝ (Fin 3)) : equator p ⊆ northern p

theorem Gleason.inner_coldest_self (p : EuclideanSpace ℝ (Fin 3)) {s : EuclideanSpace ℝ (Fin 3)} (hs : ‖s‖ = 1) : inner ℝ s (coldest p s) = 0

theorem Gleason.mem_descent_of_equator {p s t : EuclideanSpace ℝ (Fin 3)} (ht : t ∈ equator p) (hts : inner ℝ t s = 0) : t ∈ descent p s

A point of the equator orthogonal to s lies on the descent through s.

theorem Gleason.self_mem_descent {p s : EuclideanSpace ℝ (Fin 3)} (hs : s ∈ northern p) : s ∈ descent p s

Every point is on its own descent.

The gnomonic lift

noncomputable def Gleason.lift (p v : EuclideanSpace ℝ (Fin 3)) : EuclideanSpace ℝ (Fin 3)

The point of the open northern hemisphere over the tangent vector v ⟂ p: (p + v)/‖p + v‖.

Equations

• Gleason.lift p v = ‖p + v‖⁻¹ • (p + v)

theorem Gleason.norm_sq_add_of_inner_zero {p v : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) (hv : inner ℝ p v = 0) : ‖p + v‖ ^ 2 = 1 + ‖v‖ ^ 2

theorem Gleason.norm_add_pos {p v : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) (hv : inner ℝ p v = 0) : 0 < ‖p + v‖

theorem Gleason.norm_lift {p v : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) (hv : inner ℝ p v = 0) : ‖lift p v‖ = 1

theorem Gleason.inner_lift {p v : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) (hv : inner ℝ p v = 0) : inner ℝ p (lift p v) = ‖p + v‖⁻¹

theorem Gleason.inner_lift_pos {p v : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) (hv : inner ℝ p v = 0) : 0 < inner ℝ p (lift p v)

theorem Gleason.lift_mem_northern {p v : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) (hv : inner ℝ p v = 0) : lift p v ∈ northern p

theorem Gleason.lift_ne_pole {p v : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) (hv : inner ℝ p v = 0) (hv0 : v ≠ 0) : lift p v ≠ p

theorem Gleason.latitude_lift {p v : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) (hv : inner ℝ p v = 0) : latitude p (lift p v) = 1 / (1 + ‖v‖ ^ 2)

theorem Gleason.latitude_lift_lt_iff {p v w : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) (hv : inner ℝ p v = 0) (hw : inner ℝ p w = 0) : latitude p (lift p w) < latitude p (lift p v) ↔ ‖v‖ < ‖w‖

Latitudes of lifts compare inversely to the norms of the tangent vectors.

theorem Gleason.eq_lift_of_northern {p : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) {s : EuclideanSpace ℝ (Fin 3)} (hs : ‖s‖ = 1) (hps : 0 < inner ℝ p s) : inner ℝ p ((inner ℝ p s)⁻¹ • s - p) = 0 ∧ s = lift p ((inner ℝ p s)⁻¹ • s - p)

Every point of the open northern hemisphere is the lift of ⟪p, s⟫⁻¹ s − p.

theorem Gleason.lift_mem_descent_iff {p v w : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) (hv : inner ℝ p v = 0) (hw : inner ℝ p w = 0) (hv0 : v ≠ 0) : lift p w ∈ descent p (lift p v) ↔ inner ℝ w v = ‖v‖ ^ 2

The gnomonic dictionary. lift p w lies on the descent through lift p v iff ⟪w, v⟫ = ‖v‖²: the descent is the tangent line to the latitude circle.

The tangent plane as ℂ

noncomputable def Gleason.tangent (e₁ e₂ : EuclideanSpace ℝ (Fin 3)) (z : ℂ) : EuclideanSpace ℝ (Fin 3)

The tangent vector with complex coordinate z in the orthonormal frame (e₁, e₂) of the tangent plane at the pole.

Equations

• Gleason.tangent e₁ e₂ z = z.re • e₁ + z.im • e₂

theorem Gleason.inner_tangent_tangent {p e₁ e₂ : EuclideanSpace ℝ (Fin 3)} (he : Orthonormal ℝ ![p, e₁, e₂]) (z w : ℂ) : inner ℝ (tangent e₁ e₂ z) (tangent e₁ e₂ w) = (z * (starRingEnd ℂ) w).re

theorem Gleason.norm_sq_tangent {p e₁ e₂ : EuclideanSpace ℝ (Fin 3)} (he : Orthonormal ℝ ![p, e₁, e₂]) (z : ℂ) : ‖tangent e₁ e₂ z‖ ^ 2 = ‖z‖ ^ 2

theorem Gleason.norm_tangent {p e₁ e₂ : EuclideanSpace ℝ (Fin 3)} (he : Orthonormal ℝ ![p, e₁, e₂]) (z : ℂ) : ‖tangent e₁ e₂ z‖ = ‖z‖

theorem Gleason.inner_pole_tangent {p e₁ e₂ : EuclideanSpace ℝ (Fin 3)} (he : Orthonormal ℝ ![p, e₁, e₂]) (z : ℂ) : inner ℝ p (tangent e₁ e₂ z) = 0

theorem Gleason.tangent_ne_zero {p e₁ e₂ : EuclideanSpace ℝ (Fin 3)} (he : Orthonormal ℝ ![p, e₁, e₂]) {z : ℂ} (hz : z ≠ 0) : tangent e₁ e₂ z ≠ 0

theorem Gleason.exists_tangent_eq {p e₁ e₂ : EuclideanSpace ℝ (Fin 3)} (he : Orthonormal ℝ ![p, e₁, e₂]) {v : EuclideanSpace ℝ (Fin 3)} (hv : inner ℝ p v = 0) : ∃ (z : ℂ), tangent e₁ e₂ z = v

Every tangent vector has a complex coordinate.

Descent steps in the plane

theorem Gleason.lift_tangent_mem_descent_iff {p e₁ e₂ : EuclideanSpace ℝ (Fin 3)} (he : Orthonormal ℝ ![p, e₁, e₂]) {z w : ℂ} (hz : z ≠ 0) : lift p (tangent e₁ e₂ w) ∈ descent p (lift p (tangent e₁ e₂ z)) ↔ (w * (starRingEnd ℂ) z).re = ‖z‖ ^ 2

The complex form of the gnomonic dictionary: lift (tangent w) ∈ descent (lift (tangent z)) iff Re (w · conj z) = ‖z‖².

theorem Gleason.descent_step_ray (ζ : ℂ) {ρ : ℝ} (hρ0 : 0 < ρ) (hρ1 : ρ ≤ 1) : (↑ρ * ζ * (1 + ↑√(1 / ρ - 1) * Complex.I) * (starRingEnd ℂ) (↑ρ * ζ)).re = ‖↑ρ * ζ‖ ^ 2 ∧ (ζ * (starRingEnd ℂ) (↑ρ * ζ * (1 + ↑√(1 / ρ - 1) * Complex.I))).re = ‖↑ρ * ζ * (1 + ↑√(1 / ρ - 1) * Complex.I)‖ ^ 2

Two steps along a ray: from ρ ζ to ζ (0 < ρ ≤ 1) through ρ ζ (1 + i μ) with μ² = 1/ρ − 1.

The spiral

noncomputable def Gleason.spiral (z₀ : ℂ) (θ : ℝ) (k : ℕ) : ℂ

The spiral zₖ = z₀ (cos θ)⁻ᵏ e^{ikθ}: each point lies on the descent through the previous one (spiral_step), the argument advances by θ and the modulus grows by (cos θ)⁻¹.

Equations

• Gleason.spiral z₀ θ k = z₀ * ↑(Real.cos θ)⁻¹ ^ k * Complex.exp (↑(↑k * θ) * Complex.I)

theorem Gleason.spiral_zero (z₀ : ℂ) (θ : ℝ) : spiral z₀ θ 0 = z₀

theorem Gleason.spiral_ne_zero {z₀ : ℂ} (hz₀ : z₀ ≠ 0) {θ : ℝ} (hcos : 0 < Real.cos θ) (k : ℕ) : spiral z₀ θ k ≠ 0

theorem Gleason.norm_sq_spiral {z₀ : ℂ} {θ : ℝ} (hcos : 0 < Real.cos θ) (k : ℕ) : ‖spiral z₀ θ k‖ ^ 2 = ‖z₀‖ ^ 2 * (Real.cos θ)⁻¹ ^ (2 * k)

theorem Gleason.spiral_succ_mul_conj (z₀ : ℂ) (θ : ℝ) (k : ℕ) : spiral z₀ θ (k + 1) * (starRingEnd ℂ) (spiral z₀ θ k) = ↑(Complex.normSq z₀) * ↑(Real.cos θ)⁻¹ ^ (2 * k + 1) * Complex.exp (↑θ * Complex.I)

The product zₖ₊₁ · conj zₖ = ‖z₀‖² (cos θ)⁻⁽²ᵏ⁺¹⁾ e^{iθ}.

theorem Gleason.spiral_step (z₀ : ℂ) {θ : ℝ} (hcos : 0 < Real.cos θ) (k : ℕ) : (spiral z₀ θ (k + 1) * (starRingEnd ℂ) (spiral z₀ θ k)).re = ‖spiral z₀ θ k‖ ^ 2

Each spiral point lies on the descent through the previous one.

theorem Gleason.spiral_end {z₀ u : ℂ} (hu : ‖u‖ = 1) {n : ℕ} (hn : n ≠ 0) : spiral z₀ (u.arg / ↑n) n = z₀ * ↑(Real.cos (u.arg / ↑n))⁻¹ ^ n * u

The spiral's endpoint when the angle is arg u / n: zₙ = z₀ (cos θ)⁻ⁿ u.

theorem Gleason.cos_arg_div_pos (u : ℂ) {n : ℕ} (hn : 3 ≤ n) : 0 < Real.cos (u.arg / ↑n)

cos θ > 0 for θ = arg u / n, n ≥ 3.

theorem Gleason.one_sub_le_cos_arg_div_pow (u : ℂ) {n : ℕ} (hn : 3 ≤ n) : 1 - Real.pi ^ 2 / (2 * ↑n) ≤ Real.cos (u.arg / ↑n) ^ n

The growth factor tends to one: (cos (arg u / n))ⁿ ≥ 1 − π²/(2n) for n ≥ 3, by cos x ≥ 1 − x²/2 and Bernoulli's inequality.

Piron's geometric lemma

structure Gleason.IsDescentChain (p s t : EuclideanSpace ℝ (Fin 3)) (n : ℕ) (c : ℕ → EuclideanSpace ℝ (Fin 3)) : Prop

A descent chain of length n from s to t in the northern hemisphere minus the pole.

• head : c 0 = s

  The chain starts at s.

• last : c n = t

  The chain ends at t.

• mem (i : ℕ) : i ≤ n → c i ∈ northern p ∧ c i ≠ p

  Every point is in the northern hemisphere and is not the pole.

• step (i : ℕ) : i < n → c (i + 1) ∈ descent p (c i)

  Each point lies on the descent through the previous one.

theorem Gleason.spiral_chain_step {p e₁ e₂ : EuclideanSpace ℝ (Fin 3)} (he : Orthonormal ℝ ![p, e₁, e₂]) {z₀ : ℂ} {θ : ℝ} (hz₀ : z₀ ≠ 0) (hcos : 0 < Real.cos θ) (k : ℕ) : lift p (tangent e₁ e₂ (spiral z₀ θ (k + 1))) ∈ descent p (lift p (tangent e₁ e₂ (spiral z₀ θ k)))

The lifted spiral is a descent chain of its own points.

theorem Gleason.lift_tangent_mem {p e₁ e₂ : EuclideanSpace ℝ (Fin 3)} (he : Orthonormal ℝ ![p, e₁, e₂]) (z : ℂ) (hz : z ≠ 0) : lift p (tangent e₁ e₂ z) ∈ northern p ∧ lift p (tangent e₁ e₂ z) ≠ p

theorem Gleason.exists_descent_chain {p s t : EuclideanSpace ℝ (Fin 3)} (hp : ‖p‖ = 1) (hs : s ∈ northern p) (hsp : s ≠ p) (ht : t ∈ northern p) (htp : t ≠ p) (hl : latitude p t < latitude p s) : ∃ (n : ℕ) (c : ℕ → EuclideanSpace ℝ (Fin 3)), 1 ≤ n ∧ IsDescentChain p s t n c

Piron's geometric lemma (CKM §5). If s, t lie in the northern hemisphere, are not the pole, and t is strictly lower than s, there is a finite chain of descents from s to t.