dimension_three_of_cover_and_sync
plain-language theorem explainer
If a complete D-dimensional cover has combinatorial period 2^D and the synchronization identity lcm(2^D,45)=360 holds, then the spatial dimension equals three. Verification and PrimeClosure paths cite this as the strong necessity form of D=3 forcing from independent witnesses. The proof is a one-line application of the arithmetic iff for when the lcm of a power of two with 45 equals 360; the cover premise is carried only as a semantic witness.
Claim. Let $D\in\mathbb{N}$. Suppose there exists a complete cover in dimension $D$ whose period equals $2^D$, and suppose $\operatorname{lcm}(2^D,45)=360$. Then $D=3$.
background
In Recognition Science, spatial dimension is forced to three along the forcing chain (T8). This module isolates a lightweight arithmetic route to the same conclusion: RSCounting together with 45-gap synchronization. When $D=3$, the cover period is the eight-tick octave $2^3=8$ (T7).
A complete cover of dimension $D$ is a combinatorial covering structure whose natural period is $2^D$ (hypercube vertex count). The identity $\operatorname{lcm}(2^D,45)=360$ encodes Gap45 absolute synchronization against the 360-tick calendar. Per the module doc, the argument depends only on arithmetic facts about lcm and the spec-layer characterization that $\operatorname{lcm}(2^D,45)=360$ holds precisely at $D=3$, keeping the path light for PrimeClosure.
The coverage premise is independent of pure arithmetic: it ensures $2^D$ is the actual combinatorial period of a realized cover, not merely a free parameter in the lcm equation.
proof idea
Term-mode one-liner. Apply the forward direction of the RecogSpec characterization that $\operatorname{lcm}(2^D,45)=360$ if and only if $D=3$, at the given $D$. The simpa tactic feeds the sync hypothesis through that equivalence and closes $D=3$. The complete-cover existence hypothesis is unused in the proof body; it is retained only as the semantic witness that $2^D$ is realized as a cover period.
why it matters
Strong necessity form of dimension-three forcing inside Verification.Dimension. The module goal is that RSCounting with Gap45 synchronization forces $D=3$, and the sibling biconditional upgrades one-way necessity to sufficiency: the RSCounting+Gap45 absolute predicate holds if and only if the spatial dimension is three. Related siblings package the same arithmetic into absolute and iff forms (dimension_is_three, the only-$D=3$ satisfaction lemma, and the absolute-iff-dim3 characterization).
Framework landmarks: T7 (eight-tick octave, period $2^3$) and T8 ($D=3$ spatial dimensions). The 45-gap and 360 calendar are the RS counting synchronization data. No recorded downstream uses yet; the lemma sits as a lightweight building block for PrimeClosure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.