spatial_dim_is_3
plain-language theorem explainer
The eight-tick ledger period equals 2³, fixing three spatial dimensions. Anyone citing the continuum bridge from discrete RS sites to 4D Lorentzian spacetime needs this identity. The proof is pure reflexivity: eight_tick is defined as 8.
Claim. The fundamental eight-tick period satisfies $\mathrm{eight\_tick} = 2^3$ (equivalently $8 = 2^3$), so the spatial dimension forced by the octave coverage is $D = 3$.
background
In Recognition Science the discrete ledger covers a $2^D$-cell voxel per fundamental cycle. The constant eight_tick is defined as $8$ across DimensionForcing, Gap45, and RecognitionThermodynamics: it is the period of one full spatial coverage at $D = 3$, and the fundamental time unit $\tau_0$ is eight ticks.
This module builds the zero-parameter bridge from the J-cost lattice to a Lorentzian continuum. Part 10 records dimensional consistency: once the spatial count is three, adjoining the temporal tick direction yields 4D spacetime. Upstream, DimensionForcing supplies the eight-tick definition; the forcing chain landmark T7 is the eight-tick octave (period $2^3$), and T8 is $D = 3$.
The identity here is the explicit link between those two landmarks: $2^D = 8$ forces $D = 3$.
proof idea
One-line reflexivity. Unfolding eight_tick (defined as the natural number 8 in DimensionForcing and the sibling modules) reduces the goal to $8 = 2^3$, which holds by definition of natural-number exponentiation. No lemmas beyond rfl are required.
why it matters
The continuum-limit certificate packages Lorentzian signature, causal trichotomy, and related fields as a single master record. This theorem supplies the dimensional half of that story: spatial $D = 3$ from the eight-tick octave, so the Minkowski form on $\mathbb{R}^{1,3}$ is the correct ambient signature rather than an ansatz.
In the forcing chain this is the T7–T8 hinge (period $2^3$ forces three spatial dimensions). The module doc lists "$D = 3$ spatial dimensions is FORCED (DimensionForcing)" among the unconditional, zero-parameter claims of the continuum bridge. Without it, the passage from ledger sites to a 4D Lorentzian manifold would leave the spatial rank free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.