fib4_eq_3
plain-language theorem explainer
Establishes that the fourth Fibonacci number equals 3, matching the spatial dimension D in Recognition Science. Researchers verifying phi-ladder identities and the FibonacciCert structure would cite this for the canonical value F(4)=3. The proof is a one-line wrapper applying the decide tactic to the recursive definition of fib.
Claim. $F_4 = 3$, where $F_n$ is the Fibonacci sequence with $F_0 = 0$, $F_1 = 1$, and $F_{n+2} = F_{n+1} + F_n$.
background
The module derives specific Fibonacci values intrinsic to Recognition Science via the golden ratio phi, with the key identity $F(n) phi + F(n-1) = phi^n$. Upstream definitions supply the recursive sequence: one starts fib 0 = 1, fib 1 = 1; another fib 0 = 0, fib 1 = 1; and an abbreviation to Nat.fib. The local setting lists five canonical identities, including F(4)=3=D and F(6)=8=2^D, all proved by decide with zero sorrys.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the recursive definition of Nat.fib at argument 4.
why it matters
This supplies the fib4 field in the downstream FibonacciCert definition, which aggregates F(3)=2, F(4)=3, F(6)=8, the 2^D relation, and the recurrence. It fills one of the five canonical identities in the module, supporting the framework's derivation of Fibonacci numbers from phi and tying into the eight-tick octave (T7) and D=3 (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.