Approximant-Basis Interpolation Correctness Surface

Theorem statements for the modular-equation reduction and the public GSInterpContext boundary.

Width truncation helpers

The modular-equation layer

theorem CompPoly.GuruswamiSudan.ApproximantBasis.gsModularEquation_row_iff_multiplicity {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (V : CPolynomial.VanishingPolynomialContext F) (E : CPolynomial.BatchEvalContext F) (modCtx : CPolynomial.ModContext F) (mulCtx : CPolynomial.MulContext F) (points : Array (F × F)) (params : GSInterpParams) (row : PolynomialRow F) (hdistinct : DistinctXCoordinates points) (hwidth : Array.size row ≤ interpolationWidth params) : have data := buildGSModularData V E mulCtx modCtx points params; PolynomialMatrix.rowSatisfiesModularBool mulCtx modCtx row data.matrix data.moduli = true ↔ (CBivariate.ofCoeffRow row).satisfiesMultiplicityConstraintsBool points params.multiplicity = true

The executable GS modular row predicate is equivalent to packed multiplicity constraints for the bivariate coefficient-row view, for distinct interpolation nodes and rows inside the interpolation width.

Soundness

theorem CompPoly.GuruswamiSudan.ApproximantBasis.approximantBasisInterpolate_sound {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (V : CPolynomial.VanishingPolynomialContext F) (E : CPolynomial.BatchEvalContext F) (solver : PolynomialMatrix.Approximant.ModularSolutionBasisContext F) {points : Array (F × F)} {params : GSInterpParams} {Q : CBivariate F} (h : approximantBasisInterpolate V E solver points params = some Q) : ValidInterpolationWitness points params Q

Soundness for executable approximant-basis interpolation.

Completeness

theorem CompPoly.GuruswamiSudan.ApproximantBasis.approximantBasisInterpolate_complete {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (V : CPolynomial.VanishingPolynomialContext F) (E : CPolynomial.BatchEvalContext F) (solver : PolynomialMatrix.Approximant.ModularSolutionBasisContext F) (points : Array (F × F)) (params : GSInterpParams) (hdistinct : DistinctXCoordinates points) (hexists : ∃ (Q : CBivariate F), ValidInterpolationWitness points params Q) : ∃ (Q : CBivariate F), approximantBasisInterpolate V E solver points params = some Q

Completeness for executable approximant-basis interpolation on distinct input x-coordinates.

def CompPoly.GuruswamiSudan.ApproximantBasis.approximantBasisInterpContext {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (V : CPolynomial.VanishingPolynomialContext F) (E : CPolynomial.BatchEvalContext F) (solver : PolynomialMatrix.Approximant.ModularSolutionBasisContext F) : GSInterpContext F

Public approximant-basis interpolation backend context.