boseEinstein
plain-language theorem explainer
Bose-Einstein occupation number is supplied as the even-phase case in the J-cost thermodynamics bridge. Workers on spin-statistics or symmetry breaking from Recognition Science cite it when mapping 8-tick phases to multiple occupancy. The definition is a direct transcription of the standard formula whose -1 encodes symmetric stacking.
Claim. The Bose-Einstein distribution is $g(E,μ,T)=1/ (e^{(E-μ)/T}-1)$ for temperature $T>0$ and energy $E>μ$.
background
The module connects J-cost minimization to thermodynamic distributions via the Recognition Composition Law and eight-tick phase symmetry. J-cost is defined as $J(x)=½(x+1/x)-1$; temperature enters as the Lagrange multiplier enforcing average J-cost. The local setting states that even-phase stacking produces the Bose-Einstein case while odd-phase stacking produces Fermi-Dirac. Upstream imports supply the 8-tick cycle (EightTick) and the statisticsFromSpin map (SpinStatistics).
proof idea
Direct definition that transcribes the formula from the even-phase J-cost constraint stated in the module doc-comment.
why it matters
It realizes the bose_from_even_phase_jcost item listed in the module's main theorems and is invoked by statisticsFromSpin, spin_statistics_boson, and bose_can_exceed_one. The declaration therefore closes the 8-tick phases → Spin-statistics → Bose distributions step in the forcing chain (T7). It also appears in the SSBMechanism inductive type for symmetry-breaking cases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.