lambda_He4_in_range
plain-language theorem explainer
The declaration confirms that the helium-4 lambda point lies strictly between 2.0 and 2.5 kelvin. Physicists calibrating superfluid transitions in the Recognition Science eight-tick boson model cite this interval to fix the temperature scale for He-4. The proof reduces the claim to the explicit numerical constant by unfolding the definition and applying normalization.
Claim. $2.0 < T_λ^{He4} < 2.5$, where $T_λ^{He4}$ is the calibrated lambda-point temperature for helium-4 in kelvin.
background
The module treats superfluid He-4 as a Bose-Einstein condensate of integer-spin bosons obeying eight-tick coherence, with the lambda-point marking the transition to the superfluid phase. The upstream definition records a calibrated estimate: lambda_point_He4 equals 2.17, described as the standard normalized value used by the paper since the raw lambda_point formula remains dimensionful and the file omits full unit normalization for physical He-4 density.
proof idea
The proof is a one-line wrapper that unfolds the definition of lambda_point_He4 to expose the constant 2.17 and then applies norm_num to verify the numerical inequalities.
why it matters
This numerical anchor supports the superfluidity development tied to the eight-tick octave and U(1) gauge invariance for quantized vortices in the Recognition Science framework. It supplies the concrete He-4 calibration referenced in the RS_Superfluidity paper, bridging the abstract coherence model to observed transition temperatures. No downstream theorems yet reference it, leaving open its later use in critical-exponent or vortex-quantization steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.