nu_leading_eq
plain-language theorem explainer
The declaration sets the leading correlation-length exponent equal to the reciprocal of the golden ratio in the thermal fixed-point analysis. Physicists computing critical exponents on the recognition lattice would cite this when extracting nu_0 from the phi-ladder renormalization. The proof is a one-line reflexivity that follows once the thermal eigenvalue has been identified with phi.
Claim. The leading-order correlation-length exponent satisfies $nu_0 = 1/phi$.
background
In the ThermalFixedPoint module the phi-ladder is the geometric scaling sequence forced by T6 self-similarity, with the Fibonacci recurrence a(n+2) = a(n+1) + a(n) whose characteristic polynomial has unique positive root phi. The thermal eigenvalue y_t is this root, and the standard RG relation gives the correlation-length exponent as the reciprocal of y_t. The upstream definition states nu_leading : R := 1 / thermal_eigenvalue and records that this encodes the divergence xi ~ |t|^{-nu} with nu = 1/y_t.
proof idea
The proof is a one-line reflexivity that applies after thermal_eigenvalue_eq_phi has already established thermal_eigenvalue = phi.
why it matters
This equality completes the explicit step from PhiForcing through the Fibonacci cascade to nu_0 = 1/phi in the derivation chain of the module. It supplies the exact leading exponent required for correlation-length calculations on the recognition lattice and aligns with the forced eight-tick octave and D = 3. No open questions are closed here, but the result is a prerequisite for any quantitative thermal-sector analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.