Guruswami-Sudan Core Correctness #
Public correctness theorems for the backend-parametric CompPoly Guruswami-Sudan core.
theorem
CompPoly.GuruswamiSudan.gsCore_sound
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
[DecidableEq F]
{points : Array (F × F)}
{interpContext : GSInterpContext F}
{rootContext : GSRootContext F}
{params : GSInterpParams}
{p : CPolynomial F}
(hp : p ∈ (gsCore points interpContext rootContext params).toList)
:
∃ (Q : CBivariate F),
interpContext.interpolate points params = some Q ∧ ValidInterpolationWitness points params Q ∧ degreeLt p params.messageDegree ∧ Q.composeY p = 0
Every polynomial returned by gsCore is a bounded-degree root of the
interpolation polynomial produced by the interpolation backend.
theorem
CompPoly.GuruswamiSudan.gsCore_complete_of_interpolate
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
[DecidableEq F]
{points : Array (F × F)}
{interpContext : GSInterpContext F}
{rootContext : GSRootContext F}
{params : GSInterpParams}
{Q : CBivariate F}
{p : CPolynomial F}
(hQ : interpContext.interpolate points params = some Q)
(hpdeg : degreeLt p params.messageDegree)
(hroot : Q.composeY p = 0)
:
Completeness for the concrete interpolation polynomial returned by the interpolation backend.
theorem
CompPoly.GuruswamiSudan.gsCore_complete_of_roots_all_valid_witnesses
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
[DecidableEq F]
{points : Array (F × F)}
{interpContext : GSInterpContext F}
{rootContext : GSRootContext F}
{params : GSInterpParams}
{p : CPolynomial F}
(hInterpExists : ∃ (Q : CBivariate F), ValidInterpolationWitness points params Q)
(hdistinct : DistinctXCoordinates points)
(hpdeg : degreeLt p params.messageDegree)
(hrootAll : ∀ (Q : CBivariate F), ValidInterpolationWitness points params Q → Q.composeY p = 0)
:
Backend-parametric completeness for candidates that root every valid interpolation witness.
theorem
CompPoly.GuruswamiSudan.composeY_eq_zero_of_enough_matching_multiplicity_points
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
[DecidableEq F]
{points : Array (F × F)}
{params : GSInterpParams}
{Q : CBivariate F}
{p : CPolynomial F}
(hQ : ValidInterpolationWitness points params Q)
(hpdeg : degreeLt p params.messageDegree)
(hdistinct : DistinctXCoordinates points)
(hmatches : params.weightedDegreeBound < params.multiplicity * matchingPointCount points p)
:
If a bounded-degree candidate agrees with enough distinct packed multiplicity-constrained points, it roots any valid interpolation witness.
theorem
CompPoly.GuruswamiSudan.gsCore_complete_of_enough_matches
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
[DecidableEq F]
{points : Array (F × F)}
{interpContext : GSInterpContext F}
{rootContext : GSRootContext F}
{params : GSInterpParams}
{p : CPolynomial F}
(hInterpExists : ∃ (Q : CBivariate F), ValidInterpolationWitness points params Q)
(hpdeg : degreeLt p params.messageDegree)
(hdistinct : DistinctXCoordinates points)
(hmatches : params.weightedDegreeBound < params.multiplicity * matchingPointCount points p)
:
Packed-point semantic completeness for the algebraic GS core.