fib3_eq_2
plain-language theorem explainer
The theorem states that the third Fibonacci number equals 2, which Recognition Science equates with the spatial dimension D. Researchers assembling the phi-ladder identities and the eight-tick octave structure cite this when building the FibonacciCert record. The proof is a direct evaluation via the decide tactic on the standard recursive definition of the Fibonacci sequence.
Claim. $F_3 = 2$, 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 treats the Fibonacci sequence as intrinsic to Recognition Science through the golden ratio φ, with the key identity $F(n)φ + F(n-1) = φ^n$. Upstream definitions supply the recursive sequence: one variant starts 1,1,2,3,... while Nat.fib follows the standard 0,1,1,2,3,... . The local setting lists five canonical identities, including F(3)=2 and F(4)=3 both equal to D, plus F(6)=8 as the ledger period.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute the value directly from the recursive definition of Nat.fib.
why it matters
This identity supplies one field of the FibonacciCert record, which aggregates the values F(3)=2=D, F(4)=3=D, F(6)=8=2^D, and the recurrence. It fills the specific-value slot in the module's list of canonical identities and supports the forcing-chain step T8 that fixes D=3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.