RSCounting_Gap45_Absolute
plain-language theorem explainer
Packages two independent witnesses into one predicate on spatial dimension D: existence of a complete D-cover whose period is exactly 2^D, and the arithmetic identity lcm(2^D, 45) = 360. Downstream necessity and iff theorems cite this predicate as the single hypothesis that forces D = 3. The body is a pure definition, not a derived claim.
Claim. For $D \in \mathbb{N}$, the absolute RS-counting and Gap-45 synchronization predicate holds of $D$ when (i) there exists a complete cover of the $D$-dimensional hypercube whose period equals $2^D$, and (ii) $\mathrm{lcm}(2^D, 45) = 360$.
background
The Verification.Dimension module isolates a lightweight arithmetic path from RS counting plus Gap-45 synchronization to the forced spatial dimension $D = 3$. It depends only on lcm facts and the RecogSpec layer (notably lcm_pow2_45_eq_iff), keeping the argument available to PrimeClosure.
A complete cover of dimension $D$ is a combinatorial witness that the $D$-hypercube admits a closed recognition schedule; the period condition $2^D$ is the native tick count of that hypercube (eight ticks when $D = 3$). The second conjunct is the Gap-45 synchronization identity: rung 45 must lock to the coverage period so that their least common multiple is the fixed octave multiple 360.
Framework context: T7 forces the eight-tick octave (period $2^3$), and T8 forces $D = 3$ spatial dimensions. The constant $D := 3$ appears upstream in GapDerivation and AlphaDerivation as the dimension forced by linking and by T8.
proof idea
Definitional packaging only. The predicate is the conjunction of an existential cover witness (CompleteCover D with period = 2^D) and the bare Nat equality lcm(2^D, 45) = 360. No tactics, no lemmas applied at this site; downstream theorems unpack the pair and discharge the lcm half via RecogSpec.
why it matters
This is the single hypothesis fed to onlyD3_satisfies_RSCounting_Gap45_Absolute ("only D=3 satisfies RSCounting + Gap45 synchronization") and to the biconditional rs_counting_gap45_absolute_iff_dim3. The module doc states the goal explicitly: RSCounting together with 45-gap synchronization forces $D = 3$, with the iff upgrade. Framing both conjuncts as independently witnessed keeps the coverage period from being an ad-hoc number and ties rung-45 timing to that coverage. In the forcing chain this sits at T7 (eight-tick octave) and T8 ($D = 3$), giving a verification-layer certificate that the dimension forced by linking and by the octave is the unique solution of the counting-plus-sync equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.