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. -/
depends on (20)
Lean names referenced from this declaration's body.