Low-individual-degree polynomials for the low individual degree test

Multivariate low-degree polynomial objects and their restrictions.

Note: this module contributes declarations to the comparator statement closure of mainFormal, which must elaborate in the same environment as the Mathlib-only Challenge.lean. Keep the full import Mathlib; do not narrow it. See docs/comparator.md, "Environment alignment".

structure MIPStarRE.LDT.Polynomial (params : Parameters) [FieldModel params.q] : Type u_1

Global low-individual-degree polynomial outcomes.

• poly : PolynomialModel params
• lowIndividualDegree (i : Fin params.m) : MvPolynomial.degreeOf i self.poly ≤ params.d

theorem MIPStarRE.LDT.degreeOf_rename_embedCoord_lastCoord (params : Parameters) [FieldModel params.q] (p : PolynomialModel params) : MvPolynomial.degreeOf (lastCoord params) ((MvPolynomial.rename (embedCoord params)) p) = 0

Renaming a polynomial along the old-coordinate inclusion does not introduce the appended last coordinate.

noncomputable def MIPStarRE.LDT.Polynomial.toFun {params : Parameters} [FieldModel params.q] (g : Polynomial params) : Point params → Fq params

Evaluation of the stored multivariate polynomial on a coded point.

Equations

• g.toFun = MIPStarRE.LDT.evalPolynomialModel params g.poly

@[instance_reducible]

noncomputable instance MIPStarRE.LDT.Polynomial.instCoeFunForallPointFq {params : Parameters} [FieldModel params.q] : CoeFun (Polynomial params) fun (x : Polynomial params) => Point params → Fq params

Equations

• MIPStarRE.LDT.Polynomial.instCoeFunForallPointFq = { coe := MIPStarRE.LDT.Polynomial.toFun }

theorem MIPStarRE.LDT.Polynomial.hasLowIndividualDegree {params : Parameters} [FieldModel params.q] (g : Polynomial params) : HasLowIndividualDegree params g.toFun

The stored polynomial indeed certifies low individual degree.

noncomputable def MIPStarRE.LDT.Polynomial.const (params : Parameters) [FieldModel params.q] (a : Fq params) : Polynomial params

The constant polynomial with value a.

Equations

• MIPStarRE.LDT.Polynomial.const params a = { poly := MvPolynomial.C (MIPStarRE.LDT.decodeScalar a), lowIndividualDegree := ⋯ }

@[instance_reducible]

noncomputable instance MIPStarRE.LDT.Polynomial.instInhabited {params : Parameters} [FieldModel params.q] : Inhabited (Polynomial params)

Equations

• MIPStarRE.LDT.Polynomial.instInhabited = { default := MIPStarRE.LDT.Polynomial.const params default }

@[simp]

theorem MIPStarRE.LDT.Polynomial.const_apply (params : Parameters) [FieldModel params.q] (a : Fq params) (u : Point params) : (const params a).toFun u = a

The constant polynomial evaluates to its prescribed value.

theorem MIPStarRE.LDT.Polynomial.totalDegree_le_mul_degree (params : Parameters) [FieldModel params.q] (g : Polynomial params) : MvPolynomial.totalDegree g.poly ≤ params.m * params.d

The total degree of a low-individual-degree polynomial is bounded by m * d.

theorem MIPStarRE.LDT.Polynomial.eq_C_coeff_zero_of_degree_zero (params : Parameters) [FieldModel params.q] (g : Polynomial params) (hd : params.d = 0) : g.poly = MvPolynomial.C (MvPolynomial.coeff 0 g.poly)

A low-individual-degree polynomial with degree bound 0 is constant.

theorem MIPStarRE.LDT.Polynomial.apply_eq_apply_of_degree_zero (params : Parameters) [FieldModel params.q] (g : Polynomial params) (hd : params.d = 0) (u v : Point params) : g.toFun u = g.toFun v

A low-individual-degree polynomial with degree bound 0 has the same value at every two points.

theorem MIPStarRE.LDT.Polynomial.degreeOf_rename_embedCoord_le (params : Parameters) [FieldModel params.q] (g : Polynomial params) (i : Fin params.next.m) : MvPolynomial.degreeOf i ((MvPolynomial.rename (embedCoord params)) g.poly) ≤ params.d

Renaming a low-degree polynomial along the coordinate embedding preserves the low-individual-degree bound in m + 1 variables.

noncomputable def MIPStarRE.LDT.Polynomial.appendAtHeight (params : Parameters) [FieldModel params.q] (g : Polynomial params) (_x : Fq params) : Polynomial params.next

Extend a global polynomial to the slice at height x by ignoring the new variable.

Equations

• MIPStarRE.LDT.Polynomial.appendAtHeight params g _x = { poly := (MvPolynomial.rename (MIPStarRE.LDT.embedCoord params)) g.poly, lowIndividualDegree := ⋯ }

@[simp]

theorem MIPStarRE.LDT.Polynomial.appendAtHeight_apply_appendPoint (params : Parameters) [FieldModel params.q] (g : Polynomial params) (x : Fq params) (u : Point params) (y : Fq params) : (appendAtHeight params g x).toFun (appendPoint params u y) = g.toFun u

Evaluating an old polynomial after appending a new coordinate ignores the appended coordinate.

noncomputable def MIPStarRE.LDT.Polynomial.restrictAtHeightCoordinateMap (params : Parameters) [FieldModel params.q] (x : Fq params) : Fin params.next.m → PolynomialModel params

Coordinate map for restricting a polynomial in m+1 variables to the slice X_m = x.

Equations

• MIPStarRE.LDT.Polynomial.restrictAtHeightCoordinateMap params x i = if h : ↑i < params.m then MvPolynomial.X ⟨↑i, h⟩ else MvPolynomial.C (MIPStarRE.LDT.decodeScalar x)

theorem MIPStarRE.LDT.Polynomial.degreeOf_eval₂Hom_restrictAtHeightCoordinateMap_le (params : Parameters) [FieldModel params.q] (g : Polynomial params.next) (x : Fq params) (i : Fin params.m) : MvPolynomial.degreeOf i ((MvPolynomial.eval₂Hom MvPolynomial.C (restrictAtHeightCoordinateMap params x)) g.poly) ≤ params.d

Restricting a polynomial to a coordinate slice via eval₂Hom preserves the low-individual-degree bound: each variable's degree stays at most d.

noncomputable def MIPStarRE.LDT.Polynomial.restrictAtHeight (params : Parameters) [FieldModel params.q] (g : Polynomial params.next) (x : Fq params) : Polynomial params

Restrict a global polynomial in m + 1 variables to the slice at height x.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.Polynomial.axisCoordinatePolynomial (params : Parameters) [FieldModel params.q] (ℓ : AxisParallelLine params) : Fin params.m → LinePolynomialModel params

Coordinate polynomial for restricting to an axis-parallel affine line.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPStarRE.LDT.Polynomial.natDegree_eval₂Hom_axisCoordinatePolynomial_le (params : Parameters) [FieldModel params.q] (g : Polynomial params) (ℓ : AxisParallelLine params) : ((MvPolynomial.eval₂Hom Polynomial.C (axisCoordinatePolynomial params ℓ)) g.poly).natDegree ≤ params.d

Restricting a low-degree polynomial to an axis-parallel line via eval₂Hom yields a univariate polynomial whose natural degree is at most d.

noncomputable def MIPStarRE.LDT.Polynomial.restrictToAxisParallelLine (params : Parameters) [FieldModel params.q] (g : Polynomial params) (ℓ : AxisParallelLine params) : AxisLinePolynomial params

Restrict a global polynomial to an axis-parallel line.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPStarRE.LDT.Polynomial.restrictToAxisParallelLine_apply (params : Parameters) [FieldModel params.q] (g : Polynomial params) (ℓ : AxisParallelLine params) (t : Fq params) : (restrictToAxisParallelLine params g ℓ).toFun t = g.toFun (ℓ.pointAt t)

Evaluating an axis-parallel restriction agrees with evaluating the original polynomial at the corresponding point on the line.

noncomputable def MIPStarRE.LDT.Polynomial.diagonalCoordinatePolynomial (params : Parameters) [FieldModel params.q] (ℓ : DiagonalLine params) : Fin params.m → LinePolynomialModel params

Coordinate polynomial for restricting to a diagonal affine line.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPStarRE.LDT.Polynomial.natDegree_eval₂Hom_diagonalCoordinatePolynomial_le (params : Parameters) [FieldModel params.q] (g : Polynomial params) (ℓ : DiagonalLine params) : ((MvPolynomial.eval₂Hom Polynomial.C (diagonalCoordinatePolynomial params ℓ)) g.poly).natDegree ≤ params.m * params.d

Restricting a low-degree polynomial to a diagonal line via eval₂Hom yields a univariate polynomial whose natural degree is at most m · d.

noncomputable def MIPStarRE.LDT.Polynomial.restrictToDiagonalLine (params : Parameters) [FieldModel params.q] (g : Polynomial params) (ℓ : DiagonalLine params) : DiagonalLinePolynomial params

Restrict a global polynomial to a diagonal line.

Equations

• One or more equations did not get rendered due to their size.