nu_leading_lt_one
plain-language theorem explainer
The leading thermal eigenvalue satisfies ν₀ < 1. Researchers studying renormalization-group flows on three-dimensional lattices cite this to confirm sub-mean-field scaling. The proof rewrites the definition of ν₀ as a ratio and applies the positivity and relevance of the thermal eigenvalue.
Claim. Let ν₀ = 1/y_t be the leading correlation-length exponent with y_t the thermal eigenvalue forced by the φ-ladder. Then ν₀ < 1.
background
The module derives the thermal fixed-point operator on the recognition lattice ℤ³ with unit cell Q₃. The φ-ladder is the geometric scaling sequence forced by T6 self-similarity; the Fibonacci recurrence a(n+2) = a(n+1) + a(n) yields the characteristic polynomial λ² − λ − 1 = 0 whose unique positive root is φ, so the thermal growth rate y_t equals φ and ν₀ = 1/φ. Upstream results establish the positivity and relevance of this eigenvalue together with the spatial dimension D = 3.
proof idea
This is a term-mode proof. It rewrites the definition of the leading exponent and invokes the lemma that a positive ratio is less than one when the numerator is relevant, then applies the relevance property of the thermal eigenvalue.
why it matters
This theorem closes the leading-order derivation of the thermal exponent from the forcing chain T6. It precedes the treatment of anomalous-dimension corrections η/(D + η) on the Q₃ lattice. The result aligns with the expectation that ν₀ < 1 for three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.