anomalous_nu_correction_zero
plain-language theorem explainer
The anomalous correction to the correlation-length exponent vanishes at zero deviation from the fixed point. Researchers analyzing renormalization flows on the recognition lattice cite this to confirm that the leading exponent equals 1/φ with no additive term at the critical point. The proof is a one-line wrapper that unfolds the correction definition and simplifies directly to zero.
Claim. For any real $D$, the anomalous correction to the correlation-length exponent vanishes at zero deviation: if $ν_{anom}(D,η)$ denotes this correction term, then $ν_{anom}(D,0)=0$.
background
The module treats the thermal fixed-point operator on the recognition lattice, where the φ-ladder arises from self-similarity (T6) and the Fibonacci recurrence whose characteristic polynomial λ²−λ−1 has unique positive root φ. This forces the thermal eigenvalue y_t=φ and the leading correlation-length exponent ν₀=1/φ. The anomalous correction is defined to capture the first-order response to a small deviation parameter η from this fixed point, with the module doc noting that the correction rate at leading order is 1/D per unit η.
proof idea
The proof is a one-line wrapper that unfolds the definition of the anomalous correction and applies simplification to obtain zero at η=0.
why it matters
This theorem is invoked by nu_corrected_at_zero to recover the leading exponent exactly at zero deviation. It closes the renormalization analysis at the critical point, consistent with the φ-ladder forced by T6 and the structural requirement that D=3 from T8 and the Q₃ spectral-gap multiplicity. The downstream doc-comment notes that this multiplicity equals the graph degree D=3, which is why D appears in the denominator of the correction rate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.