import QLF_Spin import QLF_FreeEnergy set_option linter.unusedVariables false /-! # QLF_SpinorInformation — spin-½ is the atomic carrier of information The thesis (Scarver, after Cartan 1913): a **single-valued** object cannot express information; a **two-valued** one can, and the minimal two-valued object that is *covariant under rotation* is the spin-½ closure — the spinor. This module makes that dichotomy a pair of machine-checked theorems on the substrate, by fusing two results already in the repo. **Cartan (1913) is the cited classical foundation.** In *Les groupes projectifs qui ne laissent invariante aucune multiplicité plane* Cartan classified the irreducible linear representations of the orthogonal groups and found the ones that are **not** obtainable from tensors on the defining (vector) representation: the **spinor** representations. For `so(3)` the fundamental 2-dimensional representation descends only to a *double-valued* (projective) representation of `SO(3)`; the vector representation factors through `SO(3)` and is blind to `π₁(SO(3)) = ℤ₂`. QLF does not reprove Cartan's classification (it is the settled-math input, as Wallis/Stirling are for π and Reshetikhin–Turaev for the TQFT); QLF realizes the concrete `su(2)` instance and supplies the **information content** Cartan's geometry does not name. Two substrate facts, already proven: • **The double cover is genuine.** A half-spin (odd) history folds to `−I`, an integer-spin (even) one to `+I`, and `−I ≠ +I` (`QLF_Spin.spin_double_cover_nontrivial`, `concat_pairs_odd`/`concat_pairs_even`). The `−I` is exactly Cartan's double-valued spinor sign — the winding the vector cannot see. • **The half-spin ZFA closure carries exactly `log 2` nats, maximally.** With the delta recognition density on the uniform two-ordering prior, `D_KL = log 2` (`QLF_FreeEnergy.binary_kl_delta_uniform`), and no spread density does better (`binary_kl_uniform_lt_log_two`). This module fuses them under one reading — **information = log(number of distinguishable fold outcomes)**: * the **spinor** fold-alphabet `{+I, −I}` has *two* outcomes → one bit (`log 2`); * a **single-valued / vector** (integer-spin-only) fold-alphabet `{+I}` has *one* outcome → *zero* bits (`log 1 = 0`). So spin-½ is precisely the atom at which the substrate's fold becomes *informative*: the jump from `0` to one bit happens exactly when the `−I` (the double-cover sign) is admitted. Vectors are derivative — an even number of half-spin atoms, folding back to `+I` (`QLF_Spin.boson_even_pairs`) — and carry no bit of their own. See `Mathematics_From_QLF.md` § "Rung 5a — spin-½ is the atom of information (Cartan)". **§3 reproves the double-valuedness itself, from rotation matrices** — not merely cited. A full (2π) turn is `+I` on the vector (SO(3)) representation but `−I` on the spin-½ (SU(2)) representation (`spinor_double_valued_vector_blind`, from `Complex.exp_pi_mul_I` / `Real.cos_two_pi`), so the concrete double-cover instance the information claim rests on is machine-checked. Cartan (1913) is then retained *only* for the general classification (that these non-tensorial spinor irreps are the complete list, for every orthogonal group), which QLF does not formalize. -/ namespace QLF open QLF.Spin -- ========================================================================== -- 1. The fold alphabet is genuinely two-valued -- ========================================================================== /-- A single half-spin history folds to the spinor sign `−I` — Cartan's double-valued element, realized on the substrate. -/ theorem spinor_fold_negI : concatPairsMatrixFold [Twist.up] = -(1 : M) := concat_pairs_odd [Twist.up] ⟨0, rfl⟩ /-- The empty (trivially even, integer-spin) history folds to `+I` — the vector / single-valued outcome. -/ theorem vector_fold_id : concatPairsMatrixFold ([] : List Twist) = (1 : M) := concat_pairs_even [] ⟨0, rfl⟩ /-- **The fold alphabet is genuinely two-valued.** Both `+I` and `−I` are realized, and they are distinct (`spin_double_cover_nontrivial`). So the map `ts ↦ fold ts` distinguishes at least two outcomes — the minimal condition for carrying information. A vector-only (integer-spin) alphabet realizes only `+I`: a single outcome. -/ theorem fold_alphabet_two_valued : concatPairsMatrixFold [Twist.up] = -(1 : M) ∧ concatPairsMatrixFold ([] : List Twist) = (1 : M) ∧ (-(1 : M)) ≠ (1 : M) := ⟨spinor_fold_negI, vector_fold_id, spin_double_cover_nontrivial⟩ -- ========================================================================== -- 2. Information = log(number of distinguishable fold outcomes) -- ========================================================================== /-- **A single-valued object carries zero information.** If the prior has a single outcome (`p = 1`), resolving it costs nothing: `D_KL(δ ‖ 1) = 0`. This is the integer-spin / vector alphabet `{+I}`: a constant fold, no distinction, `log 1 = 0` nats. The formal content of "one-valued objects cannot express information." -/ theorem single_valued_zero_information : binary_kl 1 1 = 0 := by unfold binary_kl simp only [sub_self, zero_mul, mul_zero, add_zero, zero_add, one_mul, div_one, zero_div, Real.log_one] /-- **A two-valued object carries one bit.** The spinor fold-alphabet `{+I, −I}` has two equiprobable outcomes; resolving which one closed costs `D_KL(δ ‖ uniform₂) = log 2` — the maximal per-event information (`binary_kl_uniform_lt_log_two`). This is the spin-½ closure: the minimal object whose fold is *not* constant. -/ theorem two_valued_one_bit : binary_kl 1 (1/2) = Real.log 2 := binary_kl_delta_uniform /-- **Spin-½ is the basis of information (the dichotomy), machine-checked.** The single-valued / vector alphabet (`{+I}`, integer spin) carries `0` nats; the two-valued / spinor alphabet (`{+I, −I}`, admitting half-integer spin) carries `log 2` nats — one bit — and that is strictly more. The jump from *no* information to *one bit* happens exactly when the half-spin (the `−I` fold, Cartan's double-cover sign) is admitted. Vectors, being even composites of half-spins, fold back to `+I` and add no bit of their own. -/ theorem spin_half_is_information_atom : binary_kl 1 1 = 0 ∧ binary_kl 1 (1/2) = Real.log 2 ∧ binary_kl 1 1 < binary_kl 1 (1/2) := by refine ⟨single_valued_zero_information, two_valued_one_bit, ?_⟩ rw [single_valued_zero_information, two_valued_one_bit] exact Real.log_pos (by norm_num) -- ========================================================================== -- 3. The double-valuedness itself, reproven from rotation matrices -- ========================================================================== -- -- Sections 1–2 read the information off the *substrate's* twist fold. This section -- discharges the one thing that was previously only cited: the concrete double-cover -- instance the whole claim rests on — that a full (2π) rotation is `−I` on the spin-½ -- (spinor) representation but `+I` on the vector representation. We prove it directly from -- the explicit SU(2) and SO(3) rotation matrices, evaluated at θ = 2π, so the -- "two-valued vs single-valued" dichotomy no longer leans on Cartan for *this* instance; -- Cartan (1913) remains cited only for the *general* classification (that these spinor -- irreps are exactly the non-tensorial ones, for every orthogonal group). /-- The spin-½ (spinor) rotation about the z-axis by angle `θ`: the SU(2) element `diag(e^{-iθ/2}, e^{iθ/2})`. The half-angle is the whole point — it is what makes the representation double-valued. -/ noncomputable def spinorRotZ (θ : ℝ) : M := !![Complex.exp (-(θ : ℂ) / 2 * Complex.I), 0; 0, Complex.exp ((θ : ℂ) / 2 * Complex.I)] /-- The vector (spin-1) rotation about the z-axis by angle `θ`: the SO(3) rotation matrix. No half-angle — it is single-valued. -/ noncomputable def vectorRotZ (θ : ℝ) : Matrix (Fin 3) (Fin 3) ℝ := !![Real.cos θ, -Real.sin θ, 0; Real.sin θ, Real.cos θ, 0; 0, 0, 1] /-- **A full turn is `−I` on the spinor.** `spinorRotZ (2π) = diag(e^{-iπ}, e^{iπ}) = diag(−1, −1) = −I`: the spin-½ representation does **not** return to the identity after 360°. Proven from `Complex.exp_pi_mul_I`. This is Cartan's double-valued spinor sign, computed. -/ theorem spinorRotZ_two_pi : spinorRotZ (2 * Real.pi) = -(1 : M) := by have key : (((2 * Real.pi : ℝ)) : ℂ) / 2 = (Real.pi : ℂ) := by push_cast; ring have e11 : Complex.exp ((((2 * Real.pi : ℝ)) : ℂ) / 2 * Complex.I) = -1 := by rw [key, Complex.exp_pi_mul_I] have e00 : Complex.exp (-(((2 * Real.pi : ℝ)) : ℂ) / 2 * Complex.I) = -1 := by rw [show -(((2 * Real.pi : ℝ)) : ℂ) / 2 * Complex.I = -((((2 * Real.pi : ℝ)) : ℂ) / 2 * Complex.I) by ring, key, Complex.exp_neg, Complex.exp_pi_mul_I] norm_num simp only [spinorRotZ] rw [e00, e11] ext i j fin_cases i <;> fin_cases j <;> simp [Matrix.one_apply, Matrix.neg_apply] /-- **A full turn is `+I` on the vector.** `vectorRotZ (2π) = I₃`: the spin-1 (vector) representation returns to the identity after 360°. Proven from `Real.cos_two_pi` / `Real.sin_two_pi`. The vector is blind to the winding the spinor records. -/ theorem vectorRotZ_two_pi : vectorRotZ (2 * Real.pi) = (1 : Matrix (Fin 3) (Fin 3) ℝ) := by ext i j fin_cases i <;> fin_cases j <;> simp [vectorRotZ, Real.cos_two_pi, Real.sin_two_pi, Matrix.one_apply] /-- **The spinor is double-valued, the vector is single-valued — the same 2π rotation, two different fates, machine-checked from the rotation matrices.** The vector representation of a full turn is the identity (`+I`); the spinor representation of the *same* full turn is `−I ≠ +I` (`spin_double_cover_nontrivial`). This is the concrete double-cover instance the information dichotomy of §1–2 rests on — now proven, not cited. (Cartan 1913 is retained only for the general classification.) The vector cannot register the `ℤ₂` winding; the spinor is exactly the object that can — which is why the bit lives on the spinor. -/ theorem spinor_double_valued_vector_blind : vectorRotZ (2 * Real.pi) = (1 : Matrix (Fin 3) (Fin 3) ℝ) ∧ spinorRotZ (2 * Real.pi) = -(1 : M) ∧ (-(1 : M)) ≠ (1 : M) := ⟨vectorRotZ_two_pi, spinorRotZ_two_pi, spin_double_cover_nontrivial⟩ end QLF