fibonacciCert
plain-language theorem explainer
The fibonacciCert definition packages five exact Fibonacci identities that Recognition Science derives from the phi fixed point. Researchers working on the phi-ladder or ledger periodicity would cite the bundle when they need F(3) = 2, F(4) = 3, F(6) = 8 = 2^3 and the step-8 recurrence in one place. It is assembled as a direct structure literal that references five independently decided equalities.
Claim. A structure asserting the identities $F(3)=2$, $F(4)=3$, $F(6)=8$, $F(6)=2^3$ and $F(8)=F(7)+F(6)$, where $F(n)$ is the $n$th Fibonacci number.
background
Recognition Science obtains the Fibonacci sequence from the self-similar fixed point φ via the identity $F(n)φ + F(n-1) = φ^n$. The module records that specific terms coincide with the spatial dimension and the eight-tick ledger period: $F(3)=2=D$, $F(4)=3=D$ and $F(6)=8=2^D$. The structure FibonacciCert collects these five canonical identities into a single reference object. It rests on the upstream theorems fib3_eq_2, fib4_eq_3, fib6_eq_8, fib6_eq_2cubeD and fib_recurrence_8, each obtained by direct computation.
proof idea
The definition constructs an instance of FibonacciCert by assigning each field to the corresponding decided theorem: fib3 to fib3_eq_2, fib4 to fib4_eq_3, fib6 to fib6_eq_8, fib6_2cubeD to fib6_eq_2cubeD and recurrence to fib_recurrence_8.
why it matters
The definition supplies a compact reference for the Fibonacci relations that tie the sequence to spatial dimension D=3 and the eight-tick octave 2^3 inside the Recognition framework. It closes the list of canonical identities stated in the module documentation and prepares the ground for later use in mass-ladder or phi-power calculations. No downstream theorems currently depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.