FibonacciCert
plain-language theorem explainer
FibonacciCert collects five equalities for the Fibonacci sequence that match RS requirements for spatial dimension and ledger period. Researchers deriving the phi-ladder or eight-tick octave cite it to confirm F(3)=2, F(4)=3=D, F(6)=8=2^D, and the recurrence at n=8. The structure is introduced as a plain definition with no body or computational content.
Claim. A structure asserting the equalities $F_3=2$, $F_4=3$, $F_6=8$, $F_6=2^3$, and $F_8=F_7+F_6$, where $F_n$ denotes the Fibonacci sequence with the standard recurrence $F_{n+2}=F_{n+1}+F_n$.
background
The module derives Fibonacci values intrinsic to RS via φ, quoting the key identity $F(n)φ + F(n-1)=φ^n$. Upstream, fib is defined in Gap45.Derivation as the sequence with bases 1,1 and recurrence fib n + fib (n+1); in ContinuedFractionPhi as starting 0,1 with the same recurrence; and in ZeckendorfJCost as an abbreviation for Nat.fib. The local setting lists five canonical identities, including F(3)=2=D, F(4)=3=D, and F(6)=8=2^D=ledger period, all established by decide.
proof idea
This is a structure definition with empty body that bundles the five fields. Instantiation occurs downstream in fibonacciCert by direct assignment of the lemmas fib3_eq_2, fib4_eq_3, fib6_eq_8, fib6_eq_2cubeD, and fib_recurrence_8.
why it matters
FibonacciCert supplies the bundled certificate required by fibonacciCert, encoding the canonical identities listed in the module documentation. It connects directly to T7 (eight-tick octave, period 2^3 via F(6)=8) and T8 (D=3 via F(4)=3), filling a step in the phi-ladder derivation without new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.