fib
plain-language theorem explainer
The Fibonacci sequence is defined by F(0)=0, F(1)=1 and the recurrence F(n+2)=F(n+1)+F(n). Number theorists and cosmologists working on phi-ladder identities cite this definition when converting powers of the golden ratio into integer coefficients for mass formulas and eta_B bounds. The implementation is the direct recursive definition with no auxiliary lemmas or tactics.
Claim. The Fibonacci sequence satisfies $F_0=0$, $F_1=1$, and $F_{n+2}=F_{n+1}+F_n$ for all $n$ in the natural numbers.
background
The module treats continued fractions as sequential J-cost optimizations on the positive reals. The J-cost functional is $J(x)=½(x+x^{-1})-1$, which is strictly convex with unique minimum at $x=1$ and self-similar fixed point at φ. The infinite continued fraction for φ therefore generates the Fibonacci recurrence through the relation x=1+1/x. Upstream results supply equivalent Fibonacci definitions: one in Gap45.Derivation starting at 1,1 and one in ZeckendorfJCost as an abbreviation for Nat.fib.
proof idea
This is the direct recursive definition of the Fibonacci sequence. No lemmas are invoked and no tactics are applied; the three cases implement the classical recurrence exactly.
why it matters
The definition supplies the integer coefficients for the identity φ^{n+1}=F_{n+1}φ+F_n used in EtaBPrefactorDerivation.phi_pow_fib and MatterAntimatter.phi_pow_44_gt_1pt5e9, which bound φ^44 to obtain the RS prediction η_B≈φ^{-44}. It anchors the phi-ladder rungs that appear in cardinality spectra and mass formulas, consistent with the self-similar fixed point (T6) and eight-tick octave (T7) of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.