Counterexamples to Naslund's Conjecture 13

The conjecture is from Eric Naslund, Paley graphs and Sárközy's theorem in function fields, Quarterly Journal of Mathematics 74 (2023), 627–637, Conjecture 13 (https://arxiv.org/abs/2203.01293v3). This project refutes its square-difference case over F_3; it does not assert a counterexample over other finite fields.

The upstream source was written by Claude under JD Jones's direction, with Claude, GPT-6 and Grok consulted for the construction and proofs. Lean Pool adaptations rename declarations, narrow imports and optimize proofs; the statements are unchanged.

The two polynomial families give the existence statements once their internal degree bound is converted to the public one. The two refutations compare their sizes with the conjectured bound 3^{3n/4}: for n = 8e this is 3^{6e} = 729^e < 810^e, and for n = 8e + 4 it is 3^{6e+3} = 27 · 729^e < 27 · 810^e. The growth rate is the theorem of NaslundCounterexample.Asymptotics.

The statements below are proved from the explicit polynomial families.

theorem NaslundCounterexample.exists_card_810 : ∃ (A : Finset (Polynomial (ZMod 3))), DegreeBelow 8 A ∧ A.card = 810 ∧ SquareDifferenceFree A

A square-difference-free subset of P_{3,8} with 810 elements, the first lift of the one-element base.

theorem NaslundCounterexample.conjecture_fails_at_eight : ¬∀ (A : Finset (Polynomial (ZMod 3))), DegreeBelow 8 A → SquareDifferenceFree A → A.card ≤ 3 ^ 6

The conjectured bound fails at q = 3, k = 2, n = 8: not every square-difference-free subset of P_{3,8} has at most 3^6 = 729 elements, since 810 > 729.

theorem NaslundCounterexample.exists_card_pow (e : ℕ) (he : 1 ≤ e) : ∃ (A : Finset (Polynomial (ZMod 3))), DegreeBelow (8 * e) A ∧ A.card = 810 ^ e ∧ SquareDifferenceFree A

The first family. For every e ≥ 1, a square-difference-free subset of P_{3,8e} with 810^e elements.

theorem NaslundCounterexample.exists_card_twenty_seven_mul_pow (e : ℕ) : ∃ (A : Finset (Polynomial (ZMod 3))), DegreeBelow (8 * e + 4) A ∧ A.card = 27 * 810 ^ e ∧ SquareDifferenceFree A

The second family. For every e, a square-difference-free subset of P_{3,8e+4} with 27 · 810^e elements.

theorem NaslundCounterexample.conjecture_fails (n : ℕ) (h4 : 4 ∣ n) (h8 : 8 ≤ n) : ¬∀ (A : Finset (Polynomial (ZMod 3))), DegreeBelow n A → SquareDifferenceFree A → A.card ≤ 3 ^ (3 * n / 4)

The conjectured bound fails for every admissible n ≥ 8: for 4 ∣ n and n ≥ 8, not every square-difference-free subset of P_{3,n} has at most 3^{3n/4} elements. Such an n is 8e or 8e + 4 with e ≥ 1, and the corresponding family exceeds the bound by (10/9)^e.