nu_leading_pos
plain-language theorem explainer
The leading correlation-length exponent is shown strictly positive. Renormalization-group analyses in three-dimensional critical phenomena would cite this to confirm the thermal direction remains relevant. The proof is a one-line term application of positivity preservation under division by a positive thermal eigenvalue.
Claim. $0 < nu_0$ where $nu_0 := 1/y_t$ is the leading correlation-length exponent and $y_t$ denotes the thermal eigenvalue.
background
The module treats the thermal fixed-point operator on the recognition lattice at critical points, where the renormalization group acts along the phi-ladder. Self-similarity forces the thermal perturbation to obey the Fibonacci recurrence whose characteristic polynomial has unique positive root phi, yielding thermal eigenvalue y_t equal to phi and therefore nu_0 equal to 1/phi. The local definition sets nu_leading to the reciprocal of the thermal eigenvalue, with its positivity following directly from the positivity of that eigenvalue.
proof idea
Term-mode one-liner that applies the division-positivity lemma to the constant 1 and to the already-established positivity of the thermal eigenvalue.
why it matters
The result confirms the expected sub-mean-field character of the thermal exponent in D = 3, closing the positivity step in the derivation chain from PhiForcing through the phi-ladder to the correlation-length divergence. It supplies the sign information required for any downstream RG flow analysis that invokes the thermal fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.