D
plain-language theorem explainer
Spatial dimension is fixed at the natural number 3, the value forced by T8 in the Recognition forcing chain. Gap-45, configuration-dimension, and F2-power lattice arguments all cite this constant. The declaration is a bare definition with no proof obligations.
Claim. The spatial dimension is the natural number $D = 3$.
background
The module closes boundary item B-22: a recognition event has configuration dimension $D+2$ (D spatial from the lattice, one temporal tick advance from T2, one balance degree from ledger neutrality $J(x)=J(x^{-1})$ under T3). Coherence energy is then $\varphi^{-(D+2)}$. At $D=3$ this yields $\varphi^{-5}$, matching the RS-native $E_{\mathrm{coh}}$.
Upstream copies of the same constant appear in AlphaDerivation ("spatial dimension forced by T9") and FermionDOFGapBridge ("forced by T8"). The primer landmark T8 is the step that forces three spatial dimensions; the eight-tick octave is the related $2^3$ period on the hypercube of side length 2.
Sibling results in this file compute $\mathrm{configDim}=D+2$, $\mathrm{parityCount}$, and the gap $D^2(D+2)$, all specialized at this value.
proof idea
Bare definition: the natural-number literal 3 is assigned to $D$. No tactics, no lemmas, no sorry.
why it matters
This is the single numeric anchor for the gap-45 derivation. Downstream gap_at_D3 records $D^2(D+2)=9\times 5=45$; coprimality lemmas then show $\gcd(2^D,D^2(D+2))=1$ for odd $D$, supplying a fourth parity argument that $D$ is odd, which with Alexander duality selects $D=3$ and recovers gap-45 from dimension alone.
The constant is also the dimension parameter of F2Power D (the $\mathbb{F}2^D$ vector space underlying the eight-tick lattice: cardinality $2^D$, axis weights, Hamming arithmetic). Action-side Euler–Lagrange material (Hessian metric geodesics) imports it as ambient dimension. Framework landmarks: T8 ($D=3$), T7 (eight-tick period $2^3$), and the B-22 coherence exponent $D+2$ that forces $E{\mathrm{coh}}=\varphi^{-5}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.