coprimality_odd
plain-language theorem explainer
For any natural number k the integer (2k+1)^2 times (2k+3) is coprime to every power of 2. Recognition Science invokes the fact to guarantee that the recognition period 2^D stays coprime to the integration gap whenever D is odd. The proof reduces the claim to an oddness check on the second factor, expands the expression by ring, then applies the Euclidean algorithm and decides the resulting gcd.
Claim. For every natural number $k$, $2^{2k+1}$ is coprime to $(2k+1)^2(2k+3)$.
background
The module defines the integration gap as the integer $D^2(D+2)$. At the forced dimension $D=3$ this evaluates to 45. The module proves that gcd$(2^D, D^2(D+2))=1$ if and only if $D$ is odd, ensuring the recognition cycle remains orderly when $2^D$ supplies the natural period.
proof idea
The tactic proof first reduces to showing the second factor is coprime to 2. It rewrites the product via ring to obtain an explicit odd expression 2n+1. Nat.gcd_rec together with an omega step confirming the remainder is 1, followed by decide, finishes the argument.
why it matters
The theorem is called by integrationGapCert to certify the gap values at D=3. Together with the linking argument in DimensionForcing it restricts the spatial dimension to the single odd value D=3. The result directly supports the eight-tick octave (period 2^3) and the requirement that the recognition period remain coprime to the gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.