Shared Guruswami-Sudan Interpolation Correctness

Backend-neutral correctness facts for executable interpolation helpers.

theorem CompPoly.GuruswamiSudan.interpolationWitnessIsValidBool_iff {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {points : Array (F × F)} {params : GSInterpParams} {Q : CBivariate F} : interpolationWitnessIsValidBool points params Q = true ↔ ValidInterpolationWitness points params Q

The executable witness recognizer is equivalent to the semantic witness contract.

theorem CompPoly.GuruswamiSudan.lowMessageDegreeInterpolation_sound {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {points : Array (F × F)} {params : GSInterpParams} (hLow : params.messageDegree ≤ 1) : have Q := lowMessageDegreeInterpolation points params.multiplicity; ValidInterpolationWitness points params Q

Constructive low-message interpolation returns a semantic GS interpolation witness.