Tensor-product low-degree evaluation codes

This is the algebraic evaluation code used by the local-recovery gadget in the Boolean mass-production manuscript. Arbitrary data on a finite Cartesian grid is interpolated by a multivariate polynomial and evaluated over the whole ambient affine space.

The semantic node map below is a fixed noncomputable injection obtained from the finite cardinality equivalence. It proves the code theorem independently of representation. A later circuit layer must use the manuscript's concrete polynomial-basis field representation and prove its indexing costs.

noncomputable def Algebraic.MassProduction.gridBasis {K : Type u_1} {Index : Type u_2} {Coordinate : Type u_3} [Field K] [Fintype Index] [DecidableEq Index] [Fintype Coordinate] (nodes : Index → K) (point : Coordinate → Index) : MvPolynomial Coordinate K

The tensor-product Lagrange basis polynomial for one grid point.

Equations

• Algebraic.MassProduction.gridBasis nodes point = ∏ coordinate : Coordinate, (Polynomial.toMvPolynomial coordinate) (Lagrange.basis Finset.univ nodes (point coordinate))

noncomputable def Algebraic.MassProduction.gridInterpolate {K : Type u_1} {Index : Type u_2} {Coordinate : Type u_3} [Field K] [Fintype Index] [DecidableEq Index] [Fintype Coordinate] [DecidableEq Coordinate] (nodes : Index → K) (message : (Coordinate → Index) → K) : MvPolynomial Coordinate K

Interpolate an arbitrary field-valued message on a Cartesian grid.

Equations

• Algebraic.MassProduction.gridInterpolate nodes message = ∑ point : Coordinate → Index, MvPolynomial.C (message point) * Algebraic.MassProduction.gridBasis nodes point

noncomputable def Algebraic.MassProduction.evaluationCode {K : Type u_1} {Index : Type u_2} {Coordinate : Type u_3} [Field K] [Fintype Index] [DecidableEq Index] [Fintype Coordinate] [DecidableEq Coordinate] (nodes : Index → K) (message : (Coordinate → Index) → K) (point : Coordinate → K) : K

Evaluate the tensor-grid interpolant at an ambient point.

Equations

• Algebraic.MassProduction.evaluationCode nodes message point = (MvPolynomial.eval point) (Algebraic.MassProduction.gridInterpolate nodes message)

def Algebraic.MassProduction.resourceGridWidth (fieldCard dimension : ℕ) : ℕ

The paper's grid width floor ((q - 1) / dimension).

Equations

• Algebraic.MassProduction.resourceGridWidth fieldCard dimension = (fieldCard - 1) / dimension

noncomputable def Algebraic.MassProduction.resourceNodes (K : Type u_1) [Fintype K] (dimension : ℕ) : Fin (resourceGridWidth (Fintype.card K) dimension) → K

A fixed semantic injection of interpolation-node indices into a finite field. This definition is intentionally noncomputable; concrete field indexing belongs to the circuit-realization layer.

Equations

• Algebraic.MassProduction.resourceNodes K dimension point = (Fintype.equivFin K).symm ⟨↑point, ⋯⟩

noncomputable def Algebraic.MassProduction.paperEvaluationCode (K : Type u_1) [Field K] [Fintype K] (dimension : ℕ) (message : (Fin dimension → Fin (resourceGridWidth (Fintype.card K) dimension)) → K) (point : Fin dimension → K) : K

The paper-parameterized systematic resource code.

Equations

• Algebraic.MassProduction.paperEvaluationCode K dimension message point = Algebraic.MassProduction.evaluationCode (Algebraic.MassProduction.resourceNodes K dimension) message point

theorem Algebraic.MassProduction.eval_gridBasis_self {K : Type u_1} {Index : Type u_2} {Coordinate : Type u_3} [Field K] [Fintype Index] [DecidableEq Index] [Fintype Coordinate] (nodes : Index → K) (nodesInjective : Function.Injective nodes) (point : Coordinate → Index) : (MvPolynomial.eval (nodes ∘ point)) (gridBasis nodes point) = 1

A tensor Lagrange basis polynomial evaluates to one at its own grid point.

theorem Algebraic.MassProduction.eval_gridBasis_of_ne {K : Type u_1} {Index : Type u_2} {Coordinate : Type u_3} [Field K] [Fintype Index] [DecidableEq Index] [Fintype Coordinate] (nodes : Index → K) (target point : Coordinate → Index) (different : target ≠ point) : (MvPolynomial.eval (nodes ∘ target)) (gridBasis nodes point) = 0

A tensor Lagrange basis polynomial vanishes at every other grid point.

theorem Algebraic.MassProduction.evaluationCode_on_grid {K : Type u_1} {Index : Type u_2} {Coordinate : Type u_3} [Field K] [Fintype Index] [DecidableEq Index] [Fintype Coordinate] [DecidableEq Coordinate] (nodes : Index → K) (nodesInjective : Function.Injective nodes) (message : (Coordinate → Index) → K) (target : Coordinate → Index) : evaluationCode nodes message (nodes ∘ target) = message target

The evaluation code agrees with the supplied message at every grid point.

theorem Algebraic.MassProduction.gridInterpolate_add {K : Type u_1} {Index : Type u_2} {Coordinate : Type u_3} [Field K] [Fintype Index] [DecidableEq Index] [Fintype Coordinate] [DecidableEq Coordinate] (nodes : Index → K) (left right : (Coordinate → Index) → K) : gridInterpolate nodes (left + right) = gridInterpolate nodes left + gridInterpolate nodes right

Grid interpolation preserves message addition.

theorem Algebraic.MassProduction.gridInterpolate_smul {K : Type u_1} {Index : Type u_2} {Coordinate : Type u_3} [Field K] [Fintype Index] [DecidableEq Index] [Fintype Coordinate] [DecidableEq Coordinate] (nodes : Index → K) (scalar : K) (message : (Coordinate → Index) → K) : gridInterpolate nodes (scalar • message) = scalar • gridInterpolate nodes message

Grid interpolation preserves field scalar multiplication.

theorem Algebraic.MassProduction.evaluationCode_injective {K : Type u_1} {Index : Type u_2} {Coordinate : Type u_3} [Field K] [Fintype Index] [DecidableEq Index] [Fintype Coordinate] [DecidableEq Coordinate] (nodes : Index → K) (nodesInjective : Function.Injective nodes) : Function.Injective fun (message : (Coordinate → Index) → K) (point : Coordinate → K) => evaluationCode nodes message point

Distinct grid messages have distinct ambient evaluation tables.

theorem Algebraic.MassProduction.totalDegree_gridBasis_le {K : Type u_1} {Index : Type u_2} {Coordinate : Type u_3} [Field K] [Fintype Index] [DecidableEq Index] [Fintype Coordinate] (nodes : Index → K) (point : Coordinate → Index) : (gridBasis nodes point).totalDegree ≤ Fintype.card Coordinate * (Fintype.card Index - 1)

A tensor basis polynomial has total degree at most the number of coordinates times one less than the grid width.

theorem Algebraic.MassProduction.totalDegree_gridInterpolate_le {K : Type u_1} {Index : Type u_2} {Coordinate : Type u_3} [Field K] [Fintype Index] [DecidableEq Index] [Fintype Coordinate] [DecidableEq Coordinate] (nodes : Index → K) (message : (Coordinate → Index) → K) : (gridInterpolate nodes message).totalDegree ≤ Fintype.card Coordinate * (Fintype.card Index - 1)

The complete tensor-grid interpolant obeys the same total-degree budget.

theorem Algebraic.MassProduction.card_evaluationCodeDomain (K : Type u_1) (Coordinate : Type u_2) [Fintype K] [Fintype Coordinate] [DecidableEq Coordinate] : Fintype.card (Coordinate → K) = Fintype.card K ^ Fintype.card Coordinate

The ambient evaluation table has |K| ^ |Coordinate| coordinates.

theorem Algebraic.MassProduction.card_evaluationCodeMessageDomain (Index : Type u_1) (Coordinate : Type u_2) [Fintype Index] [Fintype Coordinate] [DecidableEq Coordinate] : Fintype.card (Coordinate → Index) = Fintype.card Index ^ Fintype.card Coordinate

The message grid has |Index| ^ |Coordinate| positions.

theorem Algebraic.MassProduction.resourceNodes_injective (K : Type u_1) [Fintype K] (dimension : ℕ) : Function.Injective (resourceNodes K dimension)

The fixed semantic node map is injective.

theorem Algebraic.MassProduction.resourceGridWidth_degree_lt (fieldCard dimension : ℕ) (fieldNontrivial : 2 ≤ fieldCard) (dimensionPositive : 0 < dimension) : dimension * (resourceGridWidth fieldCard dimension - 1) < fieldCard - 1

The grid-width choice satisfies the strict affine-line degree bound.

theorem Algebraic.MassProduction.paperEvaluationCode_on_grid (K : Type u_1) [Field K] [Fintype K] (dimension : ℕ) (message : (Fin dimension → Fin (resourceGridWidth (Fintype.card K) dimension)) → K) (target : Fin dimension → Fin (resourceGridWidth (Fintype.card K) dimension)) : paperEvaluationCode K dimension message (resourceNodes K dimension ∘ target) = message target

The paper-parameterized code is systematic on its interpolation grid.

theorem Algebraic.MassProduction.evaluationCode_line_recovery_charTwo {K : Type u_1} {Index : Type u_2} {Coordinate : Type u_3} [Fintype K] [Field K] [DecidableEq K] [CharP K 2] [Fintype Index] [DecidableEq Index] [Fintype Coordinate] [DecidableEq Coordinate] (nodes : Index → K) (message : (Coordinate → Index) → K) (degree : Fintype.card Coordinate * (Fintype.card Index - 1) < Fintype.card K - 1) (target direction : Coordinate → K) : evaluationCode nodes message target = ∑ parameter ∈ Finset.univ.erase 0, evaluationCode nodes message fun (index : Coordinate) => target index + direction index * parameter

Under the exact tensor-degree inequality, every code symbol is the sum of the other symbols on any affine line through it.

theorem Algebraic.MassProduction.paperEvaluationCode_line_recovery (K : Type u_1) [Fintype K] [Field K] [DecidableEq K] [CharP K 2] (dimension : ℕ) (dimensionPositive : 0 < dimension) (message : (Fin dimension → Fin (resourceGridWidth (Fintype.card K) dimension)) → K) (target direction : Fin dimension → K) : paperEvaluationCode K dimension message target = ∑ parameter ∈ Finset.univ.erase 0, paperEvaluationCode K dimension message fun (index : Fin dimension) => target index + direction index * parameter

The paper's grid-width choice gives affine-line recovery in every positive dimension.