The two bases

The recursion needs a starting set at each residue of n modulo 8 that the construction reaches. B_0 = {0} is the trivial square-difference-free subset of P_{3,0}, and

B_4 = { a T^3 + b T + c (1 - T^2) : a, b, c ∈ F_3 }

is a square-difference-free subset of P_{3,4} with 27 elements. Square-difference-freeness of B_4 is the only place where the shape 1 - T^2 matters: a difference of two of its elements has constant term c and T^2-coefficient -c, while a nonzero square of degree below 4 is the square of a linear polynomial v + u T, with constant term v^2 and T^2-coefficient u^2; so v^2 + u^2 = 0, which in F_3 forces u = v = 0.

noncomputable def NaslundCounterexample.base0 : Finset (Polynomial (ZMod 3))

The base B_0 = {0} ⊆ P_{3,0}.

Equations

• NaslundCounterexample.base0 = {0}

theorem NaslundCounterexample.base0_card : base0.card = 1

B_0 has one element.

theorem NaslundCounterexample.base0_allBelow : AllBelow 0 base0

B_0 lies in P_{3,0}.

theorem NaslundCounterexample.base0_sdf : SquareDifferenceFree base0

B_0 is square-difference-free.

noncomputable def NaslundCounterexample.base4Map (t : ZMod 3 × ZMod 3 × ZMod 3) : Polynomial (ZMod 3)

One element of B_4, the polynomial a T^3 + b T + c (1 - T^2).

Equations

• NaslundCounterexample.base4Map t = Polynomial.C t.1 * Polynomial.X ^ 3 + Polynomial.C t.2.1 * Polynomial.X + Polynomial.C t.2.2 * (1 - Polynomial.X ^ 2)

noncomputable def NaslundCounterexample.base4 : Finset (Polynomial (ZMod 3))

The base B_4 = { a T^3 + b T + c (1 - T^2) : a, b, c ∈ F_3 } ⊆ P_{3,4}.

Equations

• NaslundCounterexample.base4 = Finset.image NaslundCounterexample.base4Map Finset.univ

theorem NaslundCounterexample.base4Map_injective : Function.Injective base4Map

Distinct triples give distinct elements of B_4: the coefficients at T^3, T and 1 read a, b and c back.

theorem NaslundCounterexample.base4_card : base4.card = 27

B_4 has 27 elements.

theorem NaslundCounterexample.base4_allBelow : AllBelow 4 base4

B_4 lies in P_{3,4}.

theorem NaslundCounterexample.base4_sdf : SquareDifferenceFree base4

B_4 is square-difference-free. A difference of two of its elements has constant term c and T^2-coefficient -c; a nonzero square of degree below 4 is the square of a linear polynomial v + u T, whose constant term is v^2 and whose T^2-coefficient is u^2; so v^2 + u^2 = 0, and in F_3 that forces u = v = 0.