anomalous_nu_correction_small
plain-language theorem explainer
The inequality bounds the anomalous correction η/(D + η) to the thermal eigenvalue by η/D for D > 0 and η ≥ 0. Lattice renormalization-group analysts estimating shifts to the correlation-length exponent near critical points would cite this leading-order control. The proof unfolds the definition, splits on the sign of η, and closes the positive case with a division lemma plus linear arithmetic.
Claim. $ 0 < D, 0 ≤ η ⇒ η/(D + η) ≤ η/D $
background
The module treats the thermal fixed point on the recognition lattice (ℤ³ with unit cell Q₃). Self-similarity forces the φ-ladder via the Fibonacci recurrence whose characteristic polynomial has unique positive root φ, yielding the bare thermal eigenvalue y_t = φ and ν₀ = 1/φ. The upstream definition supplies the correction: “The anomalous correction to ν on a D-dimensional lattice. When the anomalous dimension η ≠ 0, the thermal direction couples to the D field modes at the Q₃ spectral gap (multiplicity D). The correction η/(D + η) is the unique simplest (Padé [0/1]) rational function satisfying f(0) = 0 and f'(0) = 1/D.”
proof idea
Unfold the definition of the anomalous correction. Establish positivity of D + η and D ≠ 0. Case on η = 0 (immediate simplification) or η > 0. Rewrite the target inequality via the division lemma div_le_div_iff₀ and discharge the resulting arithmetic statement with nlinarith.
why it matters
The bound supplies an explicit control on the size of η-induced shifts to ν at the thermal fixed point. It supports estimates along the φ-ladder forced by T6 and the D = 3 spatial dimensions of T8 when small anomalous dimensions appear. No downstream theorems are recorded, but the result directly implements the “for small η” statement in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.