superfluid_fraction_between
plain-language theorem explainer
The theorem shows that the superfluid fraction lies strictly between zero and one for any positive temperature below the lambda point. Condensed-matter physicists using the Recognition Science model of helium would cite this bound to confirm consistency with observed superfluid behavior. The proof is a compact term-mode reduction that unfolds the fraction definition and applies real-analysis inequalities to the temperature ratio raised to the critical exponent.
Claim. Let $f(T, T_λ)$ denote the superfluid fraction. For real numbers $T, T_λ$ satisfying $0 < T < T_λ$, it holds that $0 < f(T, T_λ) < 1$.
background
The module treats superfluidity as a consequence of RS eight-tick coherence: He-4 arises as a BEC of integer-spin (8-tick) bosons while He-3 involves Cooper pairing of 4-tick fermions. The superfluid fraction is constructed from the temperature ratio to the lambda point raised to the RS critical exponent, inheriting positivity and ordering from the imported J-cost and arithmetic foundations. Upstream results supply the non-strict order on LogicNat, the 8-tick phase definition, and the cost function induced by multiplicative recognizers, all of which ground the J-cost of recognition events.
proof idea
The argument unfolds the superfluid_fraction definition, establishes that the ratio T/Tlam is positive and strictly less than one via div_pos and div_lt_one, invokes rs_critical_exponent_positive together with Real.rpow_lt_one and Real.rpow_pos_of_pos to bound the powered term, and finishes with constructor and linarith.
why it matters
The result supplies the elementary physical bound required for the lambda-point and BEC-temperature siblings inside the same module. It directly supports the eight-tick octave and D=3 spatial structure of the forcing chain by ensuring the fraction respects the transition temperature. No downstream uses are recorded, yet the inequality closes the basic consistency check for the superfluidity paper proposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.