fibonacci_recurrence
F6 equals F5 plus F4 where F4=3 matches spatial dimension, F5=5 is the intermediate rung, and F6=8 matches the ledger period at D=3. Researchers tracing the Recognition Science T7 forcing chain cite this to anchor the eight-tick periodicity inside the Fibonacci sequence. The proof is a one-line decision procedure on the three concrete natural numbers.
claimLet $F_4 = 3$ denote spatial dimension, $F_5 = 5$, and $F_6 = 8$ denote the ledger period. Then $F_6 = F_5 + F_4$.
background
The module formalises T7 of the forcing chain: at spatial dimension D=3 the ledger period equals 2^D=8, called the eight-tick periodicity. F4 is defined as the constant 3, F6 as the constant 8, and F5 as the constant 5. These sit inside the general Fibonacci recurrence imported from LocalCache, which states that each level capacity equals the sum of the two preceding levels and arises from J-cost-optimal partitioning. The same recurrence appears for the phi-ladder in ThermalFixedPoint, where phi^(n+2) = phi^(n+1) + phi^n holds by the identity phi^2 = phi + 1.
proof idea
One-line wrapper that applies the decide tactic directly to the concrete equality 8 = 5 + 3 after unfolding the three constant definitions F4, F5, F6.
why it matters in Recognition Science
The equality closes the local verification that both D=3 and the eight-tick period are Fibonacci numbers linked by the recurrence. It is invoked by the phi-hierarchy theorems in PhiHierarchyGrowth and by the optimal-partition results in LocalCache that force the ratio to equal phi. The step therefore supplies the concrete numerical anchor for T7 inside the broader claim that the phi-ladder is the unique self-similar fixed point.
scope and limits
- Does not derive the numerical values of F4, F5, F6 from the forcing chain axioms.
- Does not prove the general Fibonacci recurrence for arbitrary sequences.
- Does not address the continuous phi-ladder version of the recurrence.
- Does not establish uniqueness of the eight-tick period without the upstream D=3 result.
formal statement (Lean)
41theorem fibonacci_recurrence : F6 = F5 + F4 := by decide
proof body
Term-mode proof.
42
43/-- D and 2^D are both Fibonacci numbers at D=3. -/