thermal_eigenvalue_pos
plain-language theorem explainer
The theorem establishes positivity of the thermal eigenvalue at the recognition-lattice RG fixed point. Researchers deriving correlation-length exponents in three-dimensional critical phenomena would cite it to confirm the leading thermal direction yields a positive growth rate. The proof is a one-line wrapper applying the known positivity of the golden ratio.
Claim. $0 < y_t$, where $y_t = phi$ is the thermal eigenvalue of the recognition-lattice renormalization-group fixed point.
background
The module derives the thermal eigenvalue of the RG operator on the recognition lattice (Z^3 with unit cell Q_3). The phi-ladder supplies the unique geometric scaling sequence forced by self-similarity, so consecutive rungs obey the Fibonacci recurrence whose characteristic polynomial lambda^2 - lambda - 1 has unique positive root phi. The thermal eigenvalue is therefore identified with this root, giving the leading correlation-length exponent nu_0 = 1/phi. The upstream definition states: the thermal eigenvalue of the recognition-lattice RG fixed point, forced because the phi-ladder is the unique geometric scaling sequence and consecutive rungs satisfy the Fibonacci recurrence whose characteristic polynomial is lambda^2 - lambda - 1.
proof idea
The proof is a one-line wrapper that applies phi_pos.
why it matters
Positivity of the thermal eigenvalue is required to establish that the leading exponent nu_0 = 1/phi is positive and less than one. It is invoked directly by nu_leading_pos and nu_leading_lt_one, the latter confirming sub-mean-field behavior expected for D = 3. The result closes the derivation chain from PhiForcing (T6) through the phi-ladder and Fibonacci cascade to y_t = phi, consistent with the eight-tick octave and the forced spatial dimension D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.