fibonacci_char_poly_root
plain-language theorem explainer
φ satisfies the characteristic equation λ² − λ − 1 of the Fibonacci recurrence. Researchers deriving renormalization flows on the recognition lattice cite this to fix the thermal eigenvalue y_t = φ and the exponent ν₀ = 1/φ. The proof is a one-line term reduction that unfolds the polynomial and applies linear arithmetic to the quadratic identity φ² = φ + 1.
Claim. The golden ratio φ satisfies φ² − φ − 1 = 0, the characteristic polynomial of the recurrence a(n+2) = a(n+1) + a(n) forced by the φ-ladder.
background
In the ThermalFixedPoint module the renormalization group acts on the recognition lattice ℤ³ at critical points. The φ-ladder is the unique geometric scaling sequence forced by self-similarity (T6). The Fibonacci identity φ^{n+2} = φ^{n+1} + φ^n implies that thermal perturbations obey the linear recurrence a(n+2) = a(n+1) + a(n), whose characteristic polynomial is λ² − λ − 1. Upstream phi_sq_eq supplies the identity φ² = φ + 1 that closes the algebra.
proof idea
The proof is a term-mode wrapper. It unfolds fibonacci_char_poly to the expression φ² − φ − 1 and invokes linarith on the hypothesis phi_sq_eq : φ² = φ + 1.
why it matters
This supplies the char_poly_root field of thermalFixedPointCert, which certifies the thermal fixed point. It completes the chain PhiForcing (T6) → φ-ladder → Fibonacci cascade → thermal eigenvalue y_t = φ, thereby fixing the leading correlation-length exponent ν₀ = 1/φ on the eight-tick octave lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.