Dense Guruswami-Sudan Interpolation Correctness

Correctness contracts for the dense interpolation path and its constructive low-message branch.

theorem CompPoly.GuruswamiSudan.normalizeVector?_some_data {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {v w : Array F} (h : normalizeVector? v = some w) : ∃ pivot < v.size, v.getD pivot 0 ≠ 0 ∧ w = Array.map (fun (x : F) => x / v.getD pivot 0) v ∧ w.size = v.size ∧ w.getD pivot 0 = 1

theorem CompPoly.GuruswamiSudan.interpolationPolynomialOnBasis_weightedDegree_le {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (basis : Array CBivariate.Monomial) (params : GSInterpParams) (coeffs : Array F) (hbound : ∀ monomial ∈ basis.toList, 1 * monomial.xDegree + yWeight params * monomial.yDegree ≤ params.weightedDegreeBound) : (interpolationPolynomialOnBasis basis coeffs).natWeightedDegree 1 (yWeight params) ≤ params.weightedDegreeBound

theorem CompPoly.GuruswamiSudan.interpolationPolynomial_weightedDegree_le {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (params : GSInterpParams) (coeffs : Array F) : (interpolationPolynomial params coeffs).natWeightedDegree 1 (yWeight params) ≤ params.weightedDegreeBound

theorem CompPoly.GuruswamiSudan.isHomogeneousSolution_map_div {F : Type u_1} [Field F] {M : DenseMatrix F} {v : Array F} (a : F) (hsol : M.IsHomogeneousSolution v) : M.IsHomogeneousSolution (Array.map (fun (x : F) => x / a) v)

theorem CompPoly.GuruswamiSudan.interpolationPolynomialOnBasis_satisfies_of_solution {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {basis : Array CBivariate.Monomial} {points : Array (F × F)} {params : GSInterpParams} {coeffs : Array F} (hsol : (interpolationMatrixOnBasis basis points params).IsHomogeneousSolution coeffs) : (interpolationPolynomialOnBasis basis coeffs).SatisfiesMultiplicityConstraints points params.multiplicity

theorem CompPoly.GuruswamiSudan.interpolationPolynomial_satisfies_of_solution {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {points : Array (F × F)} {params : GSInterpParams} {coeffs : Array F} (hsol : (interpolationMatrix points params).IsHomogeneousSolution coeffs) : (interpolationPolynomial params coeffs).SatisfiesMultiplicityConstraints points params.multiplicity

theorem CompPoly.GuruswamiSudan.interpolationCoefficientVectorOnBasis_getD_of_lt {F : Type u_1} [Zero F] (basis : Array CBivariate.Monomial) (Q : CBivariate F) {k : ℕ} (hk : k < basis.size) : (interpolationCoefficientVectorOnBasis basis Q).getD k 0 = Q.coeff (basis.getD k { xDegree := 0, yDegree := 0 }).xDegree (basis.getD k { xDegree := 0, yDegree := 0 }).yDegree

theorem CompPoly.GuruswamiSudan.interpolationCoefficientVectorOnBasis_size {F : Type u_1} [Zero F] (basis : Array CBivariate.Monomial) (Q : CBivariate F) : (interpolationCoefficientVectorOnBasis basis Q).size = basis.size

theorem CompPoly.GuruswamiSudan.cbivariate_ne_zero_exists_coeff_ne_zero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {Q : CBivariate F} (hQ : Q ≠ 0) : ∃ (i : ℕ) (j : ℕ), Q.coeff i j ≠ 0

theorem CompPoly.GuruswamiSudan.interpolationCoefficientVectorOnBasis_nonzero_of_complete {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {basis : Array CBivariate.Monomial} {Q : CBivariate F} (hQ : Q ≠ 0) (hcomplete : ∀ (i j : ℕ), Q.coeff i j ≠ 0 → { xDegree := i, yDegree := j } ∈ basis.toList) : DenseMatrix.NonzeroVector (interpolationCoefficientVectorOnBasis basis Q)

theorem CompPoly.GuruswamiSudan.interpolationPolynomialOnBasis_eq_of_complete {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {basis : Array CBivariate.Monomial} {Q : CBivariate F} (hnodup : basis.toList.Nodup) (hcomplete : ∀ (i j : ℕ), Q.coeff i j ≠ 0 → { xDegree := i, yDegree := j } ∈ basis.toList) : interpolationPolynomialOnBasis basis (interpolationCoefficientVectorOnBasis basis Q) = Q

theorem CompPoly.GuruswamiSudan.interpolationCoefficientVectorOnBasis_solution_of_satisfies {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {basis : Array CBivariate.Monomial} {points : Array (F × F)} {params : GSInterpParams} {Q : CBivariate F} (hpoly : interpolationPolynomialOnBasis basis (interpolationCoefficientVectorOnBasis basis Q) = Q) (hconstraints : Q.SatisfiesMultiplicityConstraints points params.multiplicity) : (interpolationMatrixOnBasis basis points params).IsHomogeneousSolution (interpolationCoefficientVectorOnBasis basis Q)

theorem CompPoly.GuruswamiSudan.normalizeVector?_some_of_nonzero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {v : Array F} (hnz : DenseMatrix.NonzeroVector v) : ∃ (norm : Array F), normalizeVector? v = some norm

theorem CompPoly.GuruswamiSudan.weightedDegreeBasis_sound (params : GSInterpParams) (monomial : CBivariate.Monomial) : monomial ∈ (interpolationMonomials params).toList → 1 * monomial.xDegree + yWeight params * monomial.yDegree ≤ params.weightedDegreeBound

Soundness of the weighted-degree basis used by the public GS interpolation path.

theorem CompPoly.GuruswamiSudan.denseInterpolateWithBasis_sound {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {kernelContext : LinearKernelContext F} {basis : Array CBivariate.Monomial} {points : Array (F × F)} {params : GSInterpParams} {Q : CBivariate F} (hbasis : basis.toList.Nodup) (h : denseInterpolateWithBasisAndKernel kernelContext basis points params = some Q) : Q ≠ 0 ∧ (∃ (coeffs : Array F), Q = interpolationPolynomialOnBasis basis coeffs) ∧ Q.SatisfiesMultiplicityConstraints points params.multiplicity

Soundness for one returned basis-parametric dense witness.

theorem CompPoly.GuruswamiSudan.denseInterpolateWithBasis_complete {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {kernelContext : LinearKernelContext F} {basis : Array CBivariate.Monomial} {points : Array (F × F)} {params : GSInterpParams} (hExists : ∃ (coeffs : Array F), (interpolationMatrixOnBasis basis points params).VectorWidth coeffs ∧ (interpolationMatrixOnBasis basis points params).IsHomogeneousSolution coeffs ∧ DenseMatrix.NonzeroVector coeffs) : ∃ (Q : CBivariate F), denseInterpolateWithBasisAndKernel kernelContext basis points params = some Q

Basis-parametric dense completeness for finite homogeneous systems.

theorem CompPoly.GuruswamiSudan.denseInterpolateWithBasisAndKernel_sound_of_bounded_basis {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {kernelContext : LinearKernelContext F} {basis : Array CBivariate.Monomial} {points : Array (F × F)} {params : GSInterpParams} {Q : CBivariate F} (hbasis : basis.toList.Nodup) (hbound : ∀ monomial ∈ basis.toList, 1 * monomial.xDegree + yWeight params * monomial.yDegree ≤ params.weightedDegreeBound) (h : denseInterpolateWithBasisAndKernel kernelContext basis points params = some Q) : ValidInterpolationWitness points params Q

Basis-parametric dense soundness specialized to a bounded basis.

theorem CompPoly.GuruswamiSudan.denseInterpolateWithWeightedDegreeBasis_sound {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {kernelContext : LinearKernelContext F} {points : Array (F × F)} {params : GSInterpParams} {Q : CBivariate F} (h : denseInterpolateWithBasisAndKernel kernelContext (interpolationMonomials params) points params = some Q) : ValidInterpolationWitness points params Q

Dense weighted-degree-basis soundness for the positive-message branch.

theorem CompPoly.GuruswamiSudan.denseInterpolate_sound {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {kernelContext : LinearKernelContext F} {points : Array (F × F)} {params : GSInterpParams} {Q : CBivariate F} (h : denseInterpolateWithKernel kernelContext points params = some Q) : ValidInterpolationWitness points params Q

Soundness for one returned public interpolation witness.

theorem CompPoly.GuruswamiSudan.denseInterpolateWithBasis_exists_of_dimension_slack {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (basis : Array CBivariate.Monomial) (points : Array (F × F)) (params : GSInterpParams) (hSlack : HasInterpolationDimensionSlackOnBasis basis points params) : ∃ (Q : CBivariate F), denseInterpolateWithBasisAndKernel (denseLinearKernelContext F) basis points params = some Q

If a basis-parametric dense interpolation matrix has more columns than rows, the dense solver finds a nonzero homogeneous witness.

theorem CompPoly.GuruswamiSudan.denseInterpolate_exists_of_dimension_slack {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (points : Array (F × F)) (params : GSInterpParams) (hSlack : HasInterpolationDimensionSlack points params) : ∃ (Q : CBivariate F), denseInterpolate points params = some Q

Dimension slack for the public interpolation basis gives an interpolation witness. The low-message branch is constructive; otherwise the witness comes from the dense matrix.

theorem CompPoly.GuruswamiSudan.weightedDegreeBasis_complete_of_messageDegree_gt_one {F : Type u_1} [Zero F] [BEq F] [LawfulBEq F] {params : GSInterpParams} (hHigh : ¬params.messageDegree ≤ 1) {Q : CBivariate F} (hdeg : Q.natWeightedDegree 1 (yWeight params) ≤ params.weightedDegreeBound) (i j : ℕ) : Q.coeff i j ≠ 0 → { xDegree := i, yDegree := j } ∈ (interpolationMonomials params).toList

When messageDegree > 1, the weighted-degree basis is complete for the semantic weighted-degree predicate.

theorem CompPoly.GuruswamiSudan.denseInterpolate_complete_of_messageDegree_gt_one {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {points : Array (F × F)} {params : GSInterpParams} (hHigh : ¬params.messageDegree ≤ 1) : (∃ (Q : CBivariate F), ValidInterpolationWitness points params Q) → ∃ (Q : CBivariate F), denseInterpolate points params = some Q

Dense interpolation completeness in the ordinary positive-Y-weight range.

def CompPoly.GuruswamiSudan.denseInterpContext (F : Type u_1) [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] : GSInterpContext F

The executable interpolation path packaged as a certified GS interpolation backend.

theorem CompPoly.GuruswamiSudan.denseInterpContext_correct (F : Type u_1) [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (points : Array (F × F)) (params : GSInterpParams) (Q : CBivariate F) : (denseInterpContext F).interpolate points params = some Q → ValidInterpolationWitness points params Q

Executable interpolation backend soundness.

theorem CompPoly.GuruswamiSudan.denseInterpContext_complete (F : Type u_1) [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (points : Array (F × F)) (params : GSInterpParams) : DistinctXCoordinates points → (∃ (Q : CBivariate F), ValidInterpolationWitness points params Q) → ∃ (Q : CBivariate F), (denseInterpContext F).interpolate points params = some Q

Executable interpolation backend completeness.