FermionLedgerEntry

formal source

 303  ring
 304
 305/-- Explicit ledger model: fermion entries carry odd phase. -/
 306structure FermionLedgerEntry where
 307  /-- Phase accumulated (odd multiple of π). -/
 308  phase : ℂ
 309  /-- Phase is -1 (half-integer spin). -/
 310  phase_is_minus_one : phase = -1
 311
 312/-! ## QFT-003: Boson Symmetry from Even-Phase Ledger Entries -/
 313
 314/-- **THEOREM (QFT-003)**: Bosons have symmetric wavefunctions because they
 315    accumulate an even phase through the 8-tick cycle.
 316
 317    The wavefunction ψ(x₁, x₂) for identical bosons satisfies:
 318    ψ(x₁, x₂) = +ψ(x₂, x₁)
 319
 320    This follows from the phase factor of +1 under exchange. -/
 321theorem boson_symmetry_from_8tick {α : Type*} (s : Spin) (h : s.isInteger)
 322    (ψ : α → α → ℂ) (hψ : ∀ x y, ψ x y = cyclePhase s * ψ y x) :
 323    ∀ x y, ψ x y = ψ y x := by
 324  intro x y
 325  rw [hψ, boson_symmetric s h]
 326  ring
 327
 328/-- Explicit ledger model: boson entries carry even phase. -/
 329structure BosonLedgerEntry where
 330  /-- Phase accumulated (even multiple of π). -/
 331  phase : ℂ
 332  /-- Phase is +1 (integer spin). -/
 333  phase_is_plus_one : phase = 1
 334
 335/-! ## The Connection: Exchange = 2π Rotation -/
 336