SpinStatisticsFalsifier

formal source

 272    1. A half-integer spin particle with symmetric wavefunction
 273    2. An integer spin particle with antisymmetric wavefunction
 274    3. A particle that doesn't fit the 8-tick phase pattern -/
 275structure SpinStatisticsFalsifier where
 276  /-- The particle's spin. -/
 277  spin : Spin
 278  /-- The observed exchange symmetry. -/
 279  observed : ExchangeSymmetry
 280  /-- The observation contradicts the theorem. -/
 281  contradiction : exchangeSymmetryFromSpin spin ≠ observed
 282
 283/-- No such falsifier exists in the Standard Model. -/
 284theorem no_sm_falsifier : ∀ (p : Spin), p ∈ [Spin.zero, Spin.half, Spin.one, Spin.threeHalves, Spin.two] →
 285    exchangeSymmetryFromSpin p = if p.isHalfInteger then ExchangeSymmetry.antisymmetric else ExchangeSymmetry.symmetric := by
 286  intro p _
 287  rfl
 288
 289/-! ## QFT-002: Fermion Antisymmetry from Odd-Phase Ledger Entries -/
 290
 291/-- **THEOREM (QFT-002)**: Fermions have antisymmetric wavefunctions because they
 292    accumulate an odd phase through the 8-tick cycle.
 293
 294    The wavefunction ψ(x₁, x₂) for identical fermions satisfies:
 295    ψ(x₁, x₂) = -ψ(x₂, x₁)
 296
 297    This follows from the phase factor of -1 under exchange. -/
 298theorem fermion_antisymmetry_from_8tick {α : Type*} (s : Spin) (h : s.isHalfInteger)
 299    (ψ : α → α → ℂ) (hψ : ∀ x y, ψ x y = cyclePhase s * ψ y x) :
 300    ∀ x y, ψ x y = -(ψ y x) := by
 301  intro x y
 302  rw [hψ, fermion_antisymmetric s h]
 303  ring
 304
 305/-- Explicit ledger model: fermion entries carry odd phase. -/