fib_4
The lemma asserts that the fourth term in the Fibonacci sequence equals five. Researchers deriving the 45-gap from the eight-tick structure cite it to obtain the Fibonacci factor in the factorization 45 = 9 × 5. The proof reduces immediately to reflexivity once the recursive definition is unfolded.
claimLet $F_n$ be the Fibonacci sequence with $F_0 = 1$, $F_1 = 1$, and $F_{n+2} = F_n + F_{n+1}$ for $n ≥ 0$. Then $F_4 = 5$.
background
The Fibonacci sequence is defined recursively in Gap45.Derivation as fib 0 = 1, fib 1 = 1, and fib (n+2) = fib n + fib (n+1). This indexing produces the sequence 1, 1, 2, 3, 5, 8, .... The module derives 45 from the eight-tick period (T8) combined with Fibonacci numbers, specifically via the identity 45 = (8 + 1) × 5 where 5 is the term at index 4. Upstream Fibonacci definitions appear in ContinuedFractionPhi (standard F0=0, F1=1) and ZeckendorfJCost (Nat.fib alias), supplying the sequence for related phi and J-cost calculations.
proof idea
The proof is a one-line wrapper that applies reflexivity after the recursive definition of fib is unfolded to n=4.
why it matters in Recognition Science
This lemma supplies the concrete value 5 required for the factorization 45 = 9 × 5 that expresses the gap. It feeds the claim that 45 arises from closure of the eight-tick cycle (T7) plus cumulative phase T(9), and supports the downstream forcing of D = 3 via lcm(8, 45) = 360. The result closes a small computational step in the T0–T8 chain without introducing new hypotheses.
scope and limits
- Does not prove the full 45-gap derivation or its physical motivation.
- Does not compute properties of higher Fibonacci terms.
- Does not connect to J-cost, defect distance, or mass ladder formulas.
- Does not address constants such as alpha inverse or G in RS units.
formal statement (Lean)
58@[simp] lemma fib_4 : fib 4 = 5 := rfl