fib
plain-language theorem explainer
The fib abbreviation supplies the standard Fibonacci sequence for Zeckendorf representations interpreted as J-cost stable sums on the phi-ladder. Cosmologists deriving phi-power identities for eta_B bounds and cross-domain analysts verifying cardinality spectra cite this definition. It is a one-line alias to the Mathlib Nat.fib implementation that inherits the recurrence without further obligations.
Claim. Let $F : ℕ → ℕ$ denote the Fibonacci sequence satisfying $F(0) = 0$, $F(1) = 1$, and $F(n+2) = F(n+1) + F(n)$ for all $n ≥ 0$.
background
The module interprets Zeckendorf's theorem as the statement that every positive integer admits a unique representation as a sum of non-consecutive Fibonacci numbers, which is exactly the J-cost admissible configuration on the phi-ladder. J-cost is the function $J(x) = (x + x^{-1})/2 - 1$ (equivalently cosh(log x) - 1) that quantifies instability under the Recognition Composition Law. The phi-ladder consists of rungs at successive integer powers of the golden ratio phi, the self-similar fixed point forced in the unified chain. Upstream results supply the recurrence: Gap45.Derivation.fib starts 1,1,2,3,... while ContinuedFractionPhi.fib starts 0,1,1,2,...; the present alias adopts the Mathlib convention used throughout the cosmology derivations.
proof idea
This declaration is a one-line wrapper aliasing Mathlib's Nat.fib. No tactics or additional lemmas are invoked beyond the library definition.
why it matters
The abbreviation supplies the integer sequence underlying all phi-ladder mass and cardinality formulas. It feeds parent theorems such as phi_pow_fib (phi^{n+1} = F(n+1) phi + F(n)) and the numerical bounds phi^44 > 1.5e9, phi^44 < 1.6e9 that place the predicted eta_B within 4.5 percent of observation. It realizes the classical Fibonacci sequence as the discrete skeleton of the phi-ladder positions required by T6 and the J-uniqueness step of the forcing chain, enabling the later stability results zeckendorf_is_Jcost_stable and fibonacci_lattice_is_complete.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.