pith. sign in
module module moderate

IndisputableMonolith.Thermodynamics.BoseEinstein

show as:
view Lean formalization →

The BoseEinstein module defines the Bose-Einstein distribution function g(E) = 1/(exp((E - μ)/kT) - 1) for bosons in Recognition Science. Condensed-matter physicists or QFT researchers working within the framework would cite it when modeling thermal occupation numbers or BEC thresholds. The module is purely definitional, importing the 8-tick phase structure from SpinStatistics and the native time unit from Constants to set up the distribution with its E > μ domain restriction.

claim$g(E) = 1/ (e^{(E - μ)/kT} - 1)$ for $E > μ$, where $g(E)$ is the mean occupation number of a bosonic mode at energy $E$ with chemical potential $μ$ and temperature $T$.

background

Recognition Science obtains bosonic statistics from the eight-tick octave (T7) in the forcing chain, where even phases under the 8-tick structure yield symmetric wavefunctions. The upstream SpinStatistics module states that bosons obey Bose-Einstein statistics as a direct consequence of this phase periodicity. Constants supplies the fundamental RS time quantum τ₀ = 1 tick, which normalizes the temperature and energy scales appearing in the distribution. The module therefore introduces the standard Bose-Einstein form together with the explicit domain condition E > μ required to keep the expression positive and finite.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the Bose-Einstein distribution that later thermodynamics results (criticalTemperature, bec_ground_state_occupation) rely on when computing condensate thresholds and ground-state occupations. It directly extends the 8-tick spin-statistics connection to thermal ensembles, placing bosonic occupation numbers on the same recognition-composition foundation used for the phi-ladder and mass formulas. No open scaffolding questions are closed here.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (19)