bose_einstein_positive
plain-language theorem explainer
The declaration proves that the Bose-Einstein distribution function is strictly positive when the energy level exceeds the chemical potential at positive temperature. Physicists modeling boson statistics within the Recognition Science framework would reference it to ensure the occupation number remains physically meaningful. The proof reduces the claim to the positivity of the exponential term via unfolding and standard real analysis lemmas.
Claim. For real numbers $E, mu, T$ with $T > 0$ and $E > mu$, the Bose-Einstein distribution $1/ (exp((E - mu)/T) - 1)$ is positive.
background
The module derives the Bose-Einstein distribution from Recognition Science's even-phase ledger constraint for bosons with integer spin. The distribution function is defined as $g(E) = 1 / (exp((E - mu)/T) - 1)$, requiring $E > mu$ to avoid divergence. This emerges from maximizing entropy under no-exclusion and fixed energy/particle constraints, tied to the 8-tick structure. Upstream, the SpinStatistics module supplies the spin value distinguishing bosons (integer) from fermions. The PrimitiveDistinction and SpectralEmergence supply foundational distinctions and edge counts in the D-cube, supporting the ledger framework.
proof idea
This is a term proof that first unfolds the definition of boseEinstein. It then applies one_div_pos.mpr to reduce positivity of the reciprocal to positivity of the denominator. The key steps establish (E - mu)/T > 0 using div_pos and linarith, invoke Real.one_lt_exp_iff to obtain exp((E - mu)/T) > 1, and conclude with linarith.
why it matters
This result secures the well-definedness of the Bose-Einstein distribution in the Recognition Science thermodynamics, supporting derivations from the even-phase ledger (T7 eight-tick octave). It underpins maximum-entropy derivations of quantum statistics and connects to the alpha band and phi-ladder constants elsewhere in the framework. No downstream uses are recorded yet, but it closes a basic positivity check needed for physical applications like BEC sensors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.