fib5_eq_5
plain-language theorem explainer
The fifth Fibonacci number equals five. A researcher verifying base cases for the phi-ladder and dimensional identifications in Recognition Science would cite this equality when anchoring specific values such as F(4) = 3 for spatial dimension. The proof is a direct decision procedure that evaluates the recursive definition at index 5.
Claim. $F_5 = 5$, where $F_n$ is the Fibonacci sequence defined by the recurrence $F_0 = 0$, $F_1 = 1$, $F_{n+2} = F_{n+1} + F_n$.
background
The module shows that the Fibonacci sequence is intrinsic to Recognition Science through the golden ratio φ, with the key identity $F(n)φ + F(n-1) = φ^n$ and specific values such as $F(3) = 2 = D$ and $F(6) = 8 = 2^D$. Upstream definitions supply the sequence via the standard recurrence (starting at 0,1 or 1,1) or as an abbreviation for the library version. The local setting lists five canonical identities, all established by direct evaluation, with zero sorry statements.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the recursive definition of the Fibonacci sequence at index 5.
why it matters
This equality belongs to the set of base cases that anchor Fibonacci numbers to the Recognition Science framework via φ, supporting identifications such as D = 3 from F(4) and the eight-tick octave period from F(6) = 8. It fills one of the five canonical identities listed in the module documentation. No downstream uses appear in the graph, but the result participates in the chain from the forcing steps T5–T8 to concrete numerical checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.