One-variable line polynomials for the low individual degree test

Polynomial answer types attached to axis-parallel and diagonal lines.

References

• references/ldt-paper/test_definition.tex
• blueprint/src/chapter/ch02_test.tex

def MIPStarRE.LDT.HasLowIndividualDegree (params : Parameters) [FieldModel params.q] (g : Point params → Fq params) : Prop

A coded function has low individual degree when it is represented by an actual multivariate polynomial over the chosen field model whose degree in each variable is at most d.

Equations

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

def MIPStarRE.LDT.HasUnivariateDegreeAtMost (params : Parameters) [FieldModel params.q] (bound : ℕ) (f : Fq params → Fq params) : Prop

A coded univariate function has degree at most bound when it is represented by an actual polynomial over the chosen field model of degree at most bound.

Equations

• MIPStarRE.LDT.HasUnivariateDegreeAtMost params bound f = ∃ (p : MIPStarRE.LDT.LinePolynomialModel params), Polynomial.natDegree p ≤ bound ∧ f = MIPStarRE.LDT.evalLinePolynomialModel params p

theorem MIPStarRE.LDT.natDegree_comp_C_add_X_le {params : Parameters} [FieldModel params.q] (p : LinePolynomialModel params) (a : Scalar params) {n : ℕ} (hp : Polynomial.natDegree p ≤ n) : (Polynomial.comp p (Polynomial.C a + Polynomial.X)).natDegree ≤ n

Composing with the degree-one translation C a + X preserves natDegree bounds. Shared degree bookkeeping for the reparamAt reparametrizations below.

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

Axis-parallel line answers are genuine univariate degree-d polynomials.

• poly : LinePolynomialModel params
• degreeBounded : Polynomial.natDegree self.poly ≤ params.d

@[instance_reducible]

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

Equations

• MIPStarRE.LDT.instInhabitedAxisLinePolynomial = { default := { poly := 0, degreeBounded := ⋯ } }

noncomputable def MIPStarRE.LDT.AxisLinePolynomial.toFun {params : Parameters} [FieldModel params.q] (f : AxisLinePolynomial params) : Fq params → Fq params

Evaluation of an axis-line answer on the line parameter.

Equations

• f.toFun = MIPStarRE.LDT.evalLinePolynomialModel params f.poly

@[instance_reducible]

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

Equations

• MIPStarRE.LDT.AxisLinePolynomial.instCoeFunForallFq = { coe := MIPStarRE.LDT.AxisLinePolynomial.toFun }

theorem MIPStarRE.LDT.AxisLinePolynomial.eq_C_coeff_zero_of_degree_zero {params : Parameters} [FieldModel params.q] (f : AxisLinePolynomial params) (hd : params.d = 0) : f.poly = Polynomial.C (Polynomial.coeff f.poly 0)

A degree-zero axis-line answer is a constant univariate polynomial.

Lean-only helper for the degree-zero branch of thm:ld-pasting; the source context is references/ldt-paper/ld-pasting.tex:12-55, where the boundary case d = 0 must be handled without adding 0 < d to the theorem.

theorem MIPStarRE.LDT.AxisLinePolynomial.apply_eq_apply_of_degree_zero {params : Parameters} [FieldModel params.q] (f : AxisLinePolynomial params) (hd : params.d = 0) (t s : Fq params) : f.toFun t = f.toFun s

A degree-zero axis-line answer has the same value at all line parameters.

Lean-only helper for the degree-zero branch of thm:ld-pasting; this is the vertical-line analogue of Polynomial.apply_eq_apply_of_degree_zero.

theorem MIPStarRE.LDT.AxisLinePolynomial.ext {params : Parameters} [FieldModel params.q] {f g : AxisLinePolynomial params} (hpoly : f.poly = g.poly) : f = g

theorem MIPStarRE.LDT.AxisLinePolynomial.ext_iff {params : Parameters} [FieldModel params.q] {f g : AxisLinePolynomial params} : f = g ↔ f.poly = g.poly

noncomputable def MIPStarRE.LDT.AxisLinePolynomial.reparamAt {params : Parameters} [FieldModel params.q] (f : AxisLinePolynomial params) (t : Fq params) : AxisLinePolynomial params

Reparametrize an axis-line answer by translating the line parameter.

Equations

• f.reparamAt t = { poly := Polynomial.comp f.poly (Polynomial.C (MIPStarRE.LDT.decodeScalar t) + Polynomial.X), degreeBounded := ⋯ }

@[simp]

theorem MIPStarRE.LDT.AxisLinePolynomial.reparamAt_apply {params : Parameters} [FieldModel params.q] (f : AxisLinePolynomial params) (t s : Fq params) : (f.reparamAt t).toFun s = f.toFun (addCoord t s)

@[simp]

theorem MIPStarRE.LDT.AxisLinePolynomial.reparamAt_apply_zero {params : Parameters} [FieldModel params.q] (f : AxisLinePolynomial params) (t : Fq params) : (f.reparamAt t).toFun zeroCoord = f.toFun t

@[simp]

theorem MIPStarRE.LDT.AxisLinePolynomial.reparamAt_zero {params : Parameters} [FieldModel params.q] (f : AxisLinePolynomial params) : f.reparamAt zeroCoord = f

@[simp]

theorem MIPStarRE.LDT.AxisLinePolynomial.reparamAt_default {params : Parameters} [FieldModel params.q] (t : Fq params) : default.reparamAt t = default

theorem MIPStarRE.LDT.AxisLinePolynomial.reparamAt_reparamAt {params : Parameters} [FieldModel params.q] (f : AxisLinePolynomial params) (t s : Fq params) : (f.reparamAt t).reparamAt s = f.reparamAt (addCoord t s)

noncomputable def MIPStarRE.LDT.AxisLinePolynomial.reparamAtEquiv {params : Parameters} [FieldModel params.q] (t : Fq params) : AxisLinePolynomial params ≃ AxisLinePolynomial params

Reparametrization by translation is an equivalence on axis-line answers.

Equations

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

theorem MIPStarRE.LDT.AxisLinePolynomial.hasUnivariateDegreeAtMost {params : Parameters} [FieldModel params.q] (f : AxisLinePolynomial params) : HasUnivariateDegreeAtMost params params.d f.toFun

The stored polynomial really witnesses the advertised degree bound.

def MIPStarRE.LDT.AxisLinePolynomial.appendAtHeight (params : Parameters) [FieldModel params.q] (f : AxisLinePolynomial params) (_x : Fq params) : AxisLinePolynomial params.next

Extend an axis-line answer to the slice at height x.

Equations

• MIPStarRE.LDT.AxisLinePolynomial.appendAtHeight params f _x = { poly := f.poly, degreeBounded := ⋯ }

@[simp]

theorem MIPStarRE.LDT.AxisLinePolynomial.appendAtHeight_apply {params : Parameters} [FieldModel params.q] (f : AxisLinePolynomial params) (x t : Fq params) : (appendAtHeight params f x).toFun t = f.toFun t

@[simp]

theorem MIPStarRE.LDT.AxisLinePolynomial.appendAtHeight_reparamAt {params : Parameters} [FieldModel params.q] (f : AxisLinePolynomial params) (t x : Fq params) : appendAtHeight params (f.reparamAt t) x = (appendAtHeight params f x).reparamAt t

Slice extension commutes with translating the line parameter on axis-line answers.

@[simp]

theorem MIPStarRE.LDT.AxisLinePolynomial.reparamAtEquiv_symm_appendAtHeight {params : Parameters} [FieldModel params.q] (f : AxisLinePolynomial params) (t x : Fq params) : (reparamAtEquiv t).symm (appendAtHeight params f x) = appendAtHeight params ((reparamAtEquiv t).symm f) x

The inverse reparametrization equivalence commutes with slice extension on axis-line answers.

def MIPStarRE.LDT.AxisLinePolynomial.restrictAtHeight (params : Parameters) [FieldModel params.q] (f : AxisLinePolynomial params.next) (_x : Fq params) : AxisLinePolynomial params

Restrict an axis-line answer in m + 1 variables to the slice at height x.

Equations

• MIPStarRE.LDT.AxisLinePolynomial.restrictAtHeight params f _x = { poly := f.poly, degreeBounded := ⋯ }

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

Diagonal-line answers are genuine univariate degree-md polynomials.

• poly : LinePolynomialModel params
• degreeBounded : Polynomial.natDegree self.poly ≤ params.m * params.d

@[instance_reducible]

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

Equations

• MIPStarRE.LDT.instInhabitedDiagonalLinePolynomial = { default := { poly := 0, degreeBounded := ⋯ } }

noncomputable def MIPStarRE.LDT.DiagonalLinePolynomial.toFun {params : Parameters} [FieldModel params.q] (f : DiagonalLinePolynomial params) : Fq params → Fq params

Evaluation of a diagonal-line answer on the line parameter.

Equations

• f.toFun = MIPStarRE.LDT.evalLinePolynomialModel params f.poly

@[instance_reducible]

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

Equations

• MIPStarRE.LDT.DiagonalLinePolynomial.instCoeFunForallFq = { coe := MIPStarRE.LDT.DiagonalLinePolynomial.toFun }

theorem MIPStarRE.LDT.DiagonalLinePolynomial.ext {params : Parameters} [FieldModel params.q] {f g : DiagonalLinePolynomial params} (hpoly : f.poly = g.poly) : f = g

theorem MIPStarRE.LDT.DiagonalLinePolynomial.ext_iff {params : Parameters} [FieldModel params.q] {f g : DiagonalLinePolynomial params} : f = g ↔ f.poly = g.poly

noncomputable def MIPStarRE.LDT.DiagonalLinePolynomial.reparamAt {params : Parameters} [FieldModel params.q] (f : DiagonalLinePolynomial params) (t : Fq params) : DiagonalLinePolynomial params

Reparametrize a diagonal-line answer by translating the line parameter.

Concretely, the underlying univariate polynomial f.poly (over Scalar params in the chosen field model) is precomposed with X + C (decodeScalar t), i.e. the coefficients are shifted using genuine field addition on Scalar params — not the Fin q arithmetic on Fq params. Transporting back through encodeScalar gives the answer-level identity reparamAt f t s = f (addCoord t s) (see reparamAt_apply), where addCoord is field addition lifted through the coding FieldModel.equiv. Composition with a degree-one polynomial preserves the natDegree ≤ params.m * params.d bound.

This is the answer-level geometric fact behind rebasing a diagonal line at parameter t: the old parameter addCoord t s becomes the new parameter s.

Equations

• f.reparamAt t = { poly := Polynomial.comp f.poly (Polynomial.C (MIPStarRE.LDT.decodeScalar t) + Polynomial.X), degreeBounded := ⋯ }

@[simp]

theorem MIPStarRE.LDT.DiagonalLinePolynomial.reparamAt_apply {params : Parameters} [FieldModel params.q] (f : DiagonalLinePolynomial params) (t s : Fq params) : (f.reparamAt t).toFun s = f.toFun (addCoord t s)

@[simp]

theorem MIPStarRE.LDT.DiagonalLinePolynomial.reparamAt_apply_zero {params : Parameters} [FieldModel params.q] (f : DiagonalLinePolynomial params) (t : Fq params) : (f.reparamAt t).toFun zeroCoord = f.toFun t

@[simp]

theorem MIPStarRE.LDT.DiagonalLinePolynomial.reparamAt_zero {params : Parameters} [FieldModel params.q] (f : DiagonalLinePolynomial params) : f.reparamAt zeroCoord = f

@[simp]

theorem MIPStarRE.LDT.DiagonalLinePolynomial.reparamAt_default {params : Parameters} [FieldModel params.q] (t : Fq params) : default.reparamAt t = default

theorem MIPStarRE.LDT.DiagonalLinePolynomial.reparamAt_reparamAt {params : Parameters} [FieldModel params.q] (f : DiagonalLinePolynomial params) (t s : Fq params) : (f.reparamAt t).reparamAt s = f.reparamAt (addCoord t s)

noncomputable def MIPStarRE.LDT.DiagonalLinePolynomial.reparamAtEquiv {params : Parameters} [FieldModel params.q] (t : Fq params) : DiagonalLinePolynomial params ≃ DiagonalLinePolynomial params

Reparametrization by translation is an equivalence on diagonal-line answers.

Equations

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

theorem MIPStarRE.LDT.DiagonalLinePolynomial.hasUnivariateDegreeAtMost {params : Parameters} [FieldModel params.q] (f : DiagonalLinePolynomial params) : HasUnivariateDegreeAtMost params (params.m * params.d) f.toFun

The stored polynomial really witnesses the advertised degree bound.

def MIPStarRE.LDT.DiagonalLinePolynomial.appendAtHeight (params : Parameters) [FieldModel params.q] (f : DiagonalLinePolynomial params) (_x : Fq params) : DiagonalLinePolynomial params.next

Extend a diagonal-line answer to the slice at height x.

Equations

• MIPStarRE.LDT.DiagonalLinePolynomial.appendAtHeight params f _x = { poly := f.poly, degreeBounded := ⋯ }

@[simp]

theorem MIPStarRE.LDT.DiagonalLinePolynomial.appendAtHeight_reparamAt {params : Parameters} [FieldModel params.q] (f : DiagonalLinePolynomial params) (t x : Fq params) : appendAtHeight params (f.reparamAt t) x = (appendAtHeight params f x).reparamAt t

Slice extension commutes with translating the line parameter on diagonal-line answers.

@[simp]

theorem MIPStarRE.LDT.DiagonalLinePolynomial.reparamAtEquiv_symm_appendAtHeight {params : Parameters} [FieldModel params.q] (f : DiagonalLinePolynomial params) (t x : Fq params) : (reparamAtEquiv t).symm (appendAtHeight params f x) = appendAtHeight params ((reparamAtEquiv t).symm f) x

The inverse reparametrization equivalence commutes with slice extension on diagonal-line answers.

def MIPStarRE.LDT.DiagonalLinePolynomial.restrictAtHeight (params : Parameters) [FieldModel params.q] (f : DiagonalLinePolynomial params.next) (_x : Fq params) (hdegree : Polynomial.natDegree f.poly ≤ params.m * params.d) : DiagonalLinePolynomial params

Restrict a diagonal-line answer in m + 1 variables to the slice at height x. This interface now makes the stronger slice-wise degree requirement explicit.

Equations

• MIPStarRE.LDT.DiagonalLinePolynomial.restrictAtHeight params f _x hdegree = { poly := f.poly, degreeBounded := hdegree }

Paper-level diagonal-line answers

@[reducible, inline]

abbrev MIPStarRE.LDT.DiagonalLineAnswer (params : Parameters) : Type

Paper-level diagonal-line answers as functions on the line parameter.

The existing DiagonalLinePolynomial alphabet records a degree bound on the univariate line polynomial. For the slice restriction in inductive_step.tex, lines 436--455, the paper uses the underlying line function: restricting a slice-preserving ambient line is total at the function level, while it is not total on the current degree-bounded polynomial subtype.

Equations

• MIPStarRE.LDT.DiagonalLineAnswer params = (MIPStarRE.LDT.Fq params → MIPStarRE.LDT.Fq params)

def MIPStarRE.LDT.DiagonalLineAnswer.reparamAt {params : Parameters} [FieldModel params.q] (f : DiagonalLineAnswer params) (t : Fq params) : DiagonalLineAnswer params

Reparametrize a paper-level diagonal-line answer by translating the line parameter.

Equations

• f.reparamAt t s = f (MIPStarRE.LDT.addCoord t s)

@[simp]

theorem MIPStarRE.LDT.DiagonalLineAnswer.reparamAt_apply {params : Parameters} [FieldModel params.q] (f : DiagonalLineAnswer params) (t s : Fq params) : f.reparamAt t s = f (addCoord t s)

@[simp]

theorem MIPStarRE.LDT.DiagonalLineAnswer.reparamAt_zero {params : Parameters} [FieldModel params.q] (f : DiagonalLineAnswer params) : f.reparamAt zeroCoord = f

theorem MIPStarRE.LDT.DiagonalLineAnswer.reparamAt_reparamAt {params : Parameters} [FieldModel params.q] (f : DiagonalLineAnswer params) (t s : Fq params) : (f.reparamAt t).reparamAt s = f.reparamAt (addCoord t s)

def MIPStarRE.LDT.DiagonalLineAnswer.reparamAtEquiv {params : Parameters} [FieldModel params.q] (t : Fq params) : DiagonalLineAnswer params ≃ DiagonalLineAnswer params

Reparametrization by translation is an equivalence on paper-level line answers.

Equations

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

def MIPStarRE.LDT.DiagonalLineAnswer.appendAtHeight (params : Parameters) (f : DiagonalLineAnswer params) (_x : Fq params) : DiagonalLineAnswer params.next

Extend a paper-level diagonal-line answer to the slice at height x.

Equations

• MIPStarRE.LDT.DiagonalLineAnswer.appendAtHeight params f _x t = f t

def MIPStarRE.LDT.DiagonalLineAnswer.restrictAtHeight (params : Parameters) (f : DiagonalLineAnswer params.next) (_x : Fq params) : DiagonalLineAnswer params

Restrict a paper-level ambient diagonal-line answer to the slice at height x.

Equations

• MIPStarRE.LDT.DiagonalLineAnswer.restrictAtHeight params f _x t = f t

@[simp]

theorem MIPStarRE.LDT.DiagonalLineAnswer.appendAtHeight_apply (params : Parameters) (f : DiagonalLineAnswer params) (x : Fq params) (t : Fq params.next) : appendAtHeight params f x t = f t

@[simp]

theorem MIPStarRE.LDT.DiagonalLineAnswer.restrictAtHeight_apply (params : Parameters) (f : DiagonalLineAnswer params.next) (x t : Fq params) : restrictAtHeight params f x t = f t

@[simp]

theorem MIPStarRE.LDT.DiagonalLineAnswer.appendAtHeight_reparamAt {params : Parameters} [FieldModel params.q] (f : DiagonalLineAnswer params) (t x : Fq params) : appendAtHeight params (f.reparamAt t) x = (appendAtHeight params f x).reparamAt t

@[simp]

theorem MIPStarRE.LDT.DiagonalLineAnswer.reparamAtEquiv_symm_appendAtHeight {params : Parameters} [FieldModel params.q] (f : DiagonalLineAnswer params) (t x : Fq params) : (reparamAtEquiv t).symm (appendAtHeight params f x) = appendAtHeight params ((reparamAtEquiv t).symm f) x

noncomputable def MIPStarRE.LDT.DiagonalLinePolynomial.toAnswer {params : Parameters} [FieldModel params.q] (f : DiagonalLinePolynomial params) : DiagonalLineAnswer params

Forget the degree witness and view a diagonal-line polynomial as its paper-level line answer function.

Equations

• f.toAnswer t = f.toFun t

@[simp]

theorem MIPStarRE.LDT.DiagonalLinePolynomial.toAnswer_apply {params : Parameters} [FieldModel params.q] (f : DiagonalLinePolynomial params) (t : Fq params) : f.toAnswer t = f.toFun t

@[simp]

theorem MIPStarRE.LDT.DiagonalLinePolynomial.toAnswer_reparamAt {params : Parameters} [FieldModel params.q] (f : DiagonalLinePolynomial params) (t : Fq params) : (f.reparamAt t).toAnswer = f.toAnswer.reparamAt t

@[simp]

theorem MIPStarRE.LDT.DiagonalLinePolynomial.toAnswer_appendAtHeight {params : Parameters} [FieldModel params.q] (f : DiagonalLinePolynomial params) (x : Fq params) : (appendAtHeight params f x).toAnswer = DiagonalLineAnswer.appendAtHeight params f.toAnswer x