nu_leading
plain-language theorem explainer
The definition sets the leading correlation-length exponent ν₀ equal to the reciprocal of the thermal eigenvalue y_t at the recognition-lattice fixed point. Researchers studying renormalization-group flows on the φ-ladder cite this when relating the divergence of the correlation length to the forced scaling. It is a one-line definition that inverts the already-proved thermal_eigenvalue.
Claim. $ν_0 := 1/y_t$ where $y_t$ is the thermal eigenvalue of the renormalization-group fixed point on the recognition lattice.
background
The module places the thermal fixed point on the recognition lattice ℤ³ with unit cell Q₃. The φ-ladder arises as the unique geometric scaling sequence forced by T6 self-similarity, so consecutive rungs obey the Fibonacci recurrence whose characteristic polynomial λ² − λ − 1 has unique positive root φ. Upstream, thermal_eigenvalue is defined directly as phi, confirming y_t = φ and supplying the input to the present definition.
proof idea
One-line definition that inverts thermal_eigenvalue.
why it matters
This supplies the base exponent ν₀ = 1/φ that enters the corrected formula in nu_corrected. It closes the chain from PhiForcing (T6) through the Fibonacci cascade to the standard RG relation ν₀ = 1/y_t. The ThermalFixedPointCert structure records this equality as part of the fixed-point certificate. It touches the open question of how anomalous-dimension corrections modify the leading value for D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.