fib6_eq_8
plain-language theorem explainer
The sixth Fibonacci number equals 8. Recognition Science researchers cite this to confirm the ledger period equals 2^D for spatial dimension D=3. The equality is one of five canonical values tied to the phi characterization of the sequence. The proof is a direct computational verification.
Claim. $F_6 = 8$ where $F_n$ denotes the $n$th Fibonacci number.
background
The Fibonacci sequence is intrinsic to Recognition Science through the golden ratio phi, satisfying the identity $F(n) phi + F(n-1) = phi^n$. The module records five specific values proved by direct computation, including $F(3)=2$, $F(4)=3$, and $F(6)=8$ identified as the ledger period $2^D$. Upstream modules supply the recursive definition of the sequence, either starting at 0,1 or 1,1, with the standard recurrence used for the computation here.
proof idea
The declaration is a one-line wrapper that applies the decide tactic to evaluate both sides of the equality by direct computation of the Fibonacci recurrence.
why it matters
This supplies the fib6 field inside the FibonacciCert structure that aggregates canonical values for the RS mathematics layer. It corresponds to the eight-tick octave landmark (period $2^3$) in the forcing chain T7 and reinforces the link between Fibonacci numbers and the spatial dimension D=3. The result closes one of the concrete numerical checks required before the phi-ladder mass formula can be applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.