Line parity for common-zero-block monomials

Splitting every exponent at the end of a common zero block factors its affine-line restriction as a low-degree polynomial times a Frobenius power. The resulting residue gap excludes positive multiples of q - 1 from the support. Summing over the field therefore gives zero on every affine line. This proof uses Frobenius directly and does not assume Lucas' theorem.

def Algebraic.MassProduction.HighRate.monomialValue {K : Type u_1} {Coordinate : Type u_2} [Field K] [Fintype Coordinate] (degrees : Coordinate → ℕ) (point : Coordinate → K) : K

The evaluation of a reduced multivariate monomial.

Equations

• Algebraic.MassProduction.HighRate.monomialValue degrees point = ∏ coordinate : Coordinate, point coordinate ^ degrees coordinate

noncomputable def Algebraic.MassProduction.HighRate.lineMonomial {K : Type u_1} {Coordinate : Type u_2} [Field K] [Fintype Coordinate] (degrees : Coordinate → ℕ) (center direction : Coordinate → K) : Polynomial K

The univariate polynomial obtained by restricting a monomial to a line.

Equations

• Algebraic.MassProduction.HighRate.lineMonomial degrees center direction = ∏ coordinate : Coordinate, Algebraic.MassProduction.lineCoordinate center direction coordinate ^ degrees coordinate

theorem Algebraic.MassProduction.HighRate.lineMonomial_eval {K : Type u_1} {Coordinate : Type u_2} [Field K] [Fintype Coordinate] (degrees : Coordinate → ℕ) (center direction : Coordinate → K) (parameter : K) : Polynomial.eval parameter (lineMonomial degrees center direction) = monomialValue degrees fun (coordinate : Coordinate) => center coordinate + direction coordinate * parameter

Evaluation commutes with affine-line restriction.

theorem Algebraic.MassProduction.HighRate.lineMonomialNatDegree_le {K : Type u_1} {Coordinate : Type u_2} [Field K] [Fintype Coordinate] (degrees : Coordinate → ℕ) (center direction : Coordinate → K) : (lineMonomial degrees center direction).natDegree ≤ ∑ coordinate : Coordinate, degrees coordinate

Restriction cannot increase the total monomial degree.

theorem Algebraic.MassProduction.HighRate.lineMonomialSplit {K : Type u_1} {Coordinate : Type u_2} [Field K] [Fintype Coordinate] (degrees : Coordinate → ℕ) (center direction : Coordinate → K) (width : ℕ) : lineMonomial degrees center direction = lineMonomial (fun (coordinate : Coordinate) => degrees coordinate % 2 ^ width) center direction * lineMonomial (fun (coordinate : Coordinate) => degrees coordinate / 2 ^ width) center direction ^ 2 ^ width

Splitting exponents modulo a power of two separates the low-degree factor from a Frobenius power.

theorem Algebraic.MassProduction.HighRate.lineMonomialNoPositiveMultiple {K : Type u_1} {Coordinate : Type u_2} [Field K] [Fintype Coordinate] [Fintype K] [CharP K 2] [Nonempty Coordinate] (degrees : Coordinate → ℕ) (center direction : Coordinate → K) (width start blockWidth : ℕ) (fieldCard : Fintype.card K = 2 ^ width) (blockPositive : 0 < blockWidth) (blockFits : start + blockWidth ≤ width) (dimensionFits : Fintype.card Coordinate ≤ 2 ^ blockWidth) (reduced : ∀ (coordinate : Coordinate), degrees coordinate < 2 ^ width) (zeroBlock : CommonZeroBlock degrees start blockWidth) (exponent : ℕ) (inSupport : exponent ∈ (lineMonomial degrees center direction).support) (positive : 0 < exponent) : ¬Fintype.card K - 1 ∣ exponent

A common zero block forbids every positive multiple of q - 1 in the support of the affine-line restriction.

theorem Algebraic.MassProduction.HighRate.polynomialSumEqZeroOfNoPositiveMultiples {K : Type u_1} [Field K] [Fintype K] (polynomial : Polynomial K) (notMultiple : ∀ exponent ∈ polynomial.support, 0 < exponent → ¬Fintype.card K - 1 ∣ exponent) : ∑ value : K, Polynomial.eval value polynomial = 0

A polynomial with no positive q - 1 multiples in its support has zero evaluation sum over the finite field.

theorem Algebraic.MassProduction.HighRate.monomialValueLineParity {K : Type u_1} {Coordinate : Type u_2} [Field K] [Fintype Coordinate] [Fintype K] [CharP K 2] [Nonempty Coordinate] (degrees : Coordinate → ℕ) (center direction : Coordinate → K) (width start blockWidth : ℕ) (fieldCard : Fintype.card K = 2 ^ width) (blockPositive : 0 < blockWidth) (blockFits : start + blockWidth ≤ width) (dimensionFits : Fintype.card Coordinate ≤ 2 ^ blockWidth) (reduced : ∀ (coordinate : Coordinate), degrees coordinate < 2 ^ width) (zeroBlock : CommonZeroBlock degrees start blockWidth) : (∑ parameter : K, monomialValue degrees fun (coordinate : Coordinate) => center coordinate + direction coordinate * parameter) = 0

Every retained monomial has parity zero on every affine line.

theorem Algebraic.MassProduction.HighRate.monomialValueSumPuncturedLine {K : Type u_1} {Coordinate : Type u_2} [Field K] [Fintype Coordinate] [Fintype K] [CharP K 2] [Nonempty Coordinate] (degrees : Coordinate → ℕ) (target : Coordinate → K) (direction : Projectivization K (Coordinate → K)) (width start blockWidth : ℕ) (fieldCard : Fintype.card K = 2 ^ width) (blockPositive : 0 < blockWidth) (blockFits : start + blockWidth ≤ width) (dimensionFits : Fintype.card Coordinate ≤ 2 ^ blockWidth) (reduced : ∀ (coordinate : Coordinate), degrees coordinate < 2 ^ width) (zeroBlock : CommonZeroBlock degrees start blockWidth) : monomialValue degrees target = ∑ point ∈ puncturedLine target direction, monomialValue degrees point

Retained monomials recover at any target by summing over any punctured projective line through it.