DimensionalRigidityWitness
plain-language theorem explainer
A predicate on natural D asserting two independent conditions: a complete cover of the D-cube whose period equals 2^D, and the arithmetic identity lcm(2^D, 45) = 360. Anyone proving spatial dimension uniqueness in RS cites it as the joint hypothesis package. It is a pure definition (conjunction of existence and an lcm equation), not a proved statement.
Claim. For $D \in \mathbb{N}$, the dimensional rigidity witness holds 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 shows that RS counting plus 45-gap synchronization force spatial dimension $D = 3$, with the iff form that the absolute counting-and-gap predicate holds exactly when $D = 3$. The argument is kept arithmetic: it uses only lcm facts and the RecogSpec layer identity relating $\mathrm{lcm}(2^D, 45)$ to 360.
A complete cover (from Patterns) is a structured covering of the $D$-cube whose period is the length of the discrete recognition cycle. The eight-tick octave of the forcing chain is the $D = 3$ case $2^3 = 8$. The constant 45 is the rung-gap timing target whose least common multiple with the cover period is required to hit the synchronization value 360.
Upstream, $D$ is fixed to 3 in AlphaDerivation as the spatial dimension forced by linking (T8/T9 in the primer). The witness packages coverage existence and the sync identity so both remain independently checkable before uniqueness is deduced.
proof idea
Definitional, not a proof. The body is the conjunction of an existential over CompleteCover D with period equal to $2^D$, and the bare Nat equality $\mathrm{lcm}(2^D, 45) = 360$. No tactics or lemmas are applied; downstream theorems unpack the pair and feed the second conjunct into RecogSpec.lcm_pow2_45_eq_iff.
why it matters
This is the hypothesis bundle for dimension_is_three: if the witness holds at $D$, then $D = 3$. That theorem discards the cover conjunct for the uniqueness step and applies the lcm characterization, so the witness exists to keep coverage structurally present even when only sync pins $D$.
In the Recognition framework it sits on the T7–T8 segment: eight-tick octave ($2^3$) and forced spatial dimension three. Packaging both RS counting (cover period $2^D$) and Gap45 synchronization makes the later iff RSCounting_Gap45_Absolute $D \leftrightarrow D = 3$ readable as a single rigidity statement rather than two ad-hoc side conditions. Sibling hypotheses (no linking in $D = 2$, trivial linking in $D = 4$, unique three-dimensional linking) sit beside it as the geometric story that the arithmetic uniqueness here does not yet encode.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.