be_occupation
plain-language theorem explainer
be_occupation encodes the standard Bose-Einstein occupation number n(ε, μ, T) = 1/(exp((ε-μ)/T)-1) for real energy, chemical potential, and temperature. Physicists modeling superfluid He-4 as an 8-tick BEC in the Recognition Science framework cite it to supply the occupation statistics. The definition is a direct one-line transcription of the textbook formula with no added RS structure or hypotheses.
Claim. The Bose-Einstein occupation number is given by $n(ε, μ, T) = 1 / (e^{(ε - μ)/T} - 1)$.
background
The Superfluidity module treats superfluid He-4 as a Bose-Einstein condensate of integer-spin (8-tick) bosons and He-3 as Cooper-paired fermions, with quantized vortices arising from U(1) gauge invariance. The function supplies the classical occupation number at temperature T in units where the eight-tick octave sets the coherence scale. Upstream results include T as the fundamental period from Breath1024, collision-free structures from OptionAEmpiricalProgram, and simplicial edge lengths from EdgeLengthFromPsi, though the occupation definition itself is independent of these.
proof idea
One-line definition that directly encodes the textbook Bose-Einstein formula using Real.exp and division.
why it matters
This definition is used by the downstream theorem be_occupation_positive, which proves positivity when μ < ε and T > 0. It supplies the statistical input for the RS superfluidity analysis, connecting to the T7 eight-tick octave and the treatment of He-4 as an 8-tick BEC in the forcing chain. The declaration fills the occupation-number component of the RS_Superfluidity paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.