f4_eq_3
plain-language theorem explainer
The equality identifies the fourth Fibonacci number with the spatial dimension in the Recognition Science forcing chain. Researchers formalizing T7 eight-tick periodicity cite it when linking Fibonacci indices to D=3. The proof is a direct reflexivity step on the definition of F4.
Claim. $F(4) = 3$, where $F(4)$ denotes the fourth Fibonacci number and equals the spatial dimension.
background
The module formalizes the T7 step of the forcing chain: the ledger period equals $2^D = 8$ at $D=3$, called the eight-tick fundamental periodicity. F4 is defined directly as the constant 3, with the accompanying statement that this value equals the spatial dimension. The upstream definition supplies the base case for the Fibonacci recurrence that later connects $F(4)$ to $F(6)=8$.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of F4.
why it matters
This equality supplies the Fibonacci representation of spatial dimension inside the T7 formalization. It supports the module claim that both $D=3$ and the period 8 are Fibonacci numbers linked by the recurrence $F(6)=F(5)+F(4)$. In the broader framework it anchors the eight-tick octave derived from J-uniqueness and the self-similar fixed point at $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.