coprimality_even_fails
The result shows that for any positive integer k the integers 2 to the power 2k and (2k) squared times (2k plus 2) share the divisor 2 and are therefore not coprime. Dimension-selection arguments in the Recognition Science framework cite the statement to exclude even values of the spatial dimension D. The short proof assumes coprimality for contradiction, records that 2 divides both arguments by elementary divisibility, and obtains an immediate absurdity.
claimFor every positive integer $k$, the integers $2^{2k}$ and $(2k)^2(2k+2)$ are not coprime, i.e., their greatest common divisor exceeds 1.
background
The module studies the integer $D^2(D+2)$, called the integration gap. At $D=3$ this evaluates to 45. The module documentation states that gcd of $2^D$ with the integration gap equals 1 if and only if $D$ is odd; this forces the recognition period $2^D$ to remain coprime to the gap in any orderly cycle. The definition D is the spatial dimension fixed at 3, with configuration dimension and parity count derived from it. The present theorem supplies the complementary negative statement for even arguments.
proof idea
The proof is a direct term-mode argument. It introduces the coprimality hypothesis, records that 2 divides the first factor via dvd_pow and dvd_refl, exhibits an explicit multiple showing 2 divides the second factor, forms their gcd via Nat.dvd_gcd, substitutes the hypothesis, and reaches a contradiction by norm_num.
why it matters in Recognition Science
The lemma completes the even half of the coprimality characterization used by integrationGapCert, which assembles the configuration dimension, parity count, gap value, and coprimality fact at D=3. It thereby supports the module-level claim that only odd D can satisfy the coprimality requirement, narrowing candidates before the linking argument in DimensionForcing selects D=3. This aligns with the framework step that forces three spatial dimensions while preserving an orderly recognition period.
scope and limits
- Does not prove the coprimality claim for odd D.
- Does not compute the explicit gcd value when it exceeds 1.
- Does not treat non-positive or non-integer arguments.
- Applies only to the specific polynomial form D squared times (D plus 2).
formal statement (Lean)
79theorem coprimality_even_fails (k : ℕ) (hk : 0 < k) :
80 ¬ Nat.Coprime (2 ^ (2 * k)) ((2 * k) ^ 2 * (2 * k + 2)) := by
proof body
Term-mode proof.
81 intro h
82 have h1 : 2 ∣ 2 ^ (2 * k) := dvd_pow (dvd_refl 2) (by omega)
83 have h2 : 2 ∣ (2 * k) ^ 2 * (2 * k + 2) := ⟨2 * k ^ 2 * (2 * k + 2), by ring⟩
84 have h3 := Nat.dvd_gcd h1 h2
85 rw [h] at h3
86 exact absurd h3 (by norm_num)
87
88/-- At `D = 3`: `gcd(8, 45) = 1`. -/