spin_statistics_key

formal source

  87    Phase k=4 (half-cycle) gives -1, which is the fermion antisymmetry sign.
  88    Phase k=0 (identity) gives 1, which is the boson symmetry sign.
  89    This connects 8-tick structure to spin-statistics. -/
  90theorem spin_statistics_key :
  91    phaseExp ⟨4, by norm_num⟩ = -1 ∧ phaseExp ⟨0, by norm_num⟩ = 1 :=
  92  ⟨phase_4_is_minus_one, phase_0_is_one⟩
  93
  94/-- The 8-tick structure generates the group ℤ/8ℤ.
  95    This is isomorphic to the discrete symmetry group of RS. -/
  96theorem eight_tick_generates_Z8 :
  97    ∀ k : Fin 8, ∃ n : ℕ, phaseExp k = (phaseExp ⟨1, by norm_num⟩)^n := by
  98  intro k
  99  use k.val
 100  unfold phaseExp phase
 101  rw [← Complex.exp_nat_mul]
 102  congr 1
 103  push_cast
 104  ring
 105
 106/-- Sum of all 8 phases equals zero (roots of unity).
 107    This is the foundation of vacuum fluctuation cancellation.
 108    The 8th roots of unity sum to 0: 1 + ζ + ζ² + ... + ζ⁷ = 0 where ζ = exp(iπ/4). -/
 109theorem sum_8_phases_eq_zero :
 110    ∑ k : Fin 8, phaseExp k = 0 := by
 111  -- The sum of n-th roots of unity is 0 for n > 1
 112  -- Let ζ = exp(2πi/8) = exp(iπ/4), a primitive 8th root of unity
 113  let ζ : ℂ := Complex.exp (2 * Real.pi * Complex.I / 8)
 114  -- ζ is a primitive 8th root of unity
 115  have hζ_prim : IsPrimitiveRoot ζ 8 := by
 116    have h8pos : (8 : ℕ) ≠ 0 := by norm_num
 117    exact Complex.isPrimitiveRoot_exp 8 h8pos
 118  -- Show that phaseExp k = ζ^k
 119  have h_phase_as_power : ∀ k : Fin 8, phaseExp k = ζ ^ (k : ℕ) := by
 120    intro k