IsBosonic

formal source

  33
  34/-- A ledger state is bosonic (integer spin) if its minimal recognition cycle
  35    completes in 8 ticks (or 1, 2 ticks for spin-0). -/
  36def IsBosonic (period : ℕ) : Prop := period % 4 = 0 ∧ period ≠ 4
  37
  38/-- The phase accumulated under a 2π rotation (4-tick advance). -/
  39noncomputable def rotationPhase (period : ℕ) : ℂ :=
  40  phaseExp ⟨4 % 8, by norm_num⟩
  41
  42/-- **KEY**: For fermions (4-tick period), the 2π rotation gives phase -1. -/
  43theorem fermion_rotation_phase_neg_one :
  44    rotationPhase 4 = -1 := by
  45  unfold rotationPhase
  46  exact phase_4_is_minus_one
  47
  48/-- For bosons (8-tick period), the 2π rotation gives phase +1 (via two half-cycles). -/
  49theorem boson_rotation_phase_pos_one :
  50    phaseExp ⟨0, by norm_num⟩ = 1 := phase_0_is_one
  51
  52/-! ## Exchange Statistics -/
  53
  54/-- Two-particle exchange involves one 2π rotation of the relative coordinate,
  55    contributing the rotation phase. For fermions: -1. For bosons: +1.
  56
  57    This is the fundamental RS derivation of the exchange sign. -/
  58theorem exchange_sign_fermion :
  59    rotationPhase 4 = -1 := fermion_rotation_phase_neg_one
  60
  61theorem exchange_sign_boson :
  62    phaseExp ⟨0, by norm_num⟩ * phaseExp ⟨0, by norm_num⟩ = 1 := by
  63  rw [phase_0_is_one]; ring
  64
  65/-! ## The Spin-Statistics Theorem -/
  66