be_occupation_positive
plain-language theorem explainer
The Bose-Einstein occupation number is strictly positive for positive temperature whenever chemical potential lies below the energy level. Physicists deriving BEC critical temperatures or vortex quantization in the Recognition Science eight-tick framework cite this to keep occupation numbers physical. The proof is a short term-mode argument that unfolds the definition and invokes positivity of the exponential via linear arithmetic.
Claim. For real numbers $ε, μ, T$ with $T > 0$ and $μ < ε$, the Bose-Einstein occupation number $1/ (e^{(ε - μ)/T} - 1)$ is positive.
background
The Superfluidity module derives superfluid He-4 as Bose-Einstein condensation of integer-spin bosons obeying eight-tick periodicity from the Breath1024 framework. The occupation number is defined as $1/(exp((ε-μ)/T)-1)$, with temperature obtained as the inverse Lagrange multiplier from the Boltzmann distribution, itself linked to J-cost derivatives. Upstream results supply the period T as a natural number and the triangular number T(n) = n(n+1)/2 for counting coherence steps.
proof idea
The proof unfolds the be_occupation definition, applies div_pos to the constant numerator 1, builds an auxiliary inequality showing (ε-μ)/T > 0 via div_pos and linarith, then uses linarith together with the lemma Real.one_lt_exp_iff.mpr to conclude the denominator is positive.
why it matters
This result supplies the basic positivity needed before the module derives BEC critical temperature and quantized vortices under eight-tick U(1) coherence. It fills the elementary physicality check in the RS superfluidity development, ensuring the occupation formula remains valid prior to computing lambda-point transitions or critical exponents. No downstream theorems are recorded yet, but the lemma anchors the passage from microscopic occupation to macroscopic superfluid order.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.