rs_critical_exponent
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 in Recognition Science
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.
scope and limits
- Does not derive the exponent from a microscopic Hamiltonian.
- Does not compute numerical approximations beyond the closed form.
- Does not address temperature dependence outside the power-law form.
- Does not apply to non-superfluid phases or other transitions.
Lean usage
def example_fraction (T Tlam : ℝ) : ℝ := 1 - (T / Tlam) ^ rs_critical_exponentformal statement (Lean)
99noncomputable def rs_critical_exponent : ℝ :=
proof body
Definition body.
100 Real.log ((1 + Real.sqrt 5) / 2) / Real.log 2
101
102/-- Golden ratio (1+√5)/2 > 1. -/