bose_pos
plain-language theorem explainer
The theorem shows the Bose-Einstein occupation number is strictly positive for energy above chemical potential at positive temperature. Researchers deriving quantum statistics from J-cost minimization in Recognition Science cite it to guarantee well-defined distributions. The proof is a short term-mode reduction that unfolds the definition and invokes strict monotonicity of the exponential together with positivity of division.
Claim. Let $E, mu, T in mathbb{R}$ satisfy $T > 0$ and $E > mu$. Then the Bose-Einstein occupation number $frac{1}{exp((E - mu)/T) - 1} > 0$.
background
The J-Cost to Thermodynamics Bridge module links Recognition Science's J-cost functional to standard thermodynamic distributions. J-cost is the derived cost of a multiplicative recognizer on positive ratios, given by $J(x) = (x + x^{-1})/2 - 1$. Temperature enters as the Lagrange multiplier enforcing average J-cost constraints, while eight-tick phases determine spin-statistics and thereby select Fermi-Dirac or Bose-Einstein forms. Energy is simply the real line in RS-native units; upstream cost definitions from MultiplicativeRecognizerL4 and ObserverForcing supply the non-negative J-cost values used in the bridge.
proof idea
The term proof unfolds the Bose-Einstein definition to $1/(exp((E-mu)/T)-1)$. It establishes $(E-mu)/T > 0$ by division positivity, applies the strict increase of the exponential to obtain $exp((E-mu)/T) > 1$, and concludes the denominator is positive. One_div_pos then yields the desired strict inequality.
why it matters
Positivity is a prerequisite for the module's main result that Bose-Einstein statistics arise from even-phase J-cost stacking. It supports downstream constructions of partition functions and state probabilities that connect J-cost minimization to free-energy minimization. The result sits inside the Recognition Science derivation of thermodynamics from the forcing chain and the Recognition Composition Law, ensuring occupation numbers remain physically interpretable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.