anomalous_nu_correction
The definition supplies the rational correction η/(D + η) to the leading correlation-length exponent on a D-dimensional lattice when the anomalous dimension η is nonzero. Researchers refining critical exponents in the Recognition Science framework cite it to adjust ν₀ = 1/φ for lattice effects at the Q₃ spectral gap. It is realized as the direct Padé [0/1] expression chosen to meet the boundary conditions f(0) = 0 and f'(0) = 1/D.
claimThe anomalous correction to the correlation-length exponent is given by $f(D,η) = η/(D + η)$, where $D$ is the lattice dimension and $η$ is the anomalous dimension.
background
The module derives the thermal fixed point from the phi-ladder forced by T6 self-similarity. The Fibonacci recurrence on the ladder has characteristic polynomial λ² − λ − 1 = 0 whose unique positive root is φ, yielding the leading thermal eigenvalue y_t = φ and thus the bare exponent ν₀ = 1/φ (see MODULE_DOC derivation chain). On the Q₃ lattice the spectral gap has multiplicity D, so a nonzero anomalous dimension η couples the thermal direction to these D modes. The correction is the simplest rational function satisfying the two conditions stated in the doc-comment: vanishing at η = 0 and initial slope 1/D.
proof idea
The declaration is a one-line definition that directly returns the rational expression η / (D + η). No lemmas are applied; the body encodes the Padé [0/1] approximant described in the documentation.
why it matters in Recognition Science
This supplies the additive correction term inside the downstream definition nu_corrected, which produces the full exponent ν = ν₀ + η/(D + η). It thereby incorporates anomalous-dimension effects into the thermal fixed-point analysis while remaining consistent with T6 (phi uniqueness) and T8 (D = 3). The sibling theorems anomalous_nu_correction_zero and anomalous_nu_correction_small establish the required limits f(0) = 0 and f'(0) = 1/D, supporting renormalization-group flow along the phi-ladder. It leaves open the microscopic origin of η itself.
scope and limits
- Does not derive the numerical value of η from the recognition lattice.
- Does not prove the rational form is exact rather than an effective approximation.
- Does not include higher-order terms in the expansion in η.
- Does not apply when the spectral-gap multiplicity differs from D.
Lean usage
def nu_corrected (D η : ℝ) : ℝ := nu_leading + anomalous_nu_correction D ηformal statement (Lean)
139def anomalous_nu_correction (D η : ℝ) : ℝ := η / (D + η)
proof body
Definition body.
140