thermal_eigenvalue_relevant
plain-language theorem explainer
The thermal eigenvalue y_t exceeds 1, confirming the thermal perturbation is relevant rather than marginal at the critical point on the recognition lattice. RG theorists in Recognition Science cite this to establish divergence of the correlation length via nu_0 = 1/y_t. The proof is a one-line wrapper applying the lemma one_lt_phi.
Claim. $y_t > 1$, where $y_t$ is the leading thermal eigenvalue on the phi-ladder.
background
The module derives the thermal fixed point from T6 self-similarity, which forces the phi-ladder via the Fibonacci recurrence whose characteristic polynomial has unique positive root phi. The thermal eigenvalue is therefore identified with phi, so y_t = phi and the correlation-length exponent satisfies nu_0 = 1/phi. Upstream results include one_lt_phi (Constants) establishing the base inequality and PhiForcingDerived.of together with SpectralEmergence.of supplying the ladder construction.
proof idea
One-line wrapper that applies one_lt_phi from Constants.
why it matters
Feeds directly into nu_leading_lt_one, which concludes nu_0 < 1 for D = 3. It completes the chain step from PhiForcing (T6) through the Fibonacci characteristic polynomial to y_t > 1, closing the leading-order relevance argument before anomalous-dimension corrections are considered.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.