lambda_point_lt_bec
plain-language theorem explainer
The inequality shows that the lambda-point temperature lies strictly below the BEC transition temperature whenever the interaction correction 0.43 a_s n^{1/3} is less than one. Physicists modeling superfluid helium-4 within the Recognition Science eight-tick coherence framework would cite this to confirm the ordering of critical temperatures. The short tactic proof unfolds the lambda_point definition, verifies positivity of the correction term, rewrites the expression as T_BEC minus a positive quantity via algebraic simplification, and closes a
Claim. Let $T_{BEC}>0$, $a_s>0$, and $n>0$ be the Bose-Einstein condensation temperature, s-wave scattering length, and number density. If the dimensionless interaction correction satisfies $0.43 a_s n^{1/3}<1$, then the lambda-point temperature obeys $T_λ(T_{BEC},a_s,n)<T_{BEC}$.
background
In the Recognition Science treatment of superfluidity, superfluid helium-4 is modeled as a Bose-Einstein condensate of integer-spin (8-tick) bosons whose coherence follows the eight-tick octave. The lambda_point function supplies the interaction-corrected transition temperature for the lambda transition. Upstream constants include the dimensionless bridge ratio $K=φ^{1/2}$ and the active edge count $A=1$ per fundamental tick, which support the broader temperature and mass ladders but are not invoked in this local argument. The module states the setting explicitly: superfluid He-4 arises from 8-tick bosons while He-3 arises from Cooper pairing of 4-tick fermions, with quantized vortices following from U(1) gauge invariance, as recorded in RS_Superfluidity.tex.
proof idea
The proof unfolds the definition of lambda_point. It establishes positivity of $n^{1/3}$ via Real.rpow_pos_of_pos, shows the correction term is positive by the positivity tactic, and rewrites lambda_point as $T_{BEC}$ minus $T_{BEC}$ times the correction via simp and ring. The final linarith step combines the positivity of $T_{BEC}$ and the correction with the rewritten equality to obtain the strict inequality.
why it matters
This result secures the strict ordering between the lambda point and the BEC temperature under the small-interaction hypothesis, feeding into sibling declarations such as lambda_point_He4 and lambda_He4_in_range. It fills the temperature-ordering step required by the RS_Superfluidity.tex paper for the eight-tick coherence model. The declaration closes a local gap in the critical-temperature ladder without new hypotheses or scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.