Definitions

Square-difference-free sets and their maximum cardinality inside the finite space of polynomials over the field with three elements. These definitions retain the semantics of the upstream statements.

def NaslundCounterexample.SquareDifferenceFree (A : Finset (Polynomial (ZMod 3))) : Prop

A finite set of polynomials over F_3 is square-difference-free: no two of its elements differ by a nonzero square.

Equations

• NaslundCounterexample.SquareDifferenceFree A = ∀ f ∈ A, ∀ g ∈ A, ∀ (z : Polynomial (ZMod 3)), g - f = z ^ 2 → z = 0

def NaslundCounterexample.DegreeBelow (n : ℕ) (A : Finset (Polynomial (ZMod 3))) : Prop

Every element of A has degree below n. For n ≥ 1 this says A ⊆ P_{3,n}, the polynomials of degree less than n (the zero polynomial has natDegree 0).

Equations

• NaslundCounterexample.DegreeBelow n A = ∀ f ∈ A, f.natDegree < n

noncomputable def NaslundCounterexample.polynomialsBelow (n : ℕ) : Finset (Polynomial (ZMod 3))

The polynomials of degree below n over F_3, as a finite set: the image of the coefficient vectors Fin n → ZMod 3 under c ↦ Σ c_i T^i.

Equations

• NaslundCounterexample.polynomialsBelow n = Finset.image (fun (c : Fin n → ZMod 3) => ∑ i : Fin n, Polynomial.C (c i) * Polynomial.X ^ ↑i) Finset.univ

noncomputable def NaslundCounterexample.maximumCardinality (n : ℕ) : ℕ

maximumCardinality n: the largest size of a square-difference-free set of polynomials of degree below n over F_3.

Equations

• NaslundCounterexample.maximumCardinality n = (Finset.filter NaslundCounterexample.SquareDifferenceFree (NaslundCounterexample.polynomialsBelow n).powerset).sup Finset.card