Correctness of Hybrid Guruswami-Sudan Interpolation

The hybrid's fuel/fallback dispatch affects performance only: its result always coincides with the result of one of the two verified backends (hybridPositiveInterpolate_eq_lee_or_approximant). Soundness and completeness of hybridInterpContext follow by case analysis from the corresponding backend theorems.

The only reduction-level fact needed is determinism of the fueled Mulders-Storjohann loop (muldersStorjohannReduceWithFuel_eq_of_no_conflict): when the budgeted probe ends without a shifted leading conflict, it stopped at the same matrix as the full reduction, so the kept Lee branch is literally the Lee-O'Sullivan backend run with the fast reducer context.

theorem CompPoly.GuruswamiSudan.Hybrid.hybridPositiveInterpolate_eq_lee_or_approximant {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) (budget : GSInterpParams → ℕ) (points : Array (F × F)) (params : GSInterpParams) : hybridPositiveInterpolate V E solver budget points params = LeeOSullivan.leeOSullivanPositiveInterpolate V E (PolynomialMatrix.muldersStorjohannFastReducerContext F) points params ∨ hybridPositiveInterpolate V E solver budget points params = ApproximantBasis.approximantBasisPositiveInterpolate V E solver points params

The hybrid branch result always coincides with one of the two verified backends.

theorem CompPoly.GuruswamiSudan.Hybrid.hybridInterpolate_eq_lee_or_approximant {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) (budget : GSInterpParams → ℕ) (points : Array (F × F)) (params : GSInterpParams) : hybridInterpolate V E solver budget points params = LeeOSullivan.leeOSullivanInterpolate V E (PolynomialMatrix.muldersStorjohannFastReducerContext F) points params ∨ hybridInterpolate V E solver budget points params = ApproximantBasis.approximantBasisInterpolate V E solver points params

The hybrid result always coincides with one of the two verified backends.

def CompPoly.GuruswamiSudan.Hybrid.hybridInterpContext {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) (budget : GSInterpParams → ℕ) : GSInterpContext F

Public hybrid interpolation backend context: adaptive Lee-O'Sullivan reduction under a step budget with an approximant-basis fallback.