coprime_at_D3
plain-language theorem explainer
At the forced spatial dimension D=3 the integers 8 and 45 are coprime. Researchers working on dimensional selection within Recognition Science cite the result to confirm that the recognition period 2^D stays coprime to the integration gap precisely when D is odd. The proof is a one-line native decision procedure that evaluates the gcd directly.
Claim. Let $D=3$ be the forced spatial dimension. Then $gcd(2^D, D^2(D+2))=1$.
background
The integration gap is the integer $D^2(D+2)$, obtained as the product of the parity count $D^2$ and the configuration dimension $D+2$. At $D=3$ this product equals 45. The module establishes that $gcd(2^D, D^2(D+2))=1$ if and only if $D$ is odd, which combines with the linking argument in Foundation.DimensionForcing to restrict admissible dimensions to the single value $D=3$ among the odd candidates.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic. This reduces the coprimality predicate to a direct computation of the greatest common divisor of 8 and 45.
why it matters
The declaration is packaged inside the IntegrationGapCert structure and supplies the coprimality leg of the ConstraintS_Cert used by Gap45.SyncMinimization. It closes the argument that only odd dimensions keep the recognition cycle orderly and, together with the dimension-forcing step, isolates D=3. The result therefore supports the eight-tick octave and the selection of three spatial dimensions in the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.