`BosonLedgerEntry`

definition

show as: view math explainer →

module: IndisputableMonolith.QFT.SpinStatistics
domain: QFT
line: 329 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.QFT.SpinStatistics on GitHub at line 329.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 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
 337/-- **KEY INSIGHT**: Exchanging two identical particles is topologically
 338    equivalent to rotating one of them by 2π.
 339
 340    This is the deep reason behind the spin-statistics connection:
 341    - 2π rotation of fermion: phase -1
 342    - 2π rotation of boson: phase +1
 343    - Exchange of particles: same as 2π rotation
 344    - Therefore: fermions antisymmetric, bosons symmetric -/
 345theorem exchange_equals_rotation :
 346    ∀ (s : Spin),
 347    (s.isHalfInteger → exchangePhase s = -1) ∧
 348    (s.isInteger → exchangePhase s = 1) := by
 349  intro s
 350  constructor
 351  · intro h
 352    exact fermion_antisymmetric s h
 353  · intro h
 354    exact boson_symmetric s h
 355
 356/-! ## Connection to Foundation.EightTick -/
 357
 358open Foundation.EightTick in
 359/-- **FOUNDATION CONNECTION**: The fermion phase (-1) derives from the

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.