Hybrid Guruswami-Sudan Interpolation

Output-sensitive interpolation backend combining the adaptive Lee-O'Sullivan route with the order-driven approximant-basis route through a ski-rental budget policy.

The Mulders-Storjohann reduction of the Lee-O'Sullivan basis terminates after a number of steps that vanishes on codewords and scales with the distance of the received word from the code, while the approximant-basis backend costs the same on every input. The hybrid runs the reduction with a calibrated step budget B as fuel; if the budget is exhausted before the basis is conflict-free, it falls back to the approximant solver, so the total cost is within a constant factor of the cheaper route on every input.

The budget is the entire fuel policy: the reduction loop stops by itself as soon as the basis is conflict-free, so unused fuel is free and any cap below B could only trigger premature fallback. (In particular the excess of the initial shifted-degree sum over the weak-Popov floor is not a usable cap: the step count includes leading-position moves that leave the shifted-degree sum unchanged, so reductions routinely need more steps than that excess.)

The dispatch affects performance only: both branches are complete verified interpolators, and Interpolation/Hybrid/Correctness.lean shows the hybrid result always coincides with one of them.

References

• [Karlin, A. R., Manasse, M. S., Rudolph, L., and Sleator, D. D., Competitive snoopy caching][KMRS88]

def CompPoly.GuruswamiSudan.Hybrid.hybridPositiveInterpolate {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) : Option (CBivariate F)

Positive-Y-weight hybrid interpolation branch: reduce the Lee-O'Sullivan basis with the budgeted fuel and keep the result when it reached shifted weak Popov form (no leading conflict remains), otherwise fall back to the approximant-basis solver.

def CompPoly.GuruswamiSudan.Hybrid.hybridInterpolate {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) : Option (CBivariate F)

Hybrid interpolation with the shared low-message branch.