Section 12 — Definitions: interpolation

Interpolation helpers extracted from Pasting.Defs.

def MIPStarRE.LDT.Pasting.pointTupleTail {params : Parameters} {k : ℕ} (xs : PointTuple params (k + 1)) : PointTuple params k

Remove the first coordinate from a tuple of slice questions.

Equations

• MIPStarRE.LDT.Pasting.pointTupleTail xs i = xs i.succ

def MIPStarRE.LDT.Pasting.gHatTupleOutcomeTail {params : Parameters} {k : ℕ} [FieldModel params.q] (gs : GHatTupleOutcome params (k + 1)) : GHatTupleOutcome params k

Remove the first coordinate from a tuple of completed slice outcomes.

Equations

• MIPStarRE.LDT.Pasting.gHatTupleOutcomeTail gs i = gs i.succ

noncomputable def MIPStarRE.LDT.Pasting.fallbackInterpolatedPolynomial (params : Parameters) [FieldModel params.q] : Polynomial params.next

The distinguished global polynomial h₀ used for the pasted completion outcome.

It is also the default value on tuples that have already been filtered out of the actual interpolation path (for example nonglobal tuples after the IsGloballyConsistent restriction). We take h₀ to be the zero polynomial, which trivially satisfies the low-individual-degree bound.

Equations

• MIPStarRE.LDT.Pasting.fallbackInterpolatedPolynomial params = { poly := 0, lowIndividualDegree := ⋯ }

def MIPStarRE.LDT.Pasting.extractSlicePoly {params : Parameters} {k : ℕ} [FieldModel params.q] (gs : GHatTupleOutcome params k) (i : Fin k) (hi : i ∈ gHatTupleSupport gs) : Polynomial params

Extract the polynomial from a genuine slice outcome.

Equations

• MIPStarRE.LDT.Pasting.extractSlicePoly gs i hi = Option.get (gs i) ⋯

@[instance_reducible]

instance MIPStarRE.LDT.Pasting.interpolationEligible_decidablePred (params : Parameters) [FieldModel params.q] {k : ℕ} : DecidablePred (InterpolationEligible params)

InterpolationEligible params is decidable without invoking classical logic: it is the finite inequality d + 1 ≤ |support(gs)|, where the support is computed by filtering the finite index set.

Equations

• MIPStarRE.LDT.Pasting.interpolationEligible_decidablePred params gs = id (id (id inferInstance))

structure MIPStarRE.LDT.Pasting.InterpolationSupportWitness (params : Parameters) [FieldModel params.q] {k : ℕ} (gs : GHatTupleOutcome params k) : Type

Paper origin: references/ldt-paper/ld-pasting.tex:473-482 (interpolation step of the second construction, requiring |w| \geq d+1 genuine outcomes).

A d+1-element interpolation support together with the proof fields that show it lies inside the genuine completed-slice support. The support is chosen from the finite-set existence theorem Finset.exists_subset_card_eq.

• support : Finset (Fin k)
• subset_support : self.support ⊆ gHatTupleSupport gs
• card_eq : self.support.card = params.d + 1

noncomputable def MIPStarRE.LDT.Pasting.interpolationSupportWitness {params : Parameters} {k : ℕ} [FieldModel params.q] (gs : GHatTupleOutcome params k) (hEligible : InterpolationEligible params gs) : InterpolationSupportWitness params gs

Paper origin: references/ldt-paper/ld-pasting.tex:473-482 (interpolation step of the second construction, requiring |w| \geq d+1 genuine outcomes).

Construct a d+1-point interpolation support inside the genuine support of an interpolation-eligible tuple.

Source: This is the source-faithful finite-support selection required by the interpolation step cited above; the paper assumes such a support after the cardinality lower bound is known.

Equations

• MIPStarRE.LDT.Pasting.interpolationSupportWitness gs hEligible = { support := Classical.choose ⋯, subset_support := ⋯, card_eq := ⋯ }

noncomputable def MIPStarRE.LDT.Pasting.interpolateCompletedSlicesFromSupport (params : Parameters) [FieldModel params.q] {k : ℕ} (xs : PointTuple params k) (gs : GHatTupleOutcome params k) (σ : Finset (Fin k)) (hσsupport : σ ⊆ gHatTupleSupport gs) (hσcard : σ.card = params.d + 1) : Polynomial params.next

Interpolate from a specified d+1-element index set to recover a polynomial in m+1 variables via Lagrange interpolation. The caller must provide hσsupport : σ ⊆ gHatTupleSupport gs, i.e. every interpolation node is a genuine completed-slice outcome. This keeps the support precondition explicit instead of silently falling back to the zero polynomial.

The degree bound (lowIndividualDegree ≤ d) holds for any σ with σ.card = d+1; the interpolation correctness property (that restrictAtHeight of the result agrees with each slice) additionally requires distinct evaluation points, which are ensured by the caller together with hσsupport.

The coefficient is Mathlib's Lagrange.basis σ v i, the polynomial ∏ j ∈ σ.erase i, (X - v j) / (v i - v j), evaluated at the appended coordinate.

Equations

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