superfluid_fraction_at_zero
plain-language theorem explainer
The theorem establishes that the superfluid fraction reaches exactly one at zero temperature for any positive lambda-point temperature. Physicists modeling RS-derived helium superfluidity cite it to fix the low-temperature boundary in the critical-exponent formula. The proof reduces directly to the definition by unfolding and applying positivity of the exponent to collapse the zero-power term.
Claim. For every real number $T_λ > 0$, the superfluid fraction at temperature zero equals one: $1 - (0/T_λ)^α = 1$, where $α$ is the positive RS critical exponent in the definition $1 - (T/T_λ)^α$.
background
The module treats superfluid He-4 as a Bose-Einstein condensate of integer-spin bosons obeying eight-tick periodicity under RS coherence. The superfluid fraction is introduced by the sibling definition superfluid_fraction(T, Tlam) := 1 - (T/Tlam)^rs_critical_exponent. The upstream theorem rs_critical_exponent_positive supplies the strict positivity 0 < rs_critical_exponent required for the zero-power simplification.
proof idea
The proof is a one-line wrapper that unfolds superfluid_fraction and applies simp using rs_critical_exponent_positive to evaluate the zero-power term as zero.
why it matters
The result supplies the zero-temperature anchor for the superfluid fraction inside the RS eight-tick coherence model of He-4. It aligns with the T7 eight-tick octave and T8 D=3 from the forcing chain, and supports sibling calculations of the lambda point and quantized vortices in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.