fib
plain-language theorem explainer
Standard Fibonacci sequence with F(0)=0, F(1)=1 and the usual two-step recurrence. It is the counting backbone for the two-letter Fibonacci substitution system in this module, and is cited wherever word lengths or true/false symbol counts must match Fibonacci numbers. The body is a plain recursive definition, not a theorem.
Claim. Define the Fibonacci sequence $F:\mathbb{N}\to\mathbb{N}$ by $F(0)=0$, $F(1)=1$, and $F(n+2)=F(n+1)+F(n)$ for all $n\in\mathbb{N}$.
background
The module studies a two-letter substitution system whose symbol counts obey Fibonacci recurrences. In that setting one needs an explicit integer sequence $F(n)$ so that lengths of iterated substitution words, and the numbers of each letter, can be identified with Fibonacci numbers.
This definition uses the classical indexing $F(0)=0$, $F(1)=1$. A sibling definition in Gap45.Derivation uses the shifted seed $F(0)=1$, $F(1)=1$; both satisfy the same recurrence and differ only by a unit shift of the index. Downstream cosmology lemmas often invoke Mathlib's Nat.fib, which matches this $F(0)=0$ convention, via the closed identity $\varphi^{n+1}=F_{n+1}\varphi+F_n$.
proof idea
There is no proof: the declaration is a recursive definition by pattern match on $0$, $1$, and $n+2$. The two base cases and the additive step are given directly; no lemmas are applied.
why it matters
Locally it feeds the Fibonacci substitution maps and the true/false counting lemmas in this module, so that substitution word lengths are exactly Fibonacci numbers. Downstream it supports Gap45 base facts (fib_0 through fib_4 and related) and the cosmology certificates phi_pow_fib and phi_pow_44_fib, which rewrite powers of $\varphi$ as integer linear forms $F_{n+1}\varphi+F_n$. Those identities sit on the $\varphi$-ladder used for mass and cosmological interval bounds in Recognition Science (T6 forces $\varphi$ as the self-similar fixed point). The definition itself closes no open question; it is shared infrastructure for count identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.