The two families

Iterating the lift from the two bases gives a square-difference-free subset of P_{3,n} for every n divisible by 4:

• A_0 = {0} and A_{8e+8} = L_{8e}(A_{8e}), of size 810^e inside P_{3,8e};
• A_4 = B_4 and A_{8e+12} = L_{8e+4}(A_{8e+4}), of size 27 · 810^e inside P_{3,8e+4}.

Each induction step needs the lift's three conclusions at an even degree bound: 8e and 8e + 4 are both even, which is why the two families together cover every multiple of 4.

noncomputable def NaslundCounterexample.familyFromZero : ℕ → Finset (Polynomial (ZMod 3))

The first family: A_0 = {0} and A_{8e+8} = L_{8e}(A_{8e}).

Equations

• NaslundCounterexample.familyFromZero 0 = NaslundCounterexample.base0
• NaslundCounterexample.familyFromZero e.succ = NaslundCounterexample.lift (8 * e) (NaslundCounterexample.familyFromZero e)

noncomputable def NaslundCounterexample.familyFromFour : ℕ → Finset (Polynomial (ZMod 3))

The second family: A_4 = B_4 and A_{8e+12} = L_{8e+4}(A_{8e+4}).

Equations

• NaslundCounterexample.familyFromFour 0 = NaslundCounterexample.base4
• NaslundCounterexample.familyFromFour e.succ = NaslundCounterexample.lift (8 * e + 4) (NaslundCounterexample.familyFromFour e)

theorem NaslundCounterexample.familyFromZero_allBelow (e : ℕ) : AllBelow (8 * e) (familyFromZero e)

The e-th member of the first family lies in P_{3,8e}.

theorem NaslundCounterexample.familyFromZero_card (e : ℕ) : (familyFromZero e).card = 810 ^ e

The e-th member of the first family has 810^e elements.

theorem NaslundCounterexample.familyFromZero_sdf (e : ℕ) : SquareDifferenceFree (familyFromZero e)

Every member of the first family is square-difference-free.

theorem NaslundCounterexample.familyFromFour_allBelow (e : ℕ) : AllBelow (8 * e + 4) (familyFromFour e)

The e-th member of the second family lies in P_{3,8e+4}.

theorem NaslundCounterexample.familyFromFour_card (e : ℕ) : (familyFromFour e).card = 27 * 810 ^ e

The e-th member of the second family has 27 · 810^e elements.

theorem NaslundCounterexample.familyFromFour_sdf (e : ℕ) : SquareDifferenceFree (familyFromFour e)

Every member of the second family is square-difference-free.