fib_recurrence_8
plain-language theorem explainer
The theorem confirms the Fibonacci recurrence holds at index 8, with F(8) = 21 equaling F(7) + F(6) = 13 + 8. Recognition Science derivations that tie the sequence to phi and spatial dimension D would cite this concrete check when assembling certificates. The proof is a direct decide tactic that evaluates both sides via the Nat.fib definition.
Claim. $F_8 = F_7 + F_6$ where $F_n$ is the Fibonacci sequence with $F_0=0$, $F_1=1$.
background
The Fibonacci sequence enters Recognition Science through its link to the golden ratio phi, satisfying the identity F(n) phi + F(n-1) = phi^n. Upstream definitions supply the recurrence F(n+2) = F(n+1) + F(n), with variants starting at (1,1) or (0,1) that all reduce to the standard Nat.fib. The module records canonical values such as F(3)=2=D and F(6)=8=2^D, each verified by decide.
proof idea
One-line wrapper that applies the decide tactic to unfold Nat.fib on both sides and compare the resulting numerals.
why it matters
The result populates the recurrence field of fibonacciCert, which aggregates specific Fibonacci identities for use in higher RS constructions. It supplies the general recurrence identity at a concrete point in the chain that runs from J-uniqueness through the phi fixed point to D=3 and the eight-tick octave. No open scaffolding remains for this identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.