FibonacciCert
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not prove the general Fibonacci recurrence from RS axioms.
- Does not derive the closed form $F_n = (φ^n - (-φ)^{-n})/√5$.
- Does not link these values to the mass formula or J-cost.
- Does not address convergence of $F_{n+1}/F_n$ to φ.
- Does not extend beyond the listed terms up to n=8.
formal statement (Lean)
46structure FibonacciCert where
47 fib3 : Nat.fib 3 = 2
48 fib4 : Nat.fib 4 = 3
49 fib6 : Nat.fib 6 = 8
50 fib6_2cubeD : Nat.fib 6 = 2 ^ 3
51 recurrence : Nat.fib 8 = Nat.fib 7 + Nat.fib 6
52