nu_corrected_at_zero
plain-language theorem explainer
The theorem shows that the anomaly-corrected correlation-length exponent equals its leading-order value when the anomaly parameter is zero, for any real dimension input. Researchers deriving renormalization-group exponents from the forced phi-ladder would cite this to anchor the base case before inserting higher-order terms. The proof is a one-line term wrapper that unfolds the corrected definition, applies the zero-anomaly lemma, and closes by ring simplification.
Claim. For any real number $D$, the corrected correlation-length exponent satisfies $nu_{corrected}(D,0)=nu_{leading}$.
background
The ThermalFixedPoint module treats the renormalization group on the recognition lattice Z^3 with unit cell Q3. Self-similarity (T6) forces the phi-ladder via the Fibonacci recurrence phi^{n+2}=phi^{n+1}+phi^n; the characteristic polynomial lambda^2-lambda-1=0 has unique positive root phi, so the thermal eigenvalue is phi and the leading exponent is nu_leading=1/phi. Upstream structures include SpectralEmergence.of, which shows Q3 forces SU(3)xSU(2)xU(1), three generations, and 24 chiral flavors, and PhiForcingDerived.of, which encodes the underlying J-cost on the lattice.
proof idea
The proof is a one-line term-mode wrapper. It unfolds nu_corrected, rewrites the anomalous correction term to zero via the lemma anomalous_nu_correction_zero, and finishes with the ring tactic.
why it matters
This result confirms that the leading thermal eigenvalue phi (forced by T6 in the PhiForcing chain) remains unperturbed at zero anomaly, separating the base exponent from D-dependent corrections whose denominator originates in the Q3 multiplicity equaling the graph degree 3. It closes the base case for the corrected exponent in the thermal fixed-point operator. No immediate downstream uses are recorded, but the declaration supports the full derivation chain from phi-ladder to nu_0=1/phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.