fib8_eq_21
plain-language theorem explainer
The eighth Fibonacci number equals 21 under standard indexing with F_0 = 0. Researchers verifying the Recognition Science embedding of the Fibonacci sequence via the golden ratio would cite this identity when checking phi-ladder values. The proof evaluates the recursive definition directly with a decision procedure.
Claim. The eighth Fibonacci number satisfies $F_8 = 21$, where the sequence is defined by $F_0 = 0$, $F_1 = 1$, and $F_n = F_{n-1} + F_{n-2}$ for $n > 1$.
background
The module establishes that the Fibonacci sequence arises intrinsically in Recognition Science through the golden ratio φ, with the key identity F(n) φ + F(n-1) = φ^n. Specific values are proved by direct computation, including F(3) = 2 = D and F(6) = 8 = 2^D. Upstream results supply multiple fib definitions: one recursive version starting at 1,1,2,... and the standard Nat.fib used here, which begins 0,1,1,2,3,5,8,13,21.
proof idea
This is a one-line wrapper that applies the decide tactic to evaluate the recursive definition of Nat.fib at argument 8 and confirm equality to 21.
why it matters
The identity completes one entry in the list of canonical Fibonacci values required by the RS framework, aligning with the eight-tick octave and D = 3 from the forcing chain T5-T8. It supports the phi-ladder characterisation without invoking the Recognition Composition Law directly. No downstream theorems depend on it yet, and the module reports zero sorry statements across all such identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.