structure definition def or abbrev

`BosonLedgerEntry`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 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 -/

depends on (19)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
phase in IndisputableMonolith.Foundation.EightTick decl_use
one in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
one in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
Phase in IndisputableMonolith.Information.ChurchTuringPhysicsStructure decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
phase in IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge decl_use
one in IndisputableMonolith.QFT.SpinStatistics decl_use
two in IndisputableMonolith.QFT.SpinStatistics decl_use
one in IndisputableMonolith.RecogSpec.Core decl_use
Phase in IndisputableMonolith.RRF.Hypotheses.EightTick decl_use