rs_critical_exponent_positive
plain-language theorem explainer
The declaration establishes that the RS critical exponent, defined as the ratio of the natural logarithm of the golden ratio to the natural logarithm of 2, is strictly positive. Researchers modeling superfluid phase transitions cite it to guarantee that the exponent in the superfluid fraction formula produces values strictly between zero and one below the lambda point. The proof is a term-mode reduction that unfolds the definition and splits the positivity claim via the division-positivity lemma on the two logarithms.
Claim. $0 < (ln φ) / (ln 2)$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module sets superfluid He-4 as a Bose-Einstein condensate of integer-spin bosons obeying eight-tick periodicity and He-3 as Cooper-paired fermions with four-tick periodicity. The critical exponent is introduced by definition as the ratio of the natural log of the golden ratio to the natural log of 2. This rests on the upstream lemma that the golden ratio exceeds one, which is proved by comparing square roots and applying linear arithmetic.
proof idea
The proof unfolds the definition of the critical exponent to expose the quotient of logarithms. It applies the div_pos lemma to reduce the claim to two separate positivity statements. The first is discharged directly by the golden_ratio_gt_one lemma together with Real.log_pos; the second is discharged by norm_num confirming that the logarithm of 2 is positive.
why it matters
The result is invoked by the theorems superfluid_fraction_at_zero and superfluid_fraction_between that fix the superfluid fraction at 1 when T equals 0 and strictly between 0 and 1 for 0 < T < Tλ. It supplies the required positivity for the exponent in the superfluid fraction formula, aligning with the eight-tick coherence and the golden-ratio fixed point from the forcing chain. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.