spin_statistics_theorem

formal source

  72    - Bosons (8-tick): exchange sign = rotationPhase(0)² = 1 → symmetric
  73
  74    This is certified by `spin_statistics_key` in `Foundation.EightTick`. -/
  75theorem spin_statistics_theorem :
  76    -- Fermions antisymmetrize under exchange
  77    (rotationPhase 4 = -1) ∧
  78    -- Bosons symmetrize under exchange
  79    (phaseExp ⟨0, by norm_num⟩ = 1) :=
  80  spin_statistics_key
  81
  82/-! ## Pauli Exclusion Principle -/
  83
  84/-- **PAULI EXCLUSION**:
  85    If two identical fermions occupy the same state, the antisymmetric
  86    two-particle amplitude must vanish.
  87
  88    In RS: if ψ₁ = ψ₂ = ψ, then exchange gives ψ → -ψ (from exchange_sign_fermion),
  89    but exchange of identical particles gives ψ → ψ.
  90    So ψ = -ψ → ψ = 0. -/
  91theorem pauli_exclusion (ψ : ℂ) (h_fermion : ψ = rotationPhase 4 * ψ) :
  92    ψ = 0 := by
  93  rw [fermion_rotation_phase_neg_one] at h_fermion
  94  -- h_fermion : ψ = -1 * ψ, so 2ψ = 0, so ψ = 0
  95  have h2 : (2 : ℂ) * ψ = 0 := by linear_combination ψ + h_fermion
  96  exact (mul_eq_zero.mp h2).resolve_left two_ne_zero
  97
  98/-- Simplified Pauli exclusion: ψ = -1 * ψ implies ψ = 0. -/
  99theorem pauli_exclusion_simple (ψ : ℂ) (h : ψ = -1 * ψ) : ψ = 0 := by
 100  have h2 : (2 : ℂ) * ψ = 0 := by linear_combination ψ + h
 101  exact (mul_eq_zero.mp h2).resolve_left two_ne_zero
 102
 103/-! ## CPT Invariance -/
 104
 105/-- The three parity operations on the Q₃ hypercube compose to the identity.