F5
plain-language theorem explainer
F5 assigns the natural number 5 as the fifth term in the Fibonacci sequence used to connect spatial dimension 3 with the ledger period of 8. Researchers formalizing the T7 step of the Recognition Science forcing chain cite this constant to verify that D and 2^D are consecutive Fibonacci numbers. The definition is a direct constant assignment with no computation or lemmas required.
Claim. $F_5 = 5$, where $F_n$ denotes the Fibonacci sequence satisfying $F_4 = 3$ and $F_6 = 8$.
background
The module formalizes the 8-tick periodicity from the RS forcing chain at T7, where ledgerPeriod equals 2^D and evaluates to 8 when D equals 3. Spatial dimension is identified with F4 equals 3, while the period is F6 equals 8. These are linked by the recurrence F6 equals F5 plus F4, as stated in the module documentation for the T7 formalisation with zero axioms or sorrys.
proof idea
Direct definition assigning the constant 5 to F5 in the natural numbers. It enables the one-line decide proof of the recurrence in the sibling fibonacci_recurrence declaration.
why it matters
F5 completes the Fibonacci triple that certifies both D equals 3 and the eight-tick ledger period as Fibonacci numbers at the T7 octave step. It is referenced inside EightTickCert to build the structure and inside fibonacci_recurrence to confirm F6 equals F5 plus F4. This anchors the RS-native relation between the eight-tick period 2^3 and the phi-ladder depth at D equals 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.