fib_3
plain-language theorem explainer
The lemma states that the third term equals 3 under the module's Fibonacci definition with fib 0 =1 and fib 1=1. Researchers deriving the 45-gap from the eight-tick structure would cite this when evaluating small terms in the phi-related sequence. The proof is a direct reflexivity step after the recursive clause unfolds fib 3 as fib 1 plus fib 2.
Claim. Let $f : ℕ → ℕ$ satisfy $f(0)=1$, $f(1)=1$, and $f(n+2)=f(n)+f(n+1)$. Then $f(3)=3$.
background
The Gap45.Derivation module shows that 45 arises as (8+1)×5 from the eight-tick period forced by T8 together with the Fibonacci sequence tied to φ. The local fib definition begins at 1,1 rather than the conventional 0,1 indexing used in the RamanujanBridge modules for continued fractions and Zeckendorf J-cost. Upstream fib definitions supply the recurrence that this lemma evaluates at the concrete argument 3.
proof idea
The proof is a one-line wrapper that applies reflexivity after the recursive definition computes fib 3 as fib 1 + fib 2 = 1 + 2 = 3.
why it matters
The lemma supplies an elementary evaluation inside the derivation that 45 equals the ninth triangular number T(9) and factors as closure_factor 9 times Fibonacci factor 5. It supports the claim that 45 is forced by T8 plus the fence-post closure principle, which then combines with lcm(8,45)=360 to fix D=3 spatial dimensions. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.