coprime_at_D3
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish coprimality for any dimension other than 3.
- Does not derive the value of D from first principles.
- Does not supply a physical interpretation of the integration gap.
- Does not address even dimensions beyond the explicit counterexamples already listed in the module.
Lean usage
theorem use_in_cert : IntegrationGapCert where coprime_at_3 := coprime_at_D3formal statement (Lean)
89theorem coprime_at_D3 : Nat.Coprime (2 ^ D) (integrationGap D) := by native_decide
proof body
Term-mode proof.
90
91/-! ## Integration gap minus one -/
92
93/-- The integer `D²(D+2) - 1`. At `D = 3` this equals `44`. -/