fibonacci_char_poly_unique_pos_root
plain-language theorem explainer
Any positive real satisfying the Fibonacci characteristic equation x² - x - 1 = 0 equals the golden ratio φ. Researchers deriving thermal eigenvalues or correlation-length exponents on self-similar lattices cite this to anchor the growth rate along the φ-ladder. The proof unfolds the polynomial definition, recovers r² = r + 1 by linear arithmetic, and applies the phi_forced result.
Claim. If $r > 0$ and $r^2 - r - 1 = 0$, then $r = phi$, where $phi$ denotes the golden ratio.
background
The Thermal Fixed Point module treats φ as the forced thermal eigenvalue on the recognition lattice at a critical point. Self-similarity imposes the Fibonacci recurrence a(n+2) = a(n+1) + a(n) on thermal perturbations, whose characteristic polynomial is defined by x² - x - 1. The positive root of this polynomial fixes the growth rate per ladder step and therefore the leading correlation-length exponent ν₀ = 1/φ.
proof idea
Unfold the definition of fibonacci_char_poly at the hypothesis to obtain r² - r - 1 = 0. Linear arithmetic yields the equivalent relation r² = r + 1. The result follows by direct application of the phi_forced theorem from the PhiForcing module.
why it matters
This theorem supplies the uniqueness step that closes the chain from PhiForcing (T6 self-similarity) through the φ-ladder and Fibonacci cascade to the thermal eigenvalue y_t = φ. It is invoked by thermal_eigenvalue_uniqueness to exclude other positive reals and appears inside the thermalFixedPointCert certificate. The result confirms ν₀ = 1/φ in the eight-tick octave setting with D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.