lambda_point_He4
plain-language theorem explainer
The declaration supplies the calibrated numerical value 2.17 for the lambda-point temperature of superfluid helium-4 in the Recognition Science model of eight-tick Bose-Einstein condensation. Researchers modeling superfluid transitions or verifying RS predictions against He-4 data would cite this constant. It is introduced by direct assignment of the accepted experimental estimate.
Claim. The lambda-point temperature for helium-4 is defined as $T_λ = 2.17$ K.
background
In the Recognition Science treatment of superfluidity, helium-4 is modeled as a Bose-Einstein condensate of integer-spin bosons whose coherence follows the eight-tick octave. The module derives quantized vortices from U(1) gauge invariance and places the lambda transition within the RS forcing chain. The raw lambda_point expression remains dimensionful, so this definition records the normalized experimental value $T_λ ≈ 2.17$ K used throughout the paper. Upstream constants include the bridge ratio $K = ϕ^{1/2}$, which enters the curvature functional for recurrence relations.
proof idea
This is a direct constant definition that assigns the value 2.17 without further computation or lemma application.
why it matters
This constant is invoked by the range theorem lambda_He4_in_range, which confirms that the assigned value lies inside the interval [2.0, 2.5] K. It anchors the RS superfluidity derivation to the eight-tick coherence structure and supplies the benchmark for the BEC temperature formula in the He-4 case. The parent paper RS_Superfluidity.tex uses this to connect the phi-ladder mass formula to observed transition temperatures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.