coprimality_even_fails

formal source

  76  decide
  77
  78/-- For even `D = 2k` (with `k ≥ 1`), `D²(D+2)` is even, so the gcd is `> 1`. -/
  79theorem coprimality_even_fails (k : ℕ) (hk : 0 < k) :
  80    ¬ Nat.Coprime (2 ^ (2 * k)) ((2 * k) ^ 2 * (2 * k + 2)) := by
  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`. -/
  89theorem coprime_at_D3 : Nat.Coprime (2 ^ D) (integrationGap D) := by native_decide
  90
  91/-! ## Integration gap minus one -/
  92
  93/-- The integer `D²(D+2) - 1`. At `D = 3` this equals `44`. -/
  94def gapMinusOne (d : ℕ) : ℕ := integrationGap d - 1
  95
  96theorem gapMinusOne_at_D3 : gapMinusOne D = 44 := by native_decide
  97
  98theorem gapMinusOne_factor : gapMinusOne D = 4 * 11 := by native_decide
  99
 100/-! ## φ-power identity (matter-balance bridge) -/
 101
 102noncomputable section
 103
 104/-- The active edge count per fundamental tick. -/
 105def A : ℤ := 1
 106
 107/-- The φ-power balance identity at `D = 3`:
 108    `φ^(A − gap) · φ^gap = φ`, equivalently `φ^(−44) · φ^45 = φ`. -/
 109theorem gap_balance :