fib6_eq_2cubeD
plain-language theorem explainer
F(6) equals 8, which coincides with 2 raised to the spatial dimension D. Recognition Science workers cite this identity when confirming that the ledger period matches the sixth Fibonacci entry in the phi-ladder. The proof is a direct numerical check performed by the decide tactic on the standard Fibonacci recurrence.
Claim. $F_6 = 8 = 2^3$, where $F_n$ denotes the Fibonacci sequence with the recurrence $F_{n+2} = F_{n+1} + F_n$ and initial values matching the RS-native definition.
background
The module establishes that the Fibonacci sequence arises intrinsically from the golden ratio phi in Recognition Science. The key relation is $F(n) phi + F(n-1) = phi^n$, and the listed identities include $F(3)=2=D$, $F(4)=3=D$, and $F(6)=8=2^D$ as the ledger period. Upstream definitions supply the recursive fib function in Gap45.Derivation (starting 1,1,2,3,...) and in RamanujanBridge variants (starting 0,1,1,2,...), together with the gap function F(Z) = log(1 + Z/phi)/log(phi) that links to the same phi-ladder.
proof idea
One-line wrapper that applies the decide tactic to evaluate Nat.fib 6 directly against 2^3.
why it matters
The result supplies the fib6_2cubeD field inside the FibonacciCert structure, which aggregates the canonical identities F(3)=2, F(4)=3, F(6)=8 and the recurrence at step 8. It anchors the eight-tick octave (T7) where the period is 2^3 and D=3 spatial dimensions (T8), closing the numerical verification that the ledger period equals the sixth Fibonacci number in RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.