f4_eq_spatialDim
plain-language theorem explainer
The declaration equates the fourth Fibonacci number to the spatial dimension by definition within the eight-tick periodicity formalization. Researchers tracing the T7 step of the forcing chain would cite it to anchor Fibonacci structure to D=3 before deriving the ledger period of 8. The proof is a one-line reflexivity between the two constant definitions.
Claim. $F(4) = D$, where $F(4)$ is the fourth Fibonacci number and $D$ is the spatial dimension.
background
The module formalizes T7 of the Recognition Science forcing chain: the ledger period equals $2^D$, which evaluates to 8 when the spatial dimension is fixed at 3. This yields the eight-tick fundamental periodicity. The fourth Fibonacci number is introduced as the constant 3 to match this dimension, consistent with the recurrence relation that later produces $F(6)=8$. Upstream results supply the gap function $F(Z) = log(1 + Z/φ)/log(φ)$ from AnchorPolicy and the master generating functional from Pipelines, though the local F4 is the Fibonacci constant rather than the gap.
proof idea
The proof is a one-line wrapper that applies reflexivity to the constant definitions of F4 and spatialDim.
why it matters
This equality completes the T7 formalization by confirming both the spatial dimension and F(4) equal 3, which feeds the Fibonacci recurrence to establish the ledger period of 8. It directly supports the module claim that D=3 and the period 8 are both Fibonacci numbers connected by F(6) = F(5) + F(4). The step touches the open question of whether D=3 can be derived without prior assumption in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.