thermal_eigenvalue_uniqueness
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.
claimIf $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 in Recognition Science
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.
scope and limits
- Does not establish existence of any root.
- Does not treat negative or zero values of r.
- Does not apply to other recurrences or polynomials.
- Does not derive the numerical value of phi itself.
- Does not address higher-order eigenvalues or full RG flow.
formal statement (Lean)
96theorem thermal_eigenvalue_uniqueness (r : ℝ) (hr : 0 < r)
97 (h : fibonacci_char_poly r = 0) : r = thermal_eigenvalue :=
proof body
Term-mode proof.
98 fibonacci_char_poly_unique_pos_root r hr h
99
100/-- The thermal eigenvalue satisfies the golden equation y² = y + 1. -/