phi_pow_fib
plain-language theorem explainer
The universal Fibonacci-phi identity asserts that for every natural number n, phi raised to n plus two equals the (n+2)th Fibonacci number times phi plus the (n+1)th Fibonacci number. Cross-domain modules cite this to convert exponential bounds on phi into arithmetic statements about Fibonacci numbers for results such as phi^44 expansions. The proof is by induction on n, with the base case using the quadratic relation for phi and the inductive step combining the geometric recurrence for phi with the additive recurrence for Fibonacci numbers.
Claim. For all natural numbers $n$, $phi^{n+2} = F_{n+2} phi + F_{n+1}$, where $F_k$ denotes the $k$th Fibonacci number with $F_0=0$, $F_1=1$, and $phi$ satisfies $phi^2 = phi + 1$.
background
In the CrossDomain.FibonacciPhiUniversality module the Fibonacci-phi identity is presented as a universal certificate that reduces any high power of phi to a linear expression in phi. The golden ratio phi satisfies the quadratic equation phi^2 = phi + 1, while the Fibonacci sequence obeys the recurrence F_{k+2} = F_{k+1} + F_k with the standard indexing F_0 = 0, F_1 = 1. Upstream, the similar identity in Cosmology.EtaBPrefactorDerivation states phi^(n+1) = F(n+1) phi + F(n) and is proved by the same inductive pattern.
proof idea
The proof proceeds by induction on n. The base case n=0 rewrites phi^2 using the phi_sq relation and applies ring after casting. The inductive step rewrites the left side as phi^(k+3) = phi^(k+2) * phi, substitutes the inductive hypothesis, invokes phi^2 = phi + 1, applies the Fibonacci recurrence Nat.fib_add_two to update coefficients, and closes with nlinarith.
why it matters
This theorem supplies the core identity used by phi_pow_44_fib to obtain the explicit expansion phi^44 = 701408733 phi + 433494437 for the baryon asymmetry calculation. It also feeds directly into the fibonacciPhiCert definition and the phi_pow_bounded_by_fib corollary. In the Recognition framework it realizes the mechanism for reducing high powers of phi to linear forms, supporting bounds such as phi^8 > 46 and phi^44 > 10^8 that appear in the eight-tick octave and mass-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.