coprimality_odd
plain-language theorem explainer
For every natural number k, the odd integer D = 2k+1 satisfies gcd(2^D, D²(D+2)) = 1. Gap-derivation and dimension-forcing arguments cite this to show that the configuration gap is coprime to the hypercube order precisely when D is odd. The proof reduces to showing the product is odd via a ring identity and one Euclidean gcd step.
Claim. For every natural number $k$, writing $D = 2k+1$, one has $\gcd\bigl(2^{D},\, D^{2}(D+2)\bigr) = 1$. Equivalently, $2^{2k+1}$ is coprime to $(2k+1)^{2}(2k+3)$.
background
The module derives the coherence-energy gap 45 from spatial dimension alone (boundary item B-22). A recognition event carries $D+2$ independent degrees of freedom: $D$ spatial (T8), one temporal tick advance (T2), and one ledger-balance mode $J(x)=J(x^{-1})$ (T3). Coherence energy is $\varphi^{-1}$ per degree of freedom, so $E_{\mathrm{coh}}=\varphi^{-(D+2)}$; at the forced value $D=3$ this is $\varphi^{-5}$.
The integer $D^{2}(D+2)$ is the configuration gap that appears in the parity count and in the LCM that packages the gap. The hypercube on $D$ bits has $2^{D}$ vertices. Coprimality of $2^{D}$ with the gap is needed so that the gap does not share 2-power factors with the discrete geometry. The companion statement for even $D$ shows the gcd is strictly larger than 1, giving a fourth parity argument that $D$ must be odd.
proof idea
It is enough to prove $\mathrm{Nat.Coprime},2,\bigl((2k+1)^{2}(2k+3)\bigr)$, then raise the left factor by $\mathrm{pow_left}$. Expand the product by ring arithmetic to the odd form $2n+1$ with $n=4k^{3}+10k^{2}+7k+1$. Rewrite the goal as $\gcd(2,2n+1)=1$, apply the Euclidean recurrence $\mathrm{Nat.gcd_rec}$, and observe $(2n+1)\bmod 2=1$ (by omega). The final $\gcd(2,1)=1$ is discharged by decide.
why it matters
Feeds the certificate field coprime of gap45_cert, which packages the full gap-45 derivation at $D=3$: configuration dimension 5, parity count matching the enumeration, gap value 45, and this coprimality. Together with coprimality_even_fails it supplies an independent reason $D$ is odd, which combines with Alexander duality (selecting $D=3$ from T8) so that gap 45 follows from dimension alone. In the forcing chain this sits under T8 ($D=3$ spatial) and the B-22 closure that $E_{\mathrm{coh}}=\varphi^{-5}$ matches Constants.E_coh. Status in-module is zero sorry and zero axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.