fib
plain-language theorem explainer
The Fibonacci sequence is defined recursively with base cases 1 and 1 followed by the standard addition recurrence. Cosmologists deriving phi^44 bounds for the baryon-to-photon ratio and cross-domain cardinality results cite this variant when applying the Fibonacci-phi identity. The definition is supplied as a direct pattern-matching specification on natural numbers with no lemmas or tactics.
Claim. The function $f : ℕ → ℕ$ is defined by $f(0) = 1$, $f(1) = 1$, and $f(n+2) = f(n) + f(n+1)$ for $n ≥ 0$.
background
The Gap45.Derivation module shows that 45 arises as (8+1) × 5 from the eight-tick period (T8) combined with the Fibonacci sequence tied to phi. The module document states that 45 equals the ninth triangular number T(9), representing cumulative phase accumulation over a closed 8-tick cycle plus closure, and notes that lcm(8,45)=360 forces D=3 spatial dimensions. This local definition begins at 1,1 rather than the conventional 0,1 to align with phi-ladder computations.
proof idea
The definition is introduced directly by pattern matching on the input natural number, with explicit base cases at 0 and 1 both returning 1 and the standard recurrence for the successor case. No upstream lemmas are invoked and no tactics are used; it is a pure recursive specification.
why it matters
This definition supplies the Fibonacci factor required by the parent results phi_pow_44_fib and phi_pow_fib_succ in EtaBPrefactorDerivation and the numerical bounds phi_pow_44_gt_1pt5e9, phi_pow_44_lt_1pt6e9 in MatterAntimatter that place phi^44 near the observed eta_B. It completes the 45 = 9 × 5 factorization in the module document, linking T8 eight-tick closure to the phi self-similar fixed point (T6) and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.