bec_temperature_positive
plain-language theorem explainer
The declaration proves that the Bose-Einstein condensation temperature stays strictly positive for any positive real mass and density. Researchers modeling superfluid helium-4 as an ideal Bose gas would cite it to guarantee a physical temperature scale before adding interaction corrections. The term-mode proof unfolds the explicit formula and chains mul_pos with the positivity tactic and Real.rpow_pos_of_pos.
Claim. If $m > 0$ and $n > 0$, then the Bose-Einstein condensation temperature $T_{BEC}(m,n) = (2π / m) (n / 2.612)^{2/3}$ satisfies $T_{BEC}(m,n) > 0$.
background
The module treats superfluid He-4 as a Bose-Einstein condensate of integer-spin bosons under the eight-tick coherence condition of Recognition Science. The definition bec_temperature supplies the critical temperature for an ideal Bose gas in natural units: $(2 π / m) (n / 2.612)^{2/3}$. This rests on the foundational distinction axioms that produce the required structural conditions and on the point construction for single-value intervals.
proof idea
The proof is a one-line wrapper. It unfolds bec_temperature, applies mul_pos to the product, invokes the positivity tactic on the prefactor $2 π / m$, and calls Real.rpow_pos_of_pos on the density term raised to the two-thirds power.
why it matters
The result secures positivity of the temperature parameter inside the superfluidity model, supporting the identification of He-4 with eight-tick boson condensation before the lambda-point correction is derived. It fills the basic consistency step in RS_Superfluidity.tex and aligns with the T7 eight-tick octave in the forcing chain. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.