fibonacci_char_poly
plain-language theorem explainer
The definition introduces the quadratic x² − x − 1 whose positive root encodes the asymptotic growth rate of the Fibonacci recurrence on the recognition lattice. Researchers deriving thermal eigenvalues or correlation-length exponents would cite it when connecting the phi-ladder to renormalization flow. It is supplied as the direct algebraic transcription of the recurrence a(n+2) = a(n+1) + a(n) forced by T6 self-similarity.
Claim. The characteristic polynomial of the recurrence $a_{n+2} = a_{n+1} + a_n$ is the quadratic $x^2 - x - 1$.
background
In the ThermalFixedPoint module the renormalization group operates along the phi-ladder at critical points of the recognition lattice Z³ with unit cell Q₃. T6 self-similarity forces the scaling sequence to obey the Fibonacci identity phi^{n+2} = phi^{n+1} + phi^n, whose characteristic equation is lambda² − lambda − 1. The module states that the unique positive root of this polynomial is phi, yielding the leading thermal eigenvalue y_t = phi and nu_0 = 1/phi.
proof idea
The declaration is a direct definition that transcribes the standard characteristic equation of the Fibonacci recurrence into Lean. No tactics or lemmas are invoked; the body consists of the explicit quadratic expression x² − x − 1.
why it matters
This definition supplies the polynomial whose root is identified with the thermal eigenvalue inside ThermalFixedPointCert. It completes the chain PhiForcing (T6) → phi-ladder → Fibonacci cascade → char poly → y_t = phi. The result anchors the eight-tick octave scaling and the D = 3 spatial dimensions through the spectral structure of Q₃. It leaves open the question of higher-order corrections to the eigenvalue beyond the leading phi term.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.