f6_eq_8
plain-language theorem explainer
The equality equates the sixth Fibonacci number to 8, matching the ledger period at spatial dimension three. Researchers tracing the Recognition Science T7 step would cite it to fix the eight-tick periodicity. The proof reduces immediately to reflexivity on the supplied definition of F6.
Claim. $F(6) = 8$, where $F(6)$ denotes the sixth Fibonacci number and equals the ledger period $2^D$ at $D=3$.
background
The module formalizes the eight-tick periodicity from the Recognition Science forcing chain at T7. At spatial dimension $D=3$ the ledger period is $2^D=8$. This value is identified with the sixth Fibonacci number. The sibling definition supplies F6 : ℕ := 8 directly. The module doc states that D=3 and the period are both Fibonacci numbers connected by the recurrence F(6) = F(5) + F(4).
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of F6.
why it matters
This declaration anchors the T7 step by confirming F(6)=8 as the ledger period at D=3. It supports the module claim that both D=3 (F(4)=3) and the period (F(6)=8) are Fibonacci numbers. The 8-tick period times the 5-rung depth is noted as 40, near φ^8.37. No downstream uses appear in the graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.