Ramaekers's conjecture is false for n = 4

This construction was originally found by Tom Adamczewski using GPT-6 and posted at https://github.com/tadamcz/n-conjecture-strong. The port to Redhill was done by me without any (further) LLM usage whatsoever.

def FourCase.tup (u : ℤ) : Fin 4 → ℤ

The sequence of 4-tuples containing an infinite subsequence in ramaekersTuples whose qualities tend to 9 / 8.

Equations

• FourCase.tup u 0 = u ^ 9
• FourCase.tup u 1 = (8 - u) ^ 5 * (u ^ 2 + 20 * u + 280) ^ 2
• FourCase.tup u 2 = -105 * (2 * u - 3) ^ 6
• FourCase.tup u 3 = 130032 * u ^ 4 + 10728480 * u ^ 3 - 202978980 * u ^ 2 + 1238324220 * u - 2568934655

@[reducible, inline]

abbrev FourCase.M : ℤ

The LCM of all moduli needed to prove pairwise coprimality. The original repository's M is four times this.

Equations

• FourCase.M = 2 * 3 * 5 * 7 * 13 * 23 * 41 * 103 * 113 * 127 * 149 * 197 * 439 * 1249 * 395119 * 649541 * 399635598557777987

theorem FourCase.sum_tup {u : ℤ} : ∑ i : Fin 4, tup u i = 0

theorem FourCase.quartic_modEq {u n : ℤ} (mu : u ≡ 19 [ZMOD n]) : 130032 * u ^ 4 + 10728480 * u ^ 3 - 202978980 * u ^ 2 + 1238324220 * u - 2568934655 ≡ 130032 * 19 ^ 4 + 10728480 * 19 ^ 3 - 202978980 * 19 ^ 2 + 1238324220 * 19 - 2568934655 [ZMOD n]

theorem FourCase.isCoprime_zero_one {u : ℤ} (mu : u ≡ 19 [ZMOD 70]) : IsCoprime (tup u 0) (tup u 1)

theorem FourCase.isCoprime_zero_two {u : ℤ} (mu : u ≡ 19 [ZMOD 105]) : IsCoprime (tup u 0) (tup u 2)

theorem FourCase.isCoprime_zero_three {u : ℤ} (mu : u ≡ 19 [ZMOD 2568934655]) : IsCoprime (tup u 0) (tup u 3)

theorem FourCase.isCoprime_one_two {u : ℤ} (mu : u ≡ 19 [ZMOD M]) : IsCoprime (tup u 1) (tup u 2)

theorem FourCase.isCoprime_one_three {u : ℤ} (mu : u ≡ 19 [ZMOD M]) : IsCoprime (tup u 1) (tup u 3)

theorem FourCase.isCoprime_two_three {u : ℤ} (mu : u ≡ 19 [ZMOD M]) : IsCoprime (tup u 2) (tup u 3)

theorem FourCase.pairwiseCoprime_tup {u : ℤ} (mu : u ≡ 19 [ZMOD M]) : PairwiseCoprime (tup u)