thermal_eigenvalue_uniqueness
plain-language theorem explainer
Any positive real root of the equation x² - x - 1 = 0 must equal the thermal eigenvalue φ. Researchers deriving the correlation-length exponent ν₀ = 1/φ from renormalization on the recognition lattice cite this to fix the leading growth rate per φ-ladder step. The argument is a direct one-line application of the uniqueness result for the positive root of the Fibonacci characteristic polynomial.
Claim. If $r > 0$ and $r^2 - r - 1 = 0$, then $r = phi$, where $phi$ is the thermal eigenvalue of the recognition-lattice RG fixed point.
background
The module treats the thermal fixed-point operator at critical points on the recognition lattice ℤ³. The φ-ladder is the unique geometric scaling sequence forced by self-similarity, so consecutive rungs obey the Fibonacci recurrence whose characteristic polynomial is λ² − λ − 1. The thermal eigenvalue is defined as this positive root phi, which sets the leading growth rate and the exponent ν₀ = 1/phi.
proof idea
The proof is a one-line wrapper that applies fibonacci_char_poly_unique_pos_root to the hypothesis fibonacci_char_poly r = 0 together with r > 0. That upstream theorem unfolds the polynomial, obtains r² = r + 1, and invokes phi_forced from the PhiForcing foundation to conclude r = phi, matching the definition of thermal_eigenvalue.
why it matters
The result closes the uniqueness leg of the derivation chain PhiForcing (T6) → φ-ladder → Fibonacci cascade → char poly λ² − λ − 1 = 0 → unique positive root = phi (thermal eigenvalue). It guarantees that the thermal growth rate per ladder step is unambiguously phi and therefore that ν₀ = 1/phi is fixed. The declaration sits inside the ThermalFixedPoint module and supports sibling statements such as thermal_eigenvalue_eq_phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.