Basic parameters and scalar infrastructure for the low individual degree test

Core parameter data, finite-field models, and coordinate arithmetic.

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".

@[reducible, inline]

abbrev MIPStarRE.LDT.Error : Type

Equations

• MIPStarRE.LDT.Error = ℝ

inductive MIPStarRE.LDT.Role : Type

• A : Role
• B : Role

@[instance_reducible]

instance MIPStarRE.LDT.instDecidableEqRole : DecidableEq Role

Equations

• MIPStarRE.LDT.instDecidableEqRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance MIPStarRE.LDT.instReprRole : Repr Role

Equations

• MIPStarRE.LDT.instReprRole = { reprPrec := MIPStarRE.LDT.instReprRole.repr }

def MIPStarRE.LDT.instReprRole.repr : Role → ℕ → Std.Format

Equations

• MIPStarRE.LDT.instReprRole.repr MIPStarRE.LDT.Role.A prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MIPStarRE.LDT.Role.A")).group prec✝
• MIPStarRE.LDT.instReprRole.repr MIPStarRE.LDT.Role.B prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MIPStarRE.LDT.Role.B")).group prec✝

@[instance_reducible]

instance MIPStarRE.LDT.instInhabitedRole : Inhabited Role

Equations

• MIPStarRE.LDT.instInhabitedRole = { default := MIPStarRE.LDT.instInhabitedRole.default }

@[instance_reducible]

instance MIPStarRE.LDT.instFintypeRole : Fintype Role

Equations

• MIPStarRE.LDT.instFintypeRole = { elems := { val := ↑MIPStarRE.LDT.Role.enumList, nodup := MIPStarRE.LDT.Role.enumList_nodup }, complete := MIPStarRE.LDT.instFintypeRole._proof_1 }

def MIPStarRE.LDT.Role.other : Role → Role

Equations

• MIPStarRE.LDT.Role.A.other = MIPStarRE.LDT.Role.B
• MIPStarRE.LDT.Role.B.other = MIPStarRE.LDT.Role.A

@[simp]

theorem MIPStarRE.LDT.Role.other_other (r : Role) : r.other.other = r

structure MIPStarRE.LDT.Parameters : Type

Parameters for the (m,q,d) low individual degree test.

Besides the usual positivity assumptions, we bundle the paper-faithful witness that q = p^n is a prime power.

• m : ℕ
• q : ℕ
• d : ℕ
• hm : 0 < self.m
• hq : 0 < self.q

  Kept as a compatibility field so existing positivity proofs can continue to use params.hq; it is derivable from hqPrimePower.

• hqPrimePower : ∃ (p : ℕ) (n : ℕ), Nat.Prime p ∧ 0 < n ∧ self.q = p ^ n

  Paper-faithful witness that q is a prime power.

def MIPStarRE.LDT.instDecidableEqParameters.decEq (x✝ x✝¹ : Parameters) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance MIPStarRE.LDT.instDecidableEqParameters : DecidableEq Parameters

Equations

• MIPStarRE.LDT.instDecidableEqParameters = MIPStarRE.LDT.instDecidableEqParameters.decEq

theorem MIPStarRE.LDT.Parameters.q_pos_of_primePower {q : ℕ} (hqPrimePower : ∃ (p : ℕ) (n : ℕ), Nat.Prime p ∧ 0 < n ∧ q = p ^ n) : 0 < q

Any number presented as a prime power is automatically positive.

theorem MIPStarRE.LDT.Parameters.prime_primePower {q : ℕ} (hqPrime : Nat.Prime q) : ∃ (p : ℕ) (n : ℕ), Nat.Prime p ∧ 0 < n ∧ q = p ^ n

Prime numbers are prime powers of exponent 1.

def MIPStarRE.LDT.Parameters.ofPrimePower (m q d p n : ℕ) (hm : 0 < m) (hp : Nat.Prime p) (hn : 0 < n) (hq : q = p ^ n) : Parameters

Build parameters from explicit prime-power data q = p^n.

Equations

• MIPStarRE.LDT.Parameters.ofPrimePower m q d p n hm hp hn hq = { m := m, q := q, d := d, hm := hm, hq := ⋯, hqPrimePower := ⋯ }

def MIPStarRE.LDT.Parameters.ofPrime (m q d : ℕ) (hm : 0 < m) (hqPrime : Nat.Prime q) : Parameters

Build parameters when q itself is prime.

Equations

• MIPStarRE.LDT.Parameters.ofPrime m q d hm hqPrime = { m := m, q := q, d := d, hm := hm, hq := ⋯, hqPrimePower := ⋯ }

def MIPStarRE.LDT.Parameters.ofTwo (m d : ℕ) (hm : 0 < m) : Parameters

Convenience constructor for the ubiquitous binary field.

Equations

• MIPStarRE.LDT.Parameters.ofTwo m d hm = MIPStarRE.LDT.Parameters.ofPrime m 2 d hm Nat.prime_two

theorem MIPStarRE.LDT.Parameters.two_le_q (params : Parameters) : 2 ≤ params.q

Paper finite fields have at least two elements: q = p^n with p prime and 0 < n (see preliminaries.tex, lines 17--19 and 89--93).

theorem MIPStarRE.LDT.Parameters.one_lt_q (params : Parameters) : 1 < params.q

The field-size parameter is strictly larger than 1.

theorem MIPStarRE.LDT.Parameters.q_cast_pos (params : Parameters) : 0 < ↑params.q

Positivity of the field-size parameter after casting to the repository's real-valued error scalar type.

@[instance_reducible]

instance MIPStarRE.LDT.instInhabitedParameters : Inhabited Parameters

Equations

• MIPStarRE.LDT.instInhabitedParameters = { default := MIPStarRE.LDT.Parameters.ofTwo 1 0 MIPStarRE.LDT.instInhabitedParameters._proof_1 }

def MIPStarRE.LDT.Parameters.next (params : Parameters) : Parameters

The successor test obtained by appending one coordinate.

Equations

• params.next = { m := params.m + 1, q := params.q, d := params.d, hm := ⋯, hq := ⋯, hqPrimePower := ⋯ }

def MIPStarRE.LDT.Parameters.previous (params : Parameters) (hm : 1 < params.m) : Parameters

The predecessor parameters obtained by removing the last coordinate from a non-base ambient dimension.

This is the inverse construction to Parameters.next on the data fields. The proof fields are inherited from the original parameter bundle, so the inverse is propositional rather than definitional.

Equations

• params.previous hm = { m := params.m - 1, q := params.q, d := params.d, hm := ⋯, hq := ⋯, hqPrimePower := ⋯ }

theorem MIPStarRE.LDT.Parameters.previous_next_eq (params : Parameters) (hm : 1 < params.m) : (params.previous hm).next = params

Removing the last coordinate and then applying Parameters.next recovers the original non-base parameters.

structure MIPStarRE.LDT.Parameters.SuccessorDecomposition (params : Parameters) : Type

A bundled predecessor for a parameter set known to be a successor dimension.

• pred : Parameters

  The predecessor parameter bundle.

• next_eq : self.pred.next = params

  The predecessor's successor is the original parameter bundle.

def MIPStarRE.LDT.Parameters.successorDecompositionOfOneLtM (params : Parameters) (hm : 1 < params.m) : params.SuccessorDecomposition

Every parameter bundle of dimension strictly larger than one has a bundled predecessor whose successor is propositionally equal to the original bundle.

Equations

• params.successorDecompositionOfOneLtM hm = { pred := params.previous hm, next_eq := ⋯ }

theorem MIPStarRE.LDT.Parameters.one_lt_m_of_ne_one (params : Parameters) (hm_ne_one : params.m ≠ 1) : 1 < params.m

A positive dimension that is not the base dimension is strictly larger than one.

def MIPStarRE.LDT.Parameters.successorDecompositionOfNeOne (params : Parameters) (hm_ne_one : params.m ≠ 1) : params.SuccessorDecomposition

Non-base parameters have a bundled predecessor decomposition.

Equations

• params.successorDecompositionOfNeOne hm_ne_one = params.successorDecompositionOfOneLtM ⋯

instance MIPStarRE.LDT.instNeZeroNatQ {params : Parameters} : NeZero params.q

@[reducible, inline]

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

Equations

• MIPStarRE.LDT.Fq params = Fin params.q

@[reducible, inline]

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

Equations

• MIPStarRE.LDT.Point params = (Fin params.m → MIPStarRE.LDT.Fq params)

@[reducible, inline]

abbrev MIPStarRE.LDT.PointTuple (params : Parameters) (k : ℕ) : Type

Equations

• MIPStarRE.LDT.PointTuple params k = (Fin k → MIPStarRE.LDT.Fq params)

@[instance_reducible]

instance MIPStarRE.LDT.instInhabitedFinM {params : Parameters} : Inhabited (Fin params.m)

Equations

• MIPStarRE.LDT.instInhabitedFinM = { default := ⟨0, ⋯⟩ }

@[instance_reducible]

instance MIPStarRE.LDT.instInhabitedFq {params : Parameters} : Inhabited (Fq params)

Equations

• MIPStarRE.LDT.instInhabitedFq = { default := ⟨0, ⋯⟩ }

structure MIPStarRE.LDT.PrimePowerFieldSpec (params : Parameters) : Type

Prime-power metadata extracted from params.hqPrimePower, exposing the honest finite-field carrier GaloisField p n underlying the paper's notation F_q.

• p : ℕ
• n : ℕ
• pPrime : Nat.Prime self.p
• nPos : 0 < self.n
• cardEq : params.q = self.p ^ self.n

noncomputable def MIPStarRE.LDT.Parameters.primePowerFieldSpec (params : Parameters) : PrimePowerFieldSpec params

Recover the prime-power specification bundled inside Parameters.

Equations

• params.primePowerFieldSpec = ⋯.some

@[reducible, inline]

noncomputable abbrev MIPStarRE.LDT.HonestFq (params : Parameters) (spec : PrimePowerFieldSpec params) : Type

An honest finite field of order q, obtained from the prime-power witness bundled in Parameters.

Equations

• MIPStarRE.LDT.HonestFq params spec = GaloisField spec.p spec.n

class MIPStarRE.LDT.FieldModel (q : ℕ) : Type (u_1 + 1)

A bundled field model for the paper's F_q, together with a coding equivalence to the repository's finite carrier Fin q.

• K : Type u_1
• instField : Field (K q)
• instFintype : Fintype (K q)
• instDecidableEq : DecidableEq (K q)
• equiv : K q ≃ Fin q

@[simp]

theorem MIPStarRE.LDT.FieldModel.card (q : ℕ) [FieldModel q] : Fintype.card (K q) = q

The carrier bundled in a FieldModel q has exactly q elements, matching the paper's finite-field convention |F_q| = q (preliminaries.tex, lines 17--19).

theorem MIPStarRE.LDT.FieldModel.card_pos (q : ℕ) [FieldModel q] : 0 < Fintype.card (K q)

A bundled field model has a nonempty finite carrier.

theorem MIPStarRE.LDT.FieldModel.card_ne_zero (q : ℕ) [FieldModel q] : Fintype.card (K q) ≠ 0

The finite cardinality of a bundled field model is nonzero.

@[reducible]

noncomputable def MIPStarRE.LDT.PrimePowerFieldSpec.toFieldModel (params : Parameters) (spec : PrimePowerFieldSpec params) : FieldModel params.q

Build the honest field model from prime-power data.

Equations

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

@[instance_reducible, instance 100]

noncomputable instance MIPStarRE.LDT.instFieldModelQ (params : Parameters) : FieldModel params.q

The canonical field model associated to the paper-faithful prime-power data stored in params. Lean prefers larger numeric priorities, so this fallback uses 100 while the params.next transport below uses 200; that lets instance search reuse an already chosen model when one is available. This instance is noncomputable because the coding equivalence to Fin q is obtained from finite cardinality data, so declarations that discover it through typeclass search may also need to be marked noncomputable when they reduce the model.

Equations

• MIPStarRE.LDT.instFieldModelQ params = MIPStarRE.LDT.PrimePowerFieldSpec.toFieldModel params params.primePowerFieldSpec

@[instance_reducible, instance 200]

instance MIPStarRE.LDT.instFieldModelQNext {params : Parameters} [inst : FieldModel params.q] : FieldModel params.next.q

Reuse an already chosen field model for successor parameters. Since Lean prefers larger numeric priorities, this transport uses 200 so it is tried before the canonical fallback above.

Equations

• MIPStarRE.LDT.instFieldModelQNext = id inst

@[reducible, inline]

abbrev MIPStarRE.LDT.Scalar (params : Parameters) [FieldModel params.q] : Type u_1

Equations

• MIPStarRE.LDT.Scalar params = MIPStarRE.LDT.FieldModel.K params.q

@[reducible, inline]

abbrev MIPStarRE.LDT.PolynomialModel (params : Parameters) [FieldModel params.q] : Type u_1

Equations

• MIPStarRE.LDT.PolynomialModel params = MvPolynomial (Fin params.m) (MIPStarRE.LDT.Scalar params)

@[reducible, inline]

abbrev MIPStarRE.LDT.LinePolynomialModel (params : Parameters) [FieldModel params.q] : Type u_1

Equations

• MIPStarRE.LDT.LinePolynomialModel params = Polynomial (MIPStarRE.LDT.Scalar params)

@[simp]

theorem MIPStarRE.LDT.scalar_card (params : Parameters) [FieldModel params.q] : Fintype.card (Scalar params) = params.q

The chosen scalar model for the paper's F_q has exactly q elements (preliminaries.tex, lines 17--19 and 89--93).

def MIPStarRE.LDT.decodeScalar {params : Parameters} [FieldModel params.q] (x : Fq params) : Scalar params

Interpret a coded coordinate in Fin q as a scalar in the chosen field model.

Equations

• MIPStarRE.LDT.decodeScalar x = MIPStarRE.LDT.FieldModel.equiv.symm x

def MIPStarRE.LDT.encodeScalar {params : Parameters} [FieldModel params.q] (x : Scalar params) : Fq params

Re-encode a field-model scalar as its canonical representative in Fin q.

Equations

• MIPStarRE.LDT.encodeScalar x = MIPStarRE.LDT.FieldModel.equiv x

@[simp]

theorem MIPStarRE.LDT.encode_decodeScalar {params : Parameters} [FieldModel params.q] (x : Fq params) : encodeScalar (decodeScalar x) = x

@[simp]

theorem MIPStarRE.LDT.decode_encodeScalar {params : Parameters} [FieldModel params.q] (x : Scalar params) : decodeScalar (encodeScalar x) = x

def MIPStarRE.LDT.zeroCoord {params : Parameters} [FieldModel params.q] : Fq params

The zero coordinate.

Equations

• MIPStarRE.LDT.zeroCoord = MIPStarRE.LDT.encodeScalar 0

def MIPStarRE.LDT.addCoord {params : Parameters} [FieldModel params.q] (x y : Fq params) : Fq params

Coordinate addition transported through the Fin q coding.

Equations

• MIPStarRE.LDT.addCoord x y = MIPStarRE.LDT.encodeScalar (MIPStarRE.LDT.decodeScalar x + MIPStarRE.LDT.decodeScalar y)

def MIPStarRE.LDT.subCoord {params : Parameters} [FieldModel params.q] (x y : Fq params) : Fq params

Coordinate subtraction transported through the Fin q coding.

Equations

• MIPStarRE.LDT.subCoord x y = MIPStarRE.LDT.encodeScalar (MIPStarRE.LDT.decodeScalar x - MIPStarRE.LDT.decodeScalar y)

@[simp]

theorem MIPStarRE.LDT.addCoord_subCoord_right {params : Parameters} [FieldModel params.q] (x y : Fq params) : addCoord y (subCoord x y) = x

@[simp]

theorem MIPStarRE.LDT.addCoord_subCoord_left {params : Parameters} [FieldModel params.q] (x y : Fq params) : addCoord (subCoord x y) y = x

@[simp]

theorem MIPStarRE.LDT.subCoord_addCoord_right {params : Parameters} [FieldModel params.q] (x y : Fq params) : subCoord (addCoord x y) y = x

def MIPStarRE.LDT.mulCoord {params : Parameters} [FieldModel params.q] (x y : Fq params) : Fq params

Coordinate multiplication transported through the Fin q coding.

Equations

• MIPStarRE.LDT.mulCoord x y = MIPStarRE.LDT.encodeScalar (MIPStarRE.LDT.decodeScalar x * MIPStarRE.LDT.decodeScalar y)

def MIPStarRE.LDT.invCoord {params : Parameters} [FieldModel params.q] (x : Fq params) : Fq params

Coordinate inversion transported through the Fin q coding.

Equations

• MIPStarRE.LDT.invCoord x = MIPStarRE.LDT.encodeScalar (MIPStarRE.LDT.decodeScalar x)⁻¹

def MIPStarRE.LDT.addPoint {params : Parameters} [FieldModel params.q] (u v : Point params) : Point params

Pointwise addition in the coded ambient space.

Equations

• MIPStarRE.LDT.addPoint u v i = MIPStarRE.LDT.addCoord (u i) (v i)

def MIPStarRE.LDT.smulPoint {params : Parameters} [FieldModel params.q] (t : Fq params) (u : Point params) : Point params

Scalar multiplication in the coded ambient space.

Equations

• MIPStarRE.LDT.smulPoint t u i = MIPStarRE.LDT.mulCoord t (u i)

def MIPStarRE.LDT.zeroPoint {params : Parameters} [FieldModel params.q] : Point params

The zero point in F_q^m.

Equations

• MIPStarRE.LDT.zeroPoint x✝ = MIPStarRE.LDT.zeroCoord

def MIPStarRE.LDT.embedCoord (params : Parameters) : Fin params.m → Fin params.next.m

The inclusion of the first m coordinates into m + 1 coordinates.

Equations

• MIPStarRE.LDT.embedCoord params i = ⟨↑i, ⋯⟩

theorem MIPStarRE.LDT.embedCoord_injective (params : Parameters) : Function.Injective (embedCoord params)

The old-coordinate inclusion into the appended coordinate space is injective.

def MIPStarRE.LDT.lastCoord (params : Parameters) : Fin params.next.m

The last coordinate of F_q^(m+1).

Equations

• MIPStarRE.LDT.lastCoord params = ⟨params.m, ⋯⟩

theorem MIPStarRE.LDT.embedCoord_ne_lastCoord (params : Parameters) (i : Fin params.m) : embedCoord params i ≠ lastCoord params

No old coordinate is the appended last coordinate.

def MIPStarRE.LDT.appendPoint (params : Parameters) (u : Point params) (x : Fq params) : Point params.next

Append a final coordinate to a point in F_q^m.

Equations

• MIPStarRE.LDT.appendPoint params u x i = if h : ↑i < params.m then u ⟨↑i, h⟩ else x

def MIPStarRE.LDT.truncatePoint (params : Parameters) (u : Point params.next) : Point params

Truncate the last coordinate of a point in F_q^{m+1}.

Equations

• MIPStarRE.LDT.truncatePoint params u i = u ⟨↑i, ⋯⟩

def MIPStarRE.LDT.pointHeight (params : Parameters) (u : Point params.next) : Fq params

Extract the final coordinate of a point in F_q^{m+1}.

Equations

• MIPStarRE.LDT.pointHeight params u = u (MIPStarRE.LDT.lastCoord params)

@[simp]

theorem MIPStarRE.LDT.truncatePoint_appendPoint (params : Parameters) (u : Point params) (x : Fq params) : truncatePoint params (appendPoint params u x) = u

@[simp]

theorem MIPStarRE.LDT.pointHeight_appendPoint (params : Parameters) (u : Point params) (x : Fq params) : pointHeight params (appendPoint params u x) = x

def MIPStarRE.LDT.decodePoint {params : Parameters} [FieldModel params.q] (u : Point params) : Fin params.m → Scalar params

Decode a coded point as a tuple of scalars in the chosen field model.

Equations

• MIPStarRE.LDT.decodePoint u i = MIPStarRE.LDT.decodeScalar (u i)

noncomputable def MIPStarRE.LDT.evalPolynomialModel (params : Parameters) [FieldModel params.q] (p : PolynomialModel params) (u : Point params) : Fq params

Evaluate a multivariate polynomial over the chosen field model on a coded point.

Equations

• MIPStarRE.LDT.evalPolynomialModel params p u = MIPStarRE.LDT.encodeScalar ((MvPolynomial.eval (MIPStarRE.LDT.decodePoint u)) p)

noncomputable def MIPStarRE.LDT.evalLinePolynomialModel (params : Parameters) [FieldModel params.q] (p : LinePolynomialModel params) (t : Fq params) : Fq params

Evaluate a univariate polynomial over the chosen field model on a coded point.

Equations

• MIPStarRE.LDT.evalLinePolynomialModel params p t = MIPStarRE.LDT.encodeScalar (Polynomial.eval (MIPStarRE.LDT.decodeScalar t) p)