The four polynomials of the lift

P = T^3 - T vanishes at every element of F_3, and Q = P^2 is the multiplier that carries a set of small polynomials into the top of a larger degree range. V_s is the quadratic interpolant that realises a prescribed triple of values at 0, 1, 2, and R_r is a general polynomial of degree below 3.

This file records their degrees, their values on F_3, the two coefficients of Q the construction reads ([T^5] Q = 0 and [T^6] Q = 1), and the two divisibility facts the square-freeness argument needs: a polynomial of degree at most 2 vanishing on F_3 is zero, and P divides any polynomial vanishing on F_3.

noncomputable def NaslundCounterexample.P : Polynomial (ZMod 3)

P = T^3 - T, which vanishes at every element of F_3.

Equations

• NaslundCounterexample.P = Polynomial.X ^ 3 - Polynomial.X

noncomputable def NaslundCounterexample.Q : Polynomial (ZMod 3)

Q = P^2 = T^6 + T^4 + T^2, the multiplier of the lift.

Equations

• NaslundCounterexample.Q = NaslundCounterexample.P ^ 2

noncomputable def NaslundCounterexample.V (s : Fin 4 → ZMod 3) : Polynomial (ZMod 3)

The interpolant V_s = s_0 + (s_2 - s_1) T - (s_0 + s_1 + s_2) T^2, whose value at c is s_c for c = 0, 1, 2.

Equations

• NaslundCounterexample.V s = Polynomial.C (s 0) + Polynomial.C (s 2 - s 1) * Polynomial.X - Polynomial.C (s 0 + s 1 + s 2) * Polynomial.X ^ 2

noncomputable def NaslundCounterexample.R (r : Fin 3 → ZMod 3) : Polynomial (ZMod 3)

The polynomial r_0 + r_1 T + r_2 T^2 of degree below 3 with coefficient vector r.

Equations

• NaslundCounterexample.R r = Polynomial.C (r 0) + Polynomial.C (r 1) * Polynomial.X + Polynomial.C (r 2) * Polynomial.X ^ 2

P

theorem NaslundCounterexample.P_monic : P.Monic

P is monic, being T^3 minus a polynomial of smaller degree.

theorem NaslundCounterexample.P_ne_zero : P ≠ 0

P is not the zero polynomial.

theorem NaslundCounterexample.degree_P : P.degree = 3

P has degree 3.

theorem NaslundCounterexample.natDegree_P : P.natDegree = 3

P has natural degree 3.

theorem NaslundCounterexample.eval_P (c : ZMod 3) : Polynomial.eval c P = 0

P vanishes at every element of F_3: c ^ 3 = c there.

Q

theorem NaslundCounterexample.Q_eq : Q = Polynomial.X ^ 6 + Polynomial.X ^ 4 + Polynomial.X ^ 2

Q = T^6 + T^4 + T^2: squaring P in characteristic 3 turns -2 into 1.

theorem NaslundCounterexample.Q_monic : Q.Monic

Q is monic.

theorem NaslundCounterexample.Q_ne_zero : Q ≠ 0

Q is not the zero polynomial.

theorem NaslundCounterexample.degree_Q : Q.degree = 6

Q has degree 6.

theorem NaslundCounterexample.natDegree_Q : Q.natDegree = 6

Q has natural degree 6.

theorem NaslundCounterexample.eval_Q (c : ZMod 3) : Polynomial.eval c Q = 0

Q vanishes at every element of F_3.

theorem NaslundCounterexample.coeff_Q_five : Q.coeff 5 = 0

Q has no T^5 term; this is why the parameter u does not disturb the top coordinate of a lifted polynomial.

theorem NaslundCounterexample.coeff_Q_six : Q.coeff 6 = 1

The leading coefficient of Q, read at T^6.

The interpolant V_s

theorem NaslundCounterexample.eval_V_zero (s : Fin 4 → ZMod 3) : Polynomial.eval 0 (V s) = s 0

V_s(0) = s_0.

theorem NaslundCounterexample.eval_V_one (s : Fin 4 → ZMod 3) : Polynomial.eval 1 (V s) = s 1

V_s(1) = s_1: the three coefficients sum to s_1 in F_3.

theorem NaslundCounterexample.eval_V_two (s : Fin 4 → ZMod 3) : Polynomial.eval 2 (V s) = s 2

V_s(2) = s_2.

theorem NaslundCounterexample.degree_V_le (s : Fin 4 → ZMod 3) : (V s).degree ≤ 2

V_s has degree at most 2.

theorem NaslundCounterexample.V_congr (s s' : Fin 4 → ZMod 3) (h0 : s 0 = s' 0) (h1 : s 1 = s' 1) (h2 : s 2 = s' 2) : V s = V s'

V_s depends only on the first three coordinates of s.

The general polynomial R_r of degree below 3

theorem NaslundCounterexample.degree_R_le (r : Fin 3 → ZMod 3) : (R r).degree ≤ 2

R_r has degree at most 2.

theorem NaslundCounterexample.coeff_R (r : Fin 3 → ZMod 3) (i : Fin 3) : (R r).coeff ↑i = r i

The coefficients of R_r below T^3 are the entries of r.

theorem NaslundCounterexample.R_injective : Function.Injective R

Distinct coefficient vectors give distinct polynomials.

theorem NaslundCounterexample.degree_P_mul_R_le (r : Fin 3 → ZMod 3) : (P * R r).degree ≤ 5

P · R_r has degree at most 5.

theorem NaslundCounterexample.degree_V_add_P_mul_R_le (s : Fin 4 → ZMod 3) (r : Fin 3 → ZMod 3) : (V s + P * R r).degree ≤ 5

The part of a lifted polynomial below the multiplier Q has degree at most 5.

Vanishing on F_3

theorem NaslundCounterexample.eq_zero_of_degree_le_two_of_eval (f : Polynomial (ZMod 3)) (hf : f.degree ≤ 2) (h0 : Polynomial.eval 0 f = 0) (h1 : Polynomial.eval 1 f = 0) (h2 : Polynomial.eval 2 f = 0) : f = 0

A polynomial of degree at most 2 vanishing at 0, 1 and 2 is zero: it has three roots in a field and degree below 3.

theorem NaslundCounterexample.P_dvd_of_eval (z : Polynomial (ZMod 3)) (h0 : Polynomial.eval 0 z = 0) (h1 : Polynomial.eval 1 z = 0) (h2 : Polynomial.eval 2 z = 0) : P ∣ z

P divides every polynomial vanishing at 0, 1 and 2: the remainder of the division by the monic P has degree below 3 and vanishes there too, hence is zero.

theorem NaslundCounterexample.eq_zero_of_Q_dvd_of_degree_lt (f : Polynomial (ZMod 3)) (hf : f.degree < 6) (h : Q ∣ f) : f = 0

A multiple of Q of degree below 6 is zero.