thermal_eigenvalue
plain-language theorem explainer
The thermal eigenvalue of the recognition-lattice RG fixed point equals the golden ratio phi. Researchers computing the leading correlation-length exponent at critical points cite this definition when deriving nu_0. It follows directly as the unique positive root of the characteristic polynomial of the Fibonacci recurrence on the phi-ladder.
Claim. The thermal eigenvalue $y_t$ of the recognition-lattice renormalization-group fixed point equals the golden ratio $phi$.
background
The module examines the renormalization group at critical points on the recognition lattice, the integer lattice Z^3 with unit cell Q_3. The phi-ladder is the unique geometric scaling sequence forced by T6 self-similarity, satisfying the Fibonacci identity phi^{n+2} = phi^{n+1} + phi^n. This identity forces thermal perturbations to obey the recurrence a(n+2) = a(n+1) + a(n), whose characteristic polynomial lambda^2 - lambda - 1 has phi as its unique positive root.
proof idea
The declaration is a one-line definition that assigns the thermal eigenvalue directly to phi. It rests on the upstream uniqueness result that phi is the sole positive root of the Fibonacci characteristic polynomial.
why it matters
This definition supplies the thermal eigenvalue y_t that feeds the leading-order correlation-length exponent via nu_leading, defined as 1 over the thermal eigenvalue. It fills the step in the derivation chain from PhiForcing (T6) through the phi-ladder and Fibonacci cascade to the thermal eigenvalue, as stated in the module documentation. The placement supports the forced value nu_0 = 1/phi and connects to the broader forcing chain landmarks T0 to T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.