fibonacci_char_poly_unique_pos_root
The unique positive real root of the equation x² − x − 1 = 0 is the golden ratio φ. Researchers fixing the thermal eigenvalue and correlation-length exponent on the recognition lattice cite this result to close the Fibonacci cascade step. The tactic proof unfolds the characteristic polynomial to recover the quadratic constraint r² = r + 1 and applies the phi_forced theorem.
claimIf $r > 0$ satisfies $r^2 - r - 1 = 0$, then $r = phi$.
background
The ThermalFixedPoint module treats renormalization-group flow at critical points on the ℤ³ lattice with unit cell Q₃. Self-similarity (T6) forces the φ-ladder, so thermal perturbations obey the Fibonacci recurrence a(n+2) = a(n+1) + a(n) whose characteristic polynomial is defined by fibonacci_char_poly(x) := x² − x − 1. The upstream phi_forced theorem states that any positive real obeying the compositional constraint r² = r + 1 equals φ.
proof idea
Unfold fibonacci_char_poly at the hypothesis to obtain r² = r + 1 by linarith. Apply the phi_forced theorem from PhiForcing, supplying the positivity assumption and the recovered quadratic equation.
why it matters in Recognition Science
This pins the thermal eigenvalue at φ and feeds directly into phi_ladder_growth, thermal_eigenvalue_uniqueness, and thermalFixedPointCert. It realizes the derivation-chain step “unique positive root = φ (PhiForcing)” that converts T6 into the thermal growth rate y_t = φ and ν₀ = 1/φ.
scope and limits
- Does not prove existence of any root.
- Does not characterize the negative root.
- Does not apply for r ≤ 0.
- Does not derive the Fibonacci recurrence from the lattice.
Lean usage
theorem thermal_eigenvalue_uniqueness (r : ℝ) (hr : 0 < r) (h : fibonacci_char_poly r = 0) : r = thermal_eigenvalue := fibonacci_char_poly_unique_pos_root r hr hformal statement (Lean)
55theorem fibonacci_char_poly_unique_pos_root (r : ℝ) (hr : 0 < r)
56 (h : fibonacci_char_poly r = 0) : r = phi := by
proof body
Tactic-mode proof.
57 unfold fibonacci_char_poly at h
58 have : r ^ 2 = r + 1 := by linarith
59 exact IndisputableMonolith.Foundation.PhiForcing.phi_forced r hr this
60
61/-! ## 2. The Fibonacci Cascade on the φ-Ladder -/
62
63/-- The φ-ladder satisfies the Fibonacci recurrence (natural exponents). -/