lambda_point
plain-language theorem explainer
The lambda_point definition supplies the interaction-corrected lambda transition temperature for superfluid He-4 as T_BEC scaled by the factor (1 - 0.43 a_s n^{1/3}). Researchers modeling the shift from ideal BEC temperature to the observed lambda point in quantum fluids would cite this expression. It is realized as a direct algebraic term with no lemmas or tactics applied.
Claim. The lambda-point temperature is given by $T_λ = T_{BEC} (1 - 0.43 a_s n^{1/3})$, where $T_{BEC}$ is the Bose-Einstein condensation temperature, $a_s$ the s-wave scattering length, and $n$ the number density.
background
The module treats superfluid He-4 as a BEC of integer-spin (8-tick) bosons whose coherence follows the eight-tick octave. Superfluid He-3 arises instead from Cooper pairing of half-integer-spin (4-tick) fermions. The local setting identifies quantized vortices with U(1) gauge invariance and places the lambda point as the normal-to-superfluid transition temperature.
proof idea
The definition is a direct term-mode expression that multiplies the supplied BEC temperature by the linear interaction correction factor.
why it matters
This definition supplies the left-hand side of the downstream inequality lambda_point_lt_bec, which proves the lambda point lies below T_BEC under positive scattering length. It fills the superfluidity section by connecting the RS eight-tick boson condensate to the observed He-4 transition, consistent with the T7 eight-tick octave and D = 3. The numerical coefficient 0.43 remains an external input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.