coprimality_odd
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove coprimality fails for even D.
- Does not derive the value of D from first principles.
- Does not connect the gap integer to mass or coupling formulas.
- Does not address physical units or empirical constants.
formal statement (Lean)
65theorem coprimality_odd (k : ℕ) :
66 Nat.Coprime (2 ^ (2 * k + 1)) ((2 * k + 1) ^ 2 * (2 * k + 3)) := by
proof body
Tactic-mode proof.
67 suffices h : Nat.Coprime 2 ((2 * k + 1) ^ 2 * (2 * k + 3)) from h.pow_left _
68 show Nat.gcd 2 ((2 * k + 1) ^ 2 * (2 * k + 3)) = 1
69 have hodd : (2 * k + 1) ^ 2 * (2 * k + 3) =
70 2 * (4 * k ^ 3 + 10 * k ^ 2 + 7 * k + 1) + 1 := by ring
71 rw [hodd]
72 set n := 4 * k ^ 3 + 10 * k ^ 2 + 7 * k + 1
73 rw [Nat.gcd_rec]
74 have : (2 * n + 1) % 2 = 1 := by omega
75 rw [this]
76 decide
77
78/-- For even `D = 2k` (with `k ≥ 1`), `D²(D+2)` is even, so the gcd is `> 1`. -/