eight_tick_fibonacci_connection
plain-language theorem explainer
The declaration establishes that the sixth Fibonacci number equals eight, thereby linking the eight-tick periodicity at three spatial dimensions to the Fibonacci sequence within the Recognition Science framework. Researchers examining the T7 forcing chain step would reference this result to verify the numerical identity between the ledger period and F_6. The proof relies on direct evaluation using the decide tactic.
Claim. In the Fibonacci sequence defined by $F_0=0$, $F_1=1$ and $F_{n+2}=F_{n+1}+F_n$, the equality $F_6=8$ holds.
background
The module formalizes the 8-tick periodicity arising from D=3 in the RS forcing chain T7. The ledger period is defined as 2^D, yielding 8 when D=3. This period coincides with the sixth Fibonacci number. Upstream results provide the Fibonacci definition in multiple contexts: as a recursive function in Gap45.Derivation, in ContinuedFractionPhi, and as an abbreviation to Nat.fib in ZeckendorfJCost.
proof idea
The proof is a one-line wrapper that invokes the decide tactic to verify the equality by exhaustive computation of the Fibonacci sequence up to the sixth term.
why it matters
This theorem fills the T7 step in the forcing chain by confirming that the eight-tick period at D=3 equals F_6 in the Fibonacci sequence, consistent with the self-similar fixed point phi and the phi-ladder structure. It connects to downstream siblings such as ledgerPeriod_eq_8 and both_fibonacci_at_D3, supporting the claim that both spatial dimension and the period are Fibonacci numbers linked by the recurrence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.