Low-degree affine-line recovery

This file formalizes the polynomial identity used by the local-recovery gadget in the Boolean mass-production manuscript. A multivariate polynomial of total degree below |K| - 1 is recoverable at the center of every affine line from its values at all nonzero line parameters. In characteristic two, the recovery operation is a sum.

noncomputable def Algebraic.MassProduction.lineCoordinate {K : Type u_1} {Coordinate : Type u_2} [CommRing K] (center direction : Coordinate → K) (index : Coordinate) : Polynomial K

The affine-linear polynomial substituted for coordinate index when restricting a multivariate polynomial to the line through center in direction direction.

Equations

• Algebraic.MassProduction.lineCoordinate center direction index = Polynomial.C (center index) + Polynomial.C (direction index) * Polynomial.X

noncomputable def Algebraic.MassProduction.lineRestriction {K : Type u_1} {Coordinate : Type u_2} [CommRing K] (polynomial : MvPolynomial Coordinate K) (center direction : Coordinate → K) : Polynomial K

Restrict a multivariate polynomial to an affine line.

Equations

• Algebraic.MassProduction.lineRestriction polynomial center direction = (MvPolynomial.eval₂Hom Polynomial.C (Algebraic.MassProduction.lineCoordinate center direction)) polynomial

theorem Algebraic.MassProduction.polynomial_sum_eval_eq_zero {K : Type u_1} [Fintype K] [Field K] (polynomial : Polynomial K) (degree : polynomial.natDegree < Fintype.card K - 1) : ∑ value : K, Polynomial.eval value polynomial = 0

A univariate polynomial of degree below |K| - 1 has evaluation sum zero over the finite field K.

theorem Algebraic.MassProduction.polynomial_line_identity {K : Type u_1} [Fintype K] [Field K] [DecidableEq K] (polynomial : Polynomial K) (degree : polynomial.natDegree < Fintype.card K - 1) : Polynomial.eval 0 polynomial = -∑ value ∈ Finset.univ.erase 0, Polynomial.eval value polynomial

Isolating the zero evaluation gives the punctured-field identity.

theorem Algebraic.MassProduction.natDegree_lineCoordinate_le {K : Type u_1} {Coordinate : Type u_2} [CommRing K] (center direction : Coordinate → K) (index : Coordinate) : (lineCoordinate center direction index).natDegree ≤ 1

Every substituted affine coordinate has degree at most one.

theorem Algebraic.MassProduction.lineRestriction_eval {K : Type u_1} {Coordinate : Type u_2} [CommRing K] (polynomial : MvPolynomial Coordinate K) (center direction : Coordinate → K) (parameter : K) : Polynomial.eval parameter (lineRestriction polynomial center direction) = (MvPolynomial.eval fun (index : Coordinate) => center index + direction index * parameter) polynomial

Evaluating a line restriction has the expected affine-line semantics.

theorem Algebraic.MassProduction.natDegree_lineMonomial_le {K : Type u_1} {Coordinate : Type u_2} [CommRing K] (center direction : Coordinate → K) (degrees : Coordinate →₀ ℕ) (coefficient : K) : ((MvPolynomial.eval₂Hom Polynomial.C (lineCoordinate center direction)) ((MvPolynomial.monomial degrees) coefficient)).natDegree ≤ degrees.sum fun (x : Coordinate) (exponent : ℕ) => exponent

The line restriction of a monomial has degree at most its total exponent.

theorem Algebraic.MassProduction.natDegree_lineRestriction_le {K : Type u_1} {Coordinate : Type u_2} [CommRing K] (polynomial : MvPolynomial Coordinate K) (center direction : Coordinate → K) : (lineRestriction polynomial center direction).natDegree ≤ polynomial.totalDegree

Restriction to an affine line cannot increase total degree.

theorem Algebraic.MassProduction.affineLine_identity {K : Type u_1} {Coordinate : Type u_2} [Fintype K] [Field K] [DecidableEq K] (polynomial : MvPolynomial Coordinate K) (degree : polynomial.totalDegree < Fintype.card K - 1) (center direction : Coordinate → K) : (MvPolynomial.eval center) polynomial = -∑ parameter ∈ Finset.univ.erase 0, (MvPolynomial.eval fun (index : Coordinate) => center index + direction index * parameter) polynomial

Low total degree gives recovery from the punctured affine line.

theorem Algebraic.MassProduction.neg_eq_self_of_char_two {K : Type u_1} [Ring K] [CharP K 2] (value : K) : -value = value

In a ring of characteristic two, every element is its own negation.

theorem Algebraic.MassProduction.affineLine_identity_charTwo {K : Type u_1} {Coordinate : Type u_2} [Fintype K] [Field K] [DecidableEq K] [CharP K 2] (polynomial : MvPolynomial Coordinate K) (degree : polynomial.totalDegree < Fintype.card K - 1) (center direction : Coordinate → K) : (MvPolynomial.eval center) polynomial = ∑ parameter ∈ Finset.univ.erase 0, (MvPolynomial.eval fun (index : Coordinate) => center index + direction index * parameter) polynomial

In characteristic two, punctured-line recovery is the sum of the other line values.