feat(bivariate): approximant-basis and hybrid interpolation for GS decoder#255
Open
olympichek wants to merge 10 commits into
Open
feat(bivariate): approximant-basis and hybrid interpolation for GS decoder#255olympichek wants to merge 10 commits into
olympichek wants to merge 10 commits into
Conversation
- Drop Koetter backend dependencies (Koetter is not on master yet; it lives on the gs-koetter branch): remove Koetter interpolation/core benchmark rows and the Koetter interp/filtered-core contexts, and switch WitnessDivisibilityCorrectness to the ofYConstant lemmas from the Lee-O'Sullivan Combinations module. - Align Implementations imports with master's reorganized root-search layers (RothRuckenstein/Alekhnovich correctness modules). - Regenerate CompPoly.lean for the post-rebase file set. - Mathlib bump fixes: finset_sum_coeff/eval_finset_sum renames, and in me_verification_dominates replace the rw-then-exact step for hquotExact with a single rw chain — under the new mathlib the exact's unifier fell into whnf-unfolding CPolynomial.toPoly's executable fold through Polynomial.instMul (32 s for one step); the rewrite matches syntactically and the proof is back under default maxHeartbeats.
- Remove references to untracked analysis notes (gs-interpolation-complexity-analysis.md) from the hybrid backend docstrings; the ski-rental rationale is stated inline instead. - Update benchmark docstrings that still described the long-code group as comparing exactly two backends (it also runs the hybrid row). - Replace temporal/refactoring wording with declarative phrasing (unchunked debug helper, iteration-count convention note) and an absolute-units timing claim in the validity-checksum docstring.
Mirror the References convention of the other backends (LOS06, MS03, GS99, Ale05, RR00): - Approximant/Basic.lean and PMBasis/Recursion.lean cite Beckermann- Labahn [BL94] (minimal approximant bases) and Giorgi-Jeannerod- Villard [GJV03] (the PM-Basis divide-and-conquer). - PartialLinearization.lean cites Storjohann [Sto06] (partial linearization of unbalanced orders). - ModularEquation/Basic.lean cites [GJV03], [Sto06], and Chowdhury- Jeannerod-Neiger-Schost-Villard [CJNSV15] for the diagonal modular-system-to-order-basis reduction. - The GS ApproximantBasis backend (Basic, Algorithm) cites [CJNSV15] (interpolation with multiplicities as simultaneous approximations). - Hybrid/Algorithm.lean cites Karlin-Manasse-Rudolph-Sleator [KMRS88] for the ski-rental budget policy.
🤖 PR SummaryMathematical Formalization
Algorithmic Implementations
Infrastructure & Benchmarking
Proof Completion
Statistics
Lean Declarations ✏️ **Removed:** 3 declaration(s)
✏️ **Added:** 802 declaration(s)
✏️ **Affected:** 5 declaration(s) (line number changed)
📋 **Additional Analysis**Style and Naming Guidelines Adherence
Project-Specific Review
Suggestions and Checks
No style violations found. 📄 **Per-File Summaries**
Last updated: 2026-06-12 13:15 UTC. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Overview
This PR adds two new backends for the Guruswami-Sudan interpolation subproblem: an approximant-basis backend and a hybrid backend combining it with Lee-O'Sullivan.
The approximant-basis backend solves the interpolation problem through a minimal approximant basis (PM-Basis). Its cost is quasi-linear in the code length and does not depend on how corrupted the received word is, which makes it the fastest backend on long codes with many errors — the regime where the reduction work dominates Lee-O'Sullivan.
The hybrid backend gets the best of both: it runs Lee-O'Sullivan under a step budget and falls back to the approximant solver when the budget runs out, so it is as fast as Lee-O'Sullivan on clean and lightly corrupted words while staying close to the approximant backend on heavily corrupted ones.
This PR includes:
GSInterpContextinstance, with soundness and completeness proofs.GSInterpContextinstance; its result provably always coincides with one of the two underlying verified backends, so correctness carries over directly.