be_occupation_positive
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not bound the occupation number above zero.
- Does not treat interacting or non-ideal gases.
- Does not apply to fermionic pairing in He-3.
- Does not connect directly to the J-cost functional.
formal statement (Lean)
27theorem be_occupation_positive (ε μ T : ℝ) (hT : 0 < T) (hεμ : μ < ε) :
28 0 < be_occupation ε μ T := by
proof body
Term-mode proof.
29 unfold be_occupation
30 apply div_pos one_pos
31 have harg : 0 < (ε - μ) / T := div_pos (by linarith) hT
32 linarith [Real.one_lt_exp_iff.mpr harg]
33
34/-! ## BEC Critical Temperature -/
35
36/-- BEC temperature for an ideal Bose gas. In natural units. -/