boseEinstein
plain-language theorem explainer
Bosons with even 8-tick phase symmetry obey the occupation number 1 / (exp((E - μ)/T) - 1) for E > μ and T > 0. Researchers deriving quantum statistics from ledger constraints cite this when contrasting boson and fermion cases in the spin-statistics theorem. The definition is a direct transcription of the standard form with the -1 denominator fixed by even-phase symmetric stacking.
Claim. The Bose-Einstein occupation number for energy $E$, chemical potential $μ$, and temperature $T > 0$ with $E > μ$ is given by $g(E) = 1 / (exp((E - μ)/T) - 1)$.
background
Recognition Science assigns bosons even 8-tick phase and fermions odd 8-tick phase. The Bose-Einstein form arises because even phase permits symmetric stacking, producing the -1 in the denominator; the complementary +1 appears for fermions under the odd-phase ledger constraint. Upstream definitions in BoseEinstein and JCostThermoBridge both record the identical expression g(E) = 1 / (exp((E - μ)/T) - 1) and note the requirement E > μ to keep the denominator positive. The FermiDirac module places this definition beside the odd-phase derivation of Fermi-Dirac to complete the pair of thermal distributions.
proof idea
One-line definition that directly transcribes the standard Bose-Einstein formula into RS units (k = 1). It re-exports the same expression already present in the BoseEinstein and JCostThermoBridge modules.
why it matters
Supplies the occupation number referenced by statisticsFromSpin (integer spin maps to boseEinstein) and by spin_statistics_boson. It appears as a constructor in the SSBMechanism inductive type and is invoked by eight_ticks_full_cycle to close the phase for the 8-tick octave. The definition therefore realizes the even-phase half of the T7 landmark and supplies the boson counterpart to the Fermi-Dirac derivation from odd-phase constraints in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.