phase_0_is_one

formal source

  73
  74/-- Phase at k=0 gives 1 (boson phase).
  75    This is the identity phase - no change under exchange. -/
  76theorem phase_0_is_one : phaseExp ⟨0, by norm_num⟩ = 1 := by
  77  unfold phaseExp phase
  78  simp only [Nat.cast_zero, zero_mul, zero_div, mul_zero, Complex.ofReal_zero,
  79             Complex.exp_zero]
  80
  81/-- The fundamental frequency associated with the 8-tick. -/
  82noncomputable def fundamentalFrequency : ℝ := 8 / IndisputableMonolith.Constants.tau0
  83
  84/-! ## Core 8-Tick Theorems for Physics Derivations -/
  85
  86/-- **SPIN-STATISTICS KEY THEOREM**:
  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).