QLF_Spin.lean

import QLF_BaryonWinding
import PauliExclusion

set_option linter.unusedVariables false

/-!
# QLF_Spin — spin demystified: spin IS the QLF twists

Standard spin is opaque: a 720° turn to return, a "magnetic moment" tangled up with a
"charge". QLF dissolves the mystery by showing spin is *literally* the twists — the
σ-matrix generators of the 8-twist alphabet (`^v = ±σ_y`, `<> = ∓σ_x`, `/\ = ±σ_z`,
`+− = ±I`, `QLF_TwistAlphabet`). A particle carries **two independent 720° half-spins**:

* a **perpendicular / chiral** component whose handedness *relative to motion* is what
  electric charge *is* — a positron coming toward you reads clockwise, but seen from
  behind it is counterclockwise, i.e. an electron of opposite charge. So **charge
  conjugation = viewing from behind = reversal**, the antiparticle map
  `(ts.map Twist.conj).reverse` (`QLF_Majorana`). Under it BOTH a winding/chirality
  invariant and the charge **negate together** (`C_eq_motional_reversal`).
* a **flat up/down** component, *independent of motion*, that is the magnetic moment
  (`magneticMoment`) — Stern–Gerlach, magnetism (`Magnetism_Spatial_Dynamics.md`).
  Reversing motion flips the chiral/charge component but leaves the flat one fixed
  (`flat_independent_of_motion`): the formal statement of "two independent axes".

The three spatial twist axes are the **su(2) generators** (`[σᵢ,σⱼ]=2iεᵢⱼₖσₖ`,
`su2_comm_xy/yz/zx`); the group they generate is **SU(2)**, the *double cover* of the
rotation group **SO(3)**. The 720°-to-return mystery is exactly that cover: a 360°
rotation (one Hermitian twist pair, `hermitian_pair_folds_to_negI`) lifts to `−I`, NOT the
identity; only 720° (two pairs) reaches `+I`. The kernel `{+I,−I}` is genuine
(`spin_double_cover_nontrivial`). Same `+I` closure is the opposite-spin **singlet**
(annihilation), and integer spin = an even number of half-spin pairs (a photon = two
halves = spin 1, `photon_integer_spin`); like-spin fermions
**exclude** (`pauli_exclusion`). The **neutrino** `^v` is the self-conjugate (Majorana)
spin — the same from behind — hence **neutral** (`neutrino_neutral`); the electron is
Dirac (`electron_not_majorana`).

Every dynamical claim below reduces to an already-proven theorem. The physical
identifications (`perpChirality`, `chiralCharge`, `magneticMoment`) are *naming* defs —
which twist invariant we call charge / chirality / magnetic moment — not axioms. See
`Spin_QLF.md`.
-/

namespace QLF.Spin

open QLF QLF.Majorana QLF.BaryonWinding

-- ==========================================================================
-- 1. The 720° double cover — spin's "turn twice to return"
-- ==========================================================================

/-- **360° = one Hermitian twist pair folds to `−I`** — the fermion's sign flip under a
    single full turn. Direct reuse of `hermitian_pair_folds_to_negI`. -/
theorem rotation_360_eq_negI (t : Twist) :
    t.toMatrix * t.conj.toMatrix = -(1 : M) :=
  hermitian_pair_folds_to_negI t

/-- **720° = two Hermitian pairs fold to `+I`** — identity restored only after a double
    turn. This `+I` is also the opposite-spin singlet closure (see
    `opposite_spin_singlet_closes`): the double cover and annihilation are one fact. -/
theorem rotation_720_eq_id (s t : Twist) :
    (s.toMatrix * s.conj.toMatrix) * (t.toMatrix * t.conj.toMatrix) = (1 : M) := by
  rw [hermitian_pair_folds_to_negI s, hermitian_pair_folds_to_negI t, neg_mul_neg, one_mul]

/-- The same `+I` via the canonical even-pair fold (`concat_pairs_even`, N = 2 pairs). -/
theorem rotation_720_concat (s t : Twist) :
    concatPairsMatrixFold [s, t] = (1 : M) :=
  concat_pairs_even [s, t] ⟨1, rfl⟩

-- ==========================================================================
-- 1a. Worked QuCalc folds — the literal twist arithmetic (`/qucalc`)
-- ==========================================================================
--
-- `Twist.toMatrix`: ^ = σy, v = −σy, < = −σx, > = σx, / = σz, \ = −σz, + = I, − = −I.
-- These show the actual matrix products a QuCalc fold computes.

/-- **`^v` fold** (the half-spin pair / neutrino loop): `σ_y · (−σ_y) = −σ_y² = −I`. One
    full turn → the fermion sign `−I`. -/
theorem fold_up_down : Twist.up.toMatrix * Twist.down.toMatrix = -(1 : M) := by
  show σy * (-σy) = -(1 : M)
  rw [mul_neg, sigma_y_sq]

/-- **`^v^v` fold**: `(−I)(−I) = +I`. The 720° return, written out. -/
theorem fold_up_down_twice :
    (Twist.up.toMatrix * Twist.down.toMatrix) * (Twist.up.toMatrix * Twist.down.toMatrix)
      = (1 : M) := by
  rw [fold_up_down, neg_mul_neg, one_mul]

/-- **Cross-axis fold `^>`**: `σ_y · σ_x = −i σ_z`. Two different axes fold to a third
    (times `−i`) — the chiral/winding content, not a scalar (a `/qucalc` cross-fold). -/
theorem fold_up_right : Twist.up.toMatrix * Twist.right.toMatrix = -(Complex.I • σz) := by
  show σy * σx = -(Complex.I • σz)
  exact sigma_yx

/-- **Gauge fold `+−`**: `I · (−I) = −I` — the charge pair. `+` carries `+1` charge,
    `−` carries `−1` (`twistCharge`). -/
theorem fold_plus_minus : Twist.plus.toMatrix * Twist.minus.toMatrix = -(1 : M) := by
  show (1 : M) * (-1) = -(1 : M)
  rw [one_mul]

/-- **The electron loop `^<v>` fold**: a cross-axis history that is *not* a concatenation
    of adjacent pairs, yet still folds to the fermion sign `−I`. Step by step (via the
    σ-product identities):
    `σ_y · (−σ_x)` = `iσ_z`; `(iσ_z) · (−σ_y)` = `−σ_x`; `(−σ_x) · σ_x` = `−I`.
    So the electron is a half-spin fermion. It is *not* its own antiparticle
    (`electron_not_majorana`, [`QLF_Majorana`](QLF_Majorana.lean)) — it is **Dirac**, with a
    distinct positron `v>v<`; the Majorana/Dirac split is the conjugate-reverse
    fixed-point test, not the fold value (both `^v` and `^<v>` fold to `−I`). -/
theorem fold_electron :
    Twist.up.toMatrix * Twist.left.toMatrix * Twist.down.toMatrix * Twist.right.toMatrix
      = -(1 : M) := by
  show σy * (-σx) * (-σy) * σx = -(1 : M)
  have e1 : σy * (-σx) = Complex.I • σz := by
    rw [mul_neg, sigma_yx, neg_neg]
  have e2 : (Complex.I • σz) * (-σy) = -σx := by
    rw [mul_neg, smul_mul_assoc, sigma_zy, smul_neg, neg_neg, smul_smul,
      Complex.I_mul_I, neg_one_smul]
  have e3 : (-σx) * σx = -(1 : M) := by
    rw [neg_mul, sigma_x_sq]
  rw [e1, e2, e3]

-- ==========================================================================
-- 1b. Integer spin = a composite of half-spins
-- ==========================================================================

/-- **Integer spin = an even number of half-spin pairs ⇒ boson (`+I`).** Each Hermitian
    pair is a spin-½ unit folding to `−I`; an even count folds to `+I` (returns under
    360°). Reuse of `concat_pairs_even`. -/
theorem boson_even_pairs (ts : List Twist) (h : Even ts.length) :
    concatPairsMatrixFold ts = (1 : M) :=
  concat_pairs_even ts h

/-- **Half-integer spin = an odd number of half-spin pairs ⇒ fermion (`−I`).** -/
theorem fermion_odd_pairs (ts : List Twist) (h : Odd ts.length) :
    concatPairsMatrixFold ts = -(1 : M) :=
  concat_pairs_odd ts h

/-- **The photon is spin 1.** A half-spin photon and a half-spin antiphoton — two
    half-spin pairs (½ + ½ = 1) — fold to `+I`: an integer-spin boson. (Photon = the
    joint emitter–absorber ZFA closure, `Collective_Electrodynamics.md`.) So integer spin
    is not fundamental: it is two half-spins, exactly as the substrate forces. -/
theorem photon_integer_spin (photonHalf antiphotonHalf : Twist) :
    concatPairsMatrixFold [photonHalf, antiphotonHalf] = (1 : M) :=
  concat_pairs_even [photonHalf, antiphotonHalf] ⟨1, rfl⟩

-- ==========================================================================
-- 1c. Spin and SU(2) / SO(3) — the double cover, demystified
-- ==========================================================================
--
-- The three spatial twist axes (σx = `<>`, σy = `^v`, σz = `/\`) are the **su(2)
-- generators**: their commutators close the su(2) Lie algebra `[σᵢ,σⱼ] = 2i εᵢⱼₖ σₖ`
-- (below, from the σ-product identities in QLF_TwistAlphabet). The group they generate
-- is **SU(2)** — the *double cover* of the rotation group SO(3). The "720° to return"
-- mystery is exactly this cover: a 360° physical rotation (one Hermitian pair) lifts to
-- `−I` in SU(2) (`rotation_360_eq_negI`) — NOT the identity — and only 720° (two pairs)
-- reaches `+I` (`rotation_720_eq_id`). The fold outcomes `{+I, −I}` ARE the kernel of
-- `SU(2) → SO(3)`, and `−I ≠ +I` makes the cover genuine (`spin_double_cover_nontrivial`).

/-- **su(2) on the twist axes**, x–y: `[σx, σy] = 2i σz`. The `<>` and `^v` axes close
    the Lie algebra of SU(2). Reuse of the σ-product identities. -/
theorem su2_comm_xy : σx * σy - σy * σx = (2 * Complex.I) • σz := by
  rw [sigma_xy, sigma_yx, sub_neg_eq_add, ← add_smul]; congr 1; ring

/-- su(2), y–z: `[σy, σz] = 2i σx`. -/
theorem su2_comm_yz : σy * σz - σz * σy = (2 * Complex.I) • σx := by
  rw [sigma_yz, sigma_zy, sub_neg_eq_add, ← add_smul]; congr 1; ring

/-- su(2), z–x: `[σz, σx] = 2i σy`. -/
theorem su2_comm_zx : σz * σx - σx * σz = (2 * Complex.I) • σy := by
  rw [sigma_zx, sigma_xz, sub_neg_eq_add, ← add_smul]; congr 1; ring

/-- **SU(2) is a genuine double cover of SO(3).** The 360° fold lands on `−I`, distinct
    from the `+I` of 720°: the kernel of `SU(2) → SO(3)` is the two-element group
    `{+I, −I}`, not trivial. This `−1` is the fermion's sign under one full turn. -/
theorem spin_double_cover_nontrivial : (-(1 : M)) ≠ (1 : M) := by
  intro h
  have h00 : (-(1 : M)) 0 0 = (1 : M) 0 0 := congrFun (congrFun h 0) 0
  rw [Matrix.neg_apply, Matrix.one_apply_eq] at h00
  norm_num at h00

-- ==========================================================================
-- 2. Charge conjugation = viewing from behind = reversal
-- ==========================================================================

/-- **Perpendicular-spin chirality** = the 3-axis winding sign (`baryonNumber`). The
    "handedness relative to the observer" is an orientation-odd winding; viewing from
    behind reverses it. A naming def. -/
def perpChirality (ts : List Twist) : Int := baryonNumber ts

/-- Viewing from behind (the antiparticle = conjugate-and-reverse) **flips the
    perpendicular chirality**. Direct reuse of `baryon_dagger_odd`. -/
theorem perpChirality_conj (ts : List Twist) :
    perpChirality (antiparticle ts) = - perpChirality ts := by
  unfold perpChirality; exact baryon_dagger_odd ts

/-- **Electric-charge weight on a twist**: the gauge pair carries the sign (`+` = +1,
    `−` = −1); spatial twists are charge-neutral. The twist-alphabet analog of
    `QLF_BMinusL.chargeWeight`. -/
def twistCharge : Twist → Int
  | Twist.plus  => 1
  | Twist.minus => -1
  | _ => 0

/-- **Charge** of a twist history = the signed gauge count. -/
def chiralCharge (ts : List Twist) : Int := (ts.map twistCharge).sum

/-- Conjugating a twist negates its charge (`+ ↔ −`). -/
theorem twistCharge_conj (t : Twist) : twistCharge (Twist.conj t) = - twistCharge t := by
  cases t <;> decide

private theorem chiralCharge_append (l : List Twist) (x : Twist) :
    chiralCharge (l ++ [x]) = chiralCharge l + twistCharge x := by
  simp [chiralCharge, List.map_append, List.sum_append, List.map_cons, List.map_nil,
    List.sum_cons, List.sum_nil]

private theorem antiparticle_cons (a : Twist) (rest : List Twist) :
    antiparticle (a :: rest) = antiparticle rest ++ [Twist.conj a] := by
  simp [antiparticle, List.map_cons, List.reverse_cons]

/-- Viewing from behind **negates the charge** — a positron read from behind carries the
    electron's charge. (`reverse` preserves the sum; `conj` negates each term.) -/
theorem chiralCharge_conj (ts : List Twist) :
    chiralCharge (antiparticle ts) = - chiralCharge ts := by
  induction ts with
  | nil => simp [chiralCharge, antiparticle]
  | cons a rest ih =>
    rw [antiparticle_cons, chiralCharge_append, ih, twistCharge_conj]
    simp only [chiralCharge, List.map_cons, List.sum_cons]
    ring

/-- **Charge conjugation = motional reversal.** Under "viewing from behind"
    (`antiparticle` = conjugate-and-reverse) the **charge and the perpendicular
    chirality co-negate** — a positron coming toward you reads, from behind, as an
    electron: opposite charge *and* opposite handedness, together. -/
theorem C_eq_motional_reversal (ts : List Twist) :
    chiralCharge (antiparticle ts) = - chiralCharge ts ∧
    perpChirality (antiparticle ts) = - perpChirality ts :=
  ⟨chiralCharge_conj ts, perpChirality_conj ts⟩

-- ==========================================================================
-- 3. The neutrino — the self-conjugate spin is neutral
-- ==========================================================================

/-- **A Majorana spin (its own antiparticle) is neutral**: self-conjugacy forces both
    its charge and its perpendicular chirality to vanish (`x = −x ⟹ x = 0`). Looking
    the same from behind leaves no charge handedness. -/
theorem majorana_is_neutral (ts : List Twist) (h : Majorana ts) :
    chiralCharge ts = 0 ∧ perpChirality ts = 0 := by
  have hc := chiralCharge_conj ts
  have hp := perpChirality_conj ts
  rw [h] at hc hp
  exact ⟨by omega, by omega⟩

/-- **The neutrino `^v` is neutral** — it is the Majorana fixed point
    (`neutrino_majorana`), so it has no charge and no perpendicular chirality: a pure
    (σ_y) flat spin, the same viewed from behind. The electron is *not* self-conjugate
    (`electron_not_majorana`), so it is a charged Dirac particle. -/
theorem neutrino_neutral :
    chiralCharge [Twist.up, Twist.down] = 0 ∧ perpChirality [Twist.up, Twist.down] = 0 :=
  majorana_is_neutral _ neutrino_majorana

-- ==========================================================================
-- 4. Exclusion and annihilation
-- ==========================================================================

/-- **Like-spin exclusion**: two identical fermionic processes anticommute to zero — the
    Pauli exclusion principle, reused verbatim (`pauli_exclusion`). Same-flat-spin
    fermions cannot co-occupy. -/
theorem like_spin_excludes (p : RhoProcess) : fermi_antisym p p = 0 :=
  pauli_exclusion p

/-- **Opposite-spin singlet closes (annihilation)**: two `−I` half-spin folds compose to
    `+I` — a fully closed (ZFA) pair that annihilates to vacuum. The same `+I` as the
    720° return (`rotation_720_eq_id`): annihilation and the double cover are one fact. -/
theorem opposite_spin_singlet_closes (s t : Twist) :
    (s.toMatrix * s.conj.toMatrix) * (t.toMatrix * t.conj.toMatrix) = (1 : M) := by
  rw [hermitian_pair_folds_to_negI s, hermitian_pair_folds_to_negI t, neg_mul_neg, one_mul]

-- ==========================================================================
-- 5. Magnetism — the flat axis, independent of motion
-- ==========================================================================

/-- A ± orientation. -/
inductive Sign | plus | minus
deriving DecidableEq, Repr

def Sign.neg : Sign → Sign
  | Sign.plus => Sign.minus
  | Sign.minus => Sign.plus

/-- The two-axis spin descriptor: a **chiral** sign (relative to motion → charge sense)
    and a **flat** up/down sign (independent of motion → magnetic moment). -/
structure SpinState where
  perp : Sign
  flat : Sign
deriving DecidableEq, Repr

/-- The **magnetic moment** is the flat spin component (Stern–Gerlach up/down). -/
def magneticMoment (sp : SpinState) : Sign := sp.flat

/-- **The flat axis is independent of motion.** Reversing motion flips the chiral/charge
    component (`perp`, cf. `C_eq_motional_reversal`) but leaves the magnetic moment
    fixed — the formal content of "two independent spin axes". -/
theorem flat_independent_of_motion (sp : SpinState) :
    magneticMoment { perp := sp.perp.neg, flat := sp.flat } = magneticMoment sp := rfl

end QLF.Spin