rs_critical_exponent
plain-language theorem explainer
RS critical exponent α is defined as ln φ / ln 2 where φ is the golden ratio. Physicists working on the lambda transition in superfluid helium cite this value to set the power-law scaling of superfluid density. The definition is a direct closed-form transcription of the logarithmic ratio with no further reduction steps.
Claim. $α = ln φ / ln 2$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module models superfluid He-4 as a Bose-Einstein condensate of integer-spin (8-tick) bosons and He-3 as Cooper-paired fermions, both governed by eight-tick coherence from the unified forcing chain. The critical exponent α enters the superfluid fraction ρ_s(T)/ρ = 1 - (T/T_λ)^α. This definition supplies the explicit numerical value derived from the self-similar fixed point φ.
proof idea
The definition is the explicit ratio of natural logarithms: log((1 + √5)/2) divided by log(2). It is a one-line closed-form expression with no lemma applications or tactic steps.
why it matters
It supplies the exponent used by the superfluid fraction definition and the positivity and bounding theorems in the same module. The value connects the phi fixed point (T5-T6) to the eight-tick octave (T7) in the superfluidity model of RS_Superfluidity.tex. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.