superfluid_fraction_at_lambda
plain-language theorem explainer
The theorem fixes the superfluid fraction to zero exactly when temperature equals the lambda transition Tlam. Physicists modeling He-4 superfluidity inside the Recognition Science eight-tick coherence framework cite it as the boundary condition separating normal and superfluid regimes. The proof is a one-line term reduction that unfolds the fraction definition and simplifies via division by a positive real together with the unit exponent rule.
Claim. Let $T_λ > 0$. Then the superfluid fraction evaluated at temperature $T_λ$ equals zero.
background
The module treats superfluid He-4 as a Bose-Einstein condensate of integer-spin (8-tick) bosons and He-3 as Cooper-paired fermions, both arising from RS eight-tick coherence. The superfluid_fraction function returns the proportion of fluid in the superfluid phase; its value is required to vanish at the lambda point to mark the transition to normal fluid. Upstream results supply the fundamental period T from Breath1024, the triangular-number synchronization T from Gap45, and the collision-free property from OptionAEmpiricalProgram, all of which constrain the coherence conditions that locate the lambda transition.
proof idea
The proof proceeds by direct term reduction. It unfolds the definition of superfluid_fraction and invokes simp with div_self (for a positive denominator) together with the real-number identity for exponent one.
why it matters
The result anchors the upper edge of the superfluid phase in the RS He-4 model, consistent with the eight-tick octave (T7) and the lambda-point theorems listed among the module siblings. It supplies the boundary condition presupposed by the paper proposition on quantized vortices from U(1) gauge invariance. No open scaffolding questions are closed by this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.