dimension_is_three
plain-language theorem explainer
Any natural number D that admits both a complete hypercube cover of period 2^D and the 45-gap synchronization identity lcm(2^D,45)=360 must equal 3. Citation target for the T8 spatial-dimension step and for the module's absolute RSCounting/Gap45 characterization. The proof discards the cover witness and applies the arithmetic equivalence that pins the LCM identity to D=3.
Claim. If $D\in\mathbb{N}$ admits a complete cover of the $D$-hypercube with period $2^D$, and if $\mathrm{lcm}(2^D,45)=360$, then $D=3$.
background
The Verification.Dimension module isolates a lightweight arithmetic route to spatial dimension three: RSCounting (hypercube coverage at period $2^D$) together with 45-gap synchronization forces $D=3$, and yields the absolute iff RSCounting_Gap45_Absolute D ↔ D = 3. The path is kept dependent only on LCM facts and the RecogSpec layer so PrimeClosure stays thin.
The hypothesis is the witness DimensionalRigidityWitness D: existence of a CompleteCover D whose period equals $2^D$, conjoined with the synchronization target $\mathrm{lcm}(2^D,45)=360$. Coverage makes the power-of-two period structural rather than ad hoc; the LCM identity ties rung-45 timing to that coverage. Framework-side, T8 already names $D=3$ as the forced spatial dimension (also recorded as the constant $D:=3$ in GapDerivation and AlphaDerivation); this theorem is the verification-layer certificate that the counting-plus-sync package recovers the same value.
proof idea
Destructure the witness into the coverage existential and the synchronization equality. The cover is unused quantitatively (a comment flags that a stronger uniqueness argument could fold coverage/causality into the sync step). The conclusion is the forward direction of RecogSpec.lcm_pow2_45_eq_iff D, which states that $\mathrm{lcm}(2^D,45)=360$ if and only if $D=3$. A simpa closes the goal from that equivalence applied to the sync half of the witness.
why it matters
Closes the verification certificate that spatial dimension is three under the RS counting and Gap45 package, matching the T8 landmark in the forcing chain (and the constants $D:=3$ elsewhere in the monolith). The module doc positions this as the one-direction half of the consolidated absolute statement: only $D=3$ satisfies RSCounting plus Gap45 synchronization, with the sibling iff rs_counting_gap45_absolute_iff_dim3 and onlyD3_satisfies_RSCounting_Gap45_Absolute as the natural parents. No downstream edges are recorded yet; the declaration is a leaf certificate for PrimeClosure rather than an intermediate lemma. The unused coverage half is an explicit invitation for a tighter uniqueness proof that would make both conjuncts load-bearing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.