feat(bivariate): approximant-basis and hybrid GS interpolation by dhsorens · Pull Request #291 · Verified-zkEVM/CompPoly

dhsorens · 2026-08-07T14:49:58Z

Summary

Stacked re-land of olympichek’s (Valerii Huhnin) #255 work on top of #290 (Shoup / Las Vegas roots).

Adds two Guruswami-Sudan interpolation backends plus matrix infrastructure:

Approximant-basis — modular key equations via PM-Basis (quasi-linear in code length; independent of corruption level).
Hybrid — budgeted Lee–O'Sullivan with approximant fallback; correctness by equality to one of the two verified backends.
WitnessDivisibility — fast multiplicity check ≡ Hasse pointwise check.
Supporting PolynomialMatrix.Approximant layer (and related Operations / Strassen / WeakPopov helpers).

Stack

main
 └── #290 re-land/roots-shoup-lasvegas   (Shoup + Las Vegas)
      └── this PR re-land/gs-approximant

Merge #290 first, then this PR (or restack onto main after #290 merges).

Attribution

Original author: Valerii Huhnin (olympichek) — commit author + file Authors: headers.
Maintainer port (module system, merge conflicts, API drift, lint path shorten): Derek Sorensen.

Supersedes

feat(bivariate): approximant-basis and hybrid interpolation for GS decoder #255 — re-landed here (auto-close on merge).

Closes #255

Idiom notes

Module system throughout; facades via update-lib.sh.
Plugs into existing GSInterpContext / Implementations pattern.
Wiki + ROADMAP updated for four interpolation backends.
Some overlappingInstances linter warnings remain on ported [Field F] [Zero F] pairs — follow-up cleanup without changing contracts.

Test plan

lake build (approximant stack + Implementations)
Approximant tests build
import / lint / docs integrity
CI green on this PR
CI green after feat(univariate): Shoup and Las Vegas root-search backends #290 merge / restack if needed

github-actions · 2026-08-07T15:01:50Z

Build Timing Report

Commit: 4965450
Message: Merge d07299b into 527a505
Ref: re-land/gs-approximant
Comparison baseline: b451fac from the previous successful PR update.
Measured on ubuntu-latest with /usr/bin/time -p.
Commands: library build (warm) lake build.
Clean build was skipped (warm/incremental CI; no toolchain or lake-manifest change). Runs automatically when lean-toolchain or lake-manifest.json changes, or via Actions → Lean Action CI → Run workflow with clean_build.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	392.93	-	-	-
Library build (warm)	1.54	63.41	+61.87	exit 1
Test path	45.73	-	-	-

Incremental Rebuild Signal

Warm-only run: default CI reuses cached oleans and rebuilds dirty modules only. No same-job clean:warm ratio.

Slowest Current Build Files (warm library build)

Showing 20 slowest current targets from the warm library build log, with comparison against the baseline clean build log when available.

Current (s)	Baseline (s)	Delta (s)	Path
18.00	24.00	-6.00	`CompPoly/Bivariate/Deriv.lean`
11.00	11.00	+0.00	`CompPoly/Bivariate/GuruswamiSudan/Root/Alekhnovich/Correctness.lean`
8.10	5.70	+2.40	`CompPoly/Bivariate/GuruswamiSudan/Interpolation/LeeOSullivan/Correctness/Basis.lean`
6.90	6.20	+0.70	`CompPoly/Bivariate/GuruswamiSudan/Interpolation/LeeOSullivan/Correctness/Combinations.lean`
6.60	27.00	-20.40	`CompPoly/Bivariate/GuruswamiSudan/Root/RothRuckenstein/Correctness.lean`
5.30	5.80	-0.50	`CompPoly/Bivariate/GuruswamiSudan/Interpolation/Dense/Correctness.lean`
4.80	5.60	-0.80	`CompPoly/Bivariate/GuruswamiSudan/PolynomialCorrectness.lean`
4.80	5.40	-0.60	`CompPoly/Bivariate/GuruswamiSudan/Root/RothRuckenstein/Lemmas.lean`
4.70	3.90	+0.80	`CompPoly/LinearAlgebra/PolynomialMatrix/MuldersStorjohannCorrectness/Reduction.lean`
4.70	4.70	+0.00	`CompPoly/Bivariate/GuruswamiSudan/CoreCorrectness.lean`
4.60	4.00	+0.60	`CompPoly/Bivariate/GuruswamiSudan/Root/Common/Lemmas.lean`
4.30	4.40	-0.10	`CompPoly/LinearAlgebra/PolynomialMatrix/MuldersStorjohannCorrectness/WeakPopovMinimal.lean`
4.30	6.10	-1.80	`CompPoly/Bivariate/GuruswamiSudan/Root/FieldRoots/KoalaBear.lean`
4.30	4.50	-0.20	`CompPoly/Bivariate/GuruswamiSudan/Interpolation/LeeOSullivan/Correctness/Selection.lean`
4.00	3.40	+0.60	`CompPoly/Univariate/Roots/Shoup/Basic.lean`
3.90	5.20	-1.30	`CompPoly/LinearAlgebra/PolynomialMatrix/MuldersStorjohannCorrectness/Minimal.lean`
3.50	2.40	+1.10	`CompPoly/Bivariate/GuruswamiSudan/Executable.lean`
3.40	2.00	+1.40	`CompPoly/Bivariate/GuruswamiSudan/Root/Alekhnovich/Algorithm.lean`
3.40	2.90	+0.50	`CompPoly/Bivariate/GuruswamiSudan/Interpolation/LeeOSullivan/Correctness/Normalization.lean`
3.20	2.60	+0.60	`CompPoly/Univariate/Roots/LasVegas/Basic.lean`

github-actions · 2026-08-07T15:02:38Z

🤖 PR Summary

This pull request adds a new approximant-basis backend for Guruswami-Sudan interpolation and a hybrid algorithm that uses it, along with extensive supporting formalization for polynomial matrix operations.

Statistics

Metric	Count
📝 Files Changed	46
✅ Lines Added	14551
❌ Lines Removed	28

Lean Declarations

✏️ Removed: 3 declaration(s)

CompPoly/Bivariate/GuruswamiSudan/Interpolation/LeeOSullivan/Basic.lean (3)

def distinctXCoordinatesBool {F : Type*} [BEq F] (points : Array (F × F)) : Bool
def distinctXCoordinatesListBool {F : Type*} [BEq F] : List (F × F) → Bool
def interpolationYCap (params : GSInterpParams) : Nat

✏️ Added: 748 declaration(s)

CompPoly/Bivariate/Deriv.lean (3)

theorem shiftC_add [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R]
theorem shiftC_mul [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R]
theorem toPoly_injective [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R]

CompPoly/Bivariate/GuruswamiSudan/Implementations.lean (21)

def approximantPMBasisComposeLeafCutoff : Nat
def approximantPMBasisLeafCutoff : Nat
def fastKoalaBearAlekhnovichNttFastRootContext : GSRootContext KoalaBear.Fast.Field
def fastKoalaBearAlekhnovichRootContext : GSRootContext KoalaBear.Fast.Field
def fastKoalaBearApproximantBasisDirectInterpContext :
def fastKoalaBearApproximantBasisInterpContext :
def fastKoalaBearApproximantBasisSubproductInterpContext :
def fastKoalaBearApproximantPMBasisContext :
def fastKoalaBearApproximantSolutionContext :
def fastKoalaBearHybridInterpContext : GSInterpContext KoalaBear.Fast.Field
def fastKoalaBearNttFastLowMulContext :
def hybridReductionStepBudget (params : GSInterpParams) : Nat
def koalaBearAlekhnovichNttFastRootContext : GSRootContext KoalaBear.Field
def koalaBearAlekhnovichRootContext : GSRootContext KoalaBear.Field
def koalaBearApproximantBasisDirectInterpContext : GSInterpContext KoalaBear.Field
def koalaBearApproximantBasisInterpContext : GSInterpContext KoalaBear.Field
def koalaBearApproximantBasisSubproductInterpContext : GSInterpContext KoalaBear.Field
def koalaBearApproximantPMBasisContext :
def koalaBearApproximantSolutionContext :
def koalaBearHybridInterpContext : GSInterpContext KoalaBear.Field
def koalaBearNttFastLowMulContext :

CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis/Algorithm.lean (3)

def approximantBasisInterpolate
def approximantBasisPositiveInterpolate
def normalizeApproximantCandidate? (params : GSInterpParams) (Q : CBivariate F) :

CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis/Basic.lean (8)

def buildGSModularDataWithRG
def buildGSModularData
def gsModuli (mulCtx : CPolynomial.MulContext F) (G : CPolynomial F) (s : Nat) :
def gsRelationColumn (mulCtx : CPolynomial.MulContext F)
def gsRelationEntry (modCtx : CPolynomial.ModContext F)
def gsRelationMatrixWithModuli (mulCtx : CPolynomial.MulContext F)
def gsRelationMatrixWithRG (mulCtx : CPolynomial.MulContext F)
def modularEquation (data : GSModularData F) : ModularEquation F

CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis/Correctness.lean (16)

def approximantBasisInterpContext
private theorem coeff_eq_zero_of_interpolationWidth_le
private theorem coeff_toCoeffRow_ofCoeffRow (row : PolynomialRow F)
private theorem interpolationCoefficientVector_toCoeffRow (params : GSInterpParams)
private theorem interpolationMonomials_yDegree_lt (params : GSInterpParams)
private theorem normalizeInterpolationPolynomial?_eq_none_of_rowIsZero
private theorem normalizeVector?_eq_none_of_all_zero {v : Array F}
private theorem ofCoeffRow_eq_zero_of_rowIsZero {row : PolynomialRow F}
private theorem ofCoeffRow_toCoeffRow_eq
private theorem rowGet_toCoeffRow_ofCoeffRow (row : PolynomialRow F)
private theorem rowShiftedDegree?_congr_shift {row : PolynomialRow F}
private theorem rowShiftedDegree?_toCoeffRow_le {row : PolynomialRow F}
private theorem weightedDegreeShift_getD {w width j : Nat} (hj : j < width) :
theorem approximantBasisInterpolate_complete
theorem approximantBasisInterpolate_sound
theorem gsModularEquation_row_iff_multiplicity

CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis/ModularData.lean (33)

private def relationColumnStep (mulCtx : CPolynomial.MulContext F)
private theorem dvd_iff_dvd_of_dvd_sub {M a b : Polynomial F} (h : M ∣ a - b) :
private theorem foldl_add_eq_sum {M : Type*} [AddCommMonoid M] (f : Nat → M) :
private theorem foldl_mprod_fst {α β : Type u} {γ : Type*}
private theorem gsModuli_loop (mulCtx : CPolynomial.MulContext F) (G : CPolynomial F) :
private theorem gsRelationColumn_eq_foldl (mulCtx : CPolynomial.MulContext F)
private theorem relationColumn_foldl_size_untouched (mulCtx : CPolynomial.MulContext F)
private theorem relationColumn_foldl_spec (mulCtx : CPolynomial.MulContext F)
private theorem rowGet_rowMulMatrixWith_eq_sum (mulCtx : CPolynomial.MulContext F)
private theorem rowMulMatrix_foldl_eq_sum_size (mulCtx : CPolynomial.MulContext F)
private theorem rowSatisfiesModularBool_iff_forall (mulCtx : CPolynomial.MulContext F)
private theorem toPoly_finset_sum (f : Nat → CPolynomial F) (n : Nat) :
private theorem toPoly_ofCoeffRow_eq_sum (row : PolynomialRow F) :
theorem dvd_modByMonicWith_sub (modCtx : CPolynomial.ModContext F)
theorem gsModuli_eq (mulCtx : CPolynomial.MulContext F) (G : CPolynomial F) (s : Nat) :
theorem gsModuli_getD (mulCtx : CPolynomial.MulContext F) (G : CPolynomial F)
theorem gsModuli_getD_one (mulCtx : CPolynomial.MulContext F) (G : CPolynomial F)
theorem gsModuli_size (mulCtx : CPolynomial.MulContext F) (G : CPolynomial F) (s : Nat) :
theorem gsRelationColumn_getD_congr (mulCtx : CPolynomial.MulContext F)
theorem gsRelationColumn_getD_of_lt (mulCtx : CPolynomial.MulContext F)
theorem gsRelationColumn_size (mulCtx : CPolynomial.MulContext F)
theorem gsRelationMatrixWithModuli_entry (mulCtx : CPolynomial.MulContext F)
theorem gsRelationMatrixWithModuli_matrixWidth (mulCtx : CPolynomial.MulContext F)
theorem gsRelationMatrixWithModuli_size (mulCtx : CPolynomial.MulContext F)
theorem hasseDeriv_toPoly_ofCoeffRow_eval (row : PolynomialRow F)
theorem modByMonicWith_eq_zero_iff_dvd (modCtx : CPolynomial.ModContext F)
theorem modByMonicWith_toPoly (modCtx : CPolynomial.ModContext F)
theorem ofFn_matrixWidth (rows width : Nat) (entry : Nat → Nat → CPolynomial F)
theorem ofFn_rowGet (rows width : Nat) (entry : Nat → Nat → CPolynomial F)
theorem ofFn_size (rows width : Nat) (entry : Nat → Nat → CPolynomial F) :
theorem rowMulMatrixWith_congr_of_agree (mulCtx : CPolynomial.MulContext F)
theorem rowSatisfiesModularBool_congr_of_agree (mulCtx : CPolynomial.MulContext F)
theorem rowSatisfiesModularBool_gsRelationMatrix_iff

CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis/Multiplicity.lean (9)

private theorem vanishingPolynomialArray_toPoly_list
theorem X_sub_C_pow_dvd_hasseDeriv_eval_iff_hasMultiplicity
theorem X_sub_C_pow_dvd_hasseDeriv_eval_of_dvd_sub
theorem X_sub_C_pow_dvd_iff_hasseDeriv_eval_eq_zero
theorem linearFactor_toPoly_eq (x : F) :
theorem prod_X_sub_C_pow_dvd_of_nodup
theorem vanishingPolynomialArray_toPoly (xs : Array F) :
theorem vanishingPolynomialArray_toPoly_monic (xs : Array F) :
theorem vanishing_pow_dvd_hasseDeriv_eval_iff_satisfiesMultiplicityConstraints

CompPoly/Bivariate/GuruswamiSudan/Interpolation/Basic.lean (5)

def distinctXCoordinatesBool {F : Type*} [BEq F] (points : Array (F × F)) : Bool
def distinctXCoordinatesListBool {F : Type*} [BEq F] : List (F × F) → Bool
def interpolationShifts (params : GSInterpParams) : Array Nat
def interpolationWidth (params : GSInterpParams) : Nat
def interpolationYCap (params : GSInterpParams) : Nat

CompPoly/Bivariate/GuruswamiSudan/Interpolation/Hybrid/Algorithm.lean (2)

def hybridInterpolate
def hybridPositiveInterpolate

CompPoly/Bivariate/GuruswamiSudan/Interpolation/Hybrid/Correctness.lean (4)

def hybridInterpContext
private theorem hybrid_probe_eq_reduceFast
theorem hybridInterpolate_eq_lee_or_approximant
theorem hybridPositiveInterpolate_eq_lee_or_approximant

CompPoly/Bivariate/GuruswamiSudan/Interpolation/WitnessDivisibility.lean (4)

def divByLinearYWith {R : Type*} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R]
def interpolationWitnessIsValidViaDivisibilityBool {F : Type*}
def satisfiesMultiplicityConstraintsViaDivisibilityBool {F : Type*}
theorem divByLinearYWith_eq_divByLinearY {R : Type*}

CompPoly/Bivariate/GuruswamiSudan/Interpolation/WitnessDivisibilityCorrectness.lean (27)

private theorem witness_coeff_linearYDivisor (u : CPolynomial F) (j : Nat) :
private theorem witness_coeff_low_vanish
private theorem witness_coeff_sub (p q : CPolynomial F) (i : Nat) :
private theorem witness_cpoly_eq_of_toPoly_eq {R : Type*}
private theorem witness_divByLinearY_decomposition (Q : CBivariate F)
private theorem witness_foldl_linearFactor_monic (l : List F) (acc : CPolynomial F)
private theorem witness_hasMultiplicityAtLeast_C_of_dvd
private theorem witness_hasMultiplicityAtLeast_add
private theorem witness_hasMultiplicityAtLeast_sub
private theorem witness_hasMultiplicityAtLeast_zero (P : CBivariate F) (x y : F) :
private theorem witness_hasMultiplicity_quot
private theorem witness_linearFactor_toPoly (x : F) :
private theorem witness_modByMonic_eq_zero_iff {c g : CPolynomial F}
private theorem witness_monic_pow {g : CPolynomial F} (hg : g.monic) (k : Nat) :
private theorem witness_ofYConstant_pow (G : CPolynomial F) (k : Nat) :
private theorem witness_outerCoeff_linearYDivisor_mul (u : CPolynomial F)
private theorem witness_outerCoeff_shiftC_C (x y : F) (c : CPolynomial F)
private theorem witness_shiftC_linearYDivisor (x y : F) (R : CPolynomial F) :
private theorem witness_shiftX_linearYDivisor (x : F) (u : CPolynomial F) :
private theorem witness_shiftY_linearYDivisor (y : F) (R : CPolynomial F) :
private theorem witness_taylor_neg (x : F) (u : CPolynomial F) :
private theorem witness_taylor_one (x : F) :
private theorem witness_taylor_sub_C (x y : F) (R : CPolynomial F) :
private theorem witness_vanishing_monic (xs : Array F) :
private theorem witness_viaDivisibility_iff
theorem interpolationWitnessIsValidViaDivisibilityBool_eq
theorem satisfiesMultiplicityConstraintsViaDivisibilityBool_eq

CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/Basic.lean (7)

def lowerOrders [Zero F] (problem : XAdicProblem F) (d : Nat) : Array Nat
def maxOrder [Zero F] (problem : XAdicProblem F) : Nat
def residualMatrix [Semiring F] [BEq F] [LawfulBEq F]
def residualMatrixWithProduct [Semiring F] [BEq F] [LawfulBEq F]
def residualOrders [Zero F] (problem : XAdicProblem F) (d : Nat) : Array Nat
def totalOrder [Zero F] (problem : XAdicProblem F) : Nat
def updateShiftByRows [Zero F] [BEq F]

CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/Correctness.lean (2)

theorem modularSolutionBasis_complete_minimal
theorem modularSolutionBasis_sound

CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/ModularEquation.lean (1)

def modularSolutionBasisContextViaPMBasis

CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/ModularEquation/Basic.lean (53)

def ModularEquation.modularWidth (equation : ModularEquation F) : Nat
def ModularEquation.solutionWidth (equation : ModularEquation F) : Nat
def PivotDegreeProfile.coversAll (profile : PivotDegreeProfile) : Bool
def PivotDegreeProfile.discoveredAny (profile : PivotDegreeProfile) : Bool
def PivotDegreeProfile.insert (profile : PivotDegreeProfile)

…and 598 more not listed.

✏️ Affected: 1 declaration(s) (line number changed)

theorem eval_hasseDeriv_eval_hasseDeriv_toPoly {F : Type*} in CompPoly/Bivariate/GuruswamiSudan/PolynomialCorrectness.lean moved from L931 to L931

sorry Tracking

No sorrys were added, removed, or affected.

Coverage Notes

Additional-instructions analysis was skipped because the full diff exceeded the analysis size budget, and partial results would be misleading.

📄 **Per-File Summaries**

CompPoly.lean: Summary unavailable — AI generation failed.
CompPoly/Bivariate/Deriv.lean: The diff adds three theorems to CompPoly/Bivariate/Deriv.lean: toPoly_injective, which proves that toPoly is injective on CBivariate R (using the existing toPoly_ofPoly lemma); shiftC_add, showing that shiftC a b distributes over addition of bivariate polynomials; and shiftC_mul, showing that shiftC a b distributes over multiplication. Both ring-homomorphism properties are proved by applying toPoly_injective after rewriting via the underlying Polynomial representation, establishing that the generic Taylor shift is a ring endomorphism of CBivariate R.
CompPoly/Bivariate/GuruswamiSudan/Implementations.lean: The file adds two new public imports (hybrid interpolation correctness and Alekhnovich root correctness), updates the module comment to reflect the benchmark-suite focus, and introduces multiple new concrete definitions: NTTFast-backed low univariate multiplication contexts (koalaBearNttFastLowMulContext, fastKoalaBearNttFastLowMulContext); approximant-basis PM‑basis contexts with leaf and compose cutoffs (approximantPMBasisLeafCutoff, approximantPMBasisComposeLeafCutoff), solution contexts, and three interpolation contexts per field (direct, subproduct, default); a budget formula for hybrid reduction (hybridReductionStepBudget) and hybrid interpolation contexts (koalaBearHybridInterpContext, fastKoalaBearHybridInterpContext); and four Alekhnovich root‑finding contexts for both field variants. These additions extend the set of concrete Guruswami‑Sudan implementations and correctness specializations exercised by the benchmark suite.
CompPoly/Bivariate/GuruswamiSudan/Interpolation.lean: This file establishes the public interface for the certified Guruswami-Sudan interpolation module. It publicly re-exports correctness theorems from five submodules—Interpolation.Correctness, Interpolation.Dense.Correctness, Interpolation.LeeOSullivan.Correctness, Interpolation.ApproximantBasis.Correctness, and Interpolation.Hybrid.Correctness—and opens a @[expose] public section to make the top-level API accessible.
CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis.lean: Added a new file ApproximantBasis.lean that publicly re-exports three submodules Basic, Algorithm, and Correctness under the CompPoly.Bivariate.GuruswamiSudan.Interpolation.ApproximantBasis namespace. This file serves as the top-level entry point for the approximant basis component of the Guruswami-Sudan interpolation algorithm, providing a convenient single import for its basic definitions, algorithm, and correctness proofs. The file includes a doc comment and an @[expose] attribute to expose the module.
CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis/Algorithm.lean: This new file introduces three executable functions for the approximant-basis interpolation step of the Guruswami‑Sudan algorithm. normalizeApproximantCandidate? normalizes a candidate bivariate polynomial using the shared interpolation vector policy. approximantBasisPositiveInterpolate handles the positive‑Y‑weight branch by building modular GS data, computing a solution basis, selecting a least shifted‑degree row, and normalizing the result. approximantBasisInterpolate serves as the top‑level entry point, delegating to a low‑message‑degree shortcut or to the positive‑weight branch. Together they provide the executable backend that turns the abstract approximant‑basis construction into a concrete algorithmic routine.
CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis/Basic.lean: This new file introduces the GSModularData structure and its construction functions (gsModuli, gsRelationColumn, gsRelationMatrixWithModuli, gsRelationMatrixWithRG, buildGSModularDataWithRG, buildGSModularData, and modularEquation) that produce the modular equations needed for the approximant‑basis backend of the Guruswami–Sudan interpolation step. The column moduli M_b = G^(s-b) are built iteratively in gsModuli, columns of the binomial relation matrix are incrementally computed by gsRelationColumn, and the full matrix is assembled by gsRelationMatrixWithModuli; buildGSModularData further constructs G and R from evaluation data. No sorry or admit appear.
CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis/Correctness.lean: Summary unavailable — AI generation failed.
CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis/ModularData.lean: This file adds roughly 692 lines establishing semantic characterizations of the executable GS (Guruswami–Sudan) modular data used in the approximant-basis construction. It introduces several new theorems: gsModuli_eq, gsModuli_size, and gsModuli_getD give a closed form for the modulus array (showing the b-th modulus is G^(s-b) and the array has size s); modByMonicWith_toPoly, dvd_modByMonicWith_sub, and modByMonicWith_eq_zero_iff_dvd connect the executable remainder to Mathlib's monic remainder and divisibility; gsRelationColumn_size, gsRelationColumn_getD_of_lt, and gsRelationColumn_getD_congr describe the size and entries of each GS relation column; and gsRelationMatrixWithModuli_entry, gsRelationMatrixWithModuli_size, and gsRelationMatrixWithModuli_matrixWidth provide analogous properties for the relation matrix. The central final theorem rowSatisfiesModularBool_gsRelationMatrix_iff identifies the executable modular row predicate over the GS data with divisibility of every sheared coefficient (hasseDeriv b Q.toPoly).eval R by G^(s-b). The file also includes auxiliary lemmas foldl_add_eq_sum, foldl_mprod_fst, toPoly_finset_sum, dvd_iff_dvd_of_dvd_sub, ofFn_rowGet, ofFn_size, ofFn_matrixWidth, hasseDeriv_toPoly_ofCoeffRow_eval, rowMulMatrixWith_congr_of_agree, rowSatisfiesModularBool_congr_of_agree, and rowSatisfiesModularBool_iff_forall. The private lemmas relationColumn_foldl_size_untouched and relationColumn_foldl_spec are used internally to prove the column theorems. There are no sorry or admit in the diff.
CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis/Multiplicity.lean: This new file Multiplicity.lean proves the semantic equivalence that underpins the ApproximantBasis backend for Guruswami–Sudan interpolation. It introduces X_sub_C_pow_dvd_iff_hasseDeriv_eval_eq_zero (characterising (X-x)^k divisibility by vanishing of Hasse derivatives), X_sub_C_pow_dvd_hasseDeriv_eval_of_dvd_sub (a shear-transfer lemma moving divisibility families between evaluation points that agree modulo X-x), and X_sub_C_pow_dvd_hasseDeriv_eval_iff_hasMultiplicity (equivalence at a single node). Auxiliary lemmas linearFactor_toPoly_eq, vanishingPolynomialArray_toPoly, and vanishingPolynomialArray_toPoly_monic connect the array vanishing polynomial to the product of linear factors over the polynomial ring. The glue lemma prod_X_sub_C_pow_dvd_of_nodup lifts per‑node (X-x)^k divisibility to divisibility by the k‑th power of the product of distinct linear factors. The main theorem vanishing_pow_dvd_hasseDeriv_eval_iff_satisfiesMultiplicityConstraints then proves that for distinct interpolation nodes, sheared coefficients (hasseDeriv b Q.toPoly).eval R.toPoly are divisible by G^(s-b) (where G is the vanishing polynomial of the nodes) iff Q satisfies the packed GS multiplicity constraints. No sorry or admit appear in the file.
CompPoly/Bivariate/GuruswamiSudan/Interpolation/Basic.lean: Added four new definitions (interpolationYCap, interpolationWidth, interpolationShifts, distinctXCoordinatesListBool, distinctXCoordinatesBool) and one new public import (CompPoly.Bivariate.CoeffRows). interpolationYCap computes a finite Y-degree cap (weightedDegreeBound / yWeight); interpolationWidth gives the number of coefficient columns (interpolationYCap + 1); interpolationShifts produces weighted-degree shifts j * yWeight params for the interpolation width; distinctXCoordinatesListBool and distinctXCoordinatesBool provide executable duplicate-x-coordinate checks on lists and arrays of point pairs, respectively, under a BEq instance. The public import makes the CoeffRows module available to this file.
CompPoly/Bivariate/GuruswamiSudan/Interpolation/Hybrid.lean: Added CompPoly/Bivariate/GuruswamiSudan/Interpolation/Hybrid.lean as a new module that publicly re-exports Algorithm and Correctness submodules, providing a single entry point for the Hybrid Guruswami-Sudan interpolation algorithm and its correctness proof.
CompPoly/Bivariate/GuruswamiSudan/Interpolation/Hybrid/Algorithm.lean: This new file introduces two interpolation functions: hybridPositiveInterpolate and hybridInterpolate. Both are defined under CompPoly.GuruswamiSudan.Hybrid. The hybridPositiveInterpolate function implements a hybrid algorithm that first attempts the Lee-O'Sullivan route with a budgeted reduction (using muldersStorjohannReduceWithFuelFast). If the reduction yields a conflict-free basis (no leading conflict), it extracts and normalizes a candidate polynomial; otherwise it falls back to the approximant-basis solver (ApproximantBasis.approximantBasisPositiveInterpolate). The hybridInterpolate function dispatches to lowMessageDegreeInterpolation when params.messageDegree ≤ 1, and otherwise delegates to hybridPositiveInterpolate. No sorry or admit appear in the code.
CompPoly/Bivariate/GuruswamiSudan/Interpolation/Hybrid/Correctness.lean: This file adds correctness proofs for the hybrid Guruswami–Sudan interpolation backend. It proves hybridPositiveInterpolate_eq_lee_or_approximant and hybridInterpolate_eq_lee_or_approximant, each stating that the hybrid's result matches either the Lee–O'Sullivan backend or the approximant-basis backend. The private lemma hybrid_probe_eq_reduceFast shows that when the budgeted Mulders–Storjohann probe ends conflict-free, it equals the full fast reduction. The definition hybridInterpContext packages hybridInterpolate into a GSInterpContext whose sound and complete fields are proven by case analysis on those equivalence theorems.
CompPoly/Bivariate/GuruswamiSudan/Interpolation/LeeOSullivan/Basic.lean: Removed the definitions interpolationYCap (a finite Y cap for positive-Y-weight interpolation backends), distinctXCoordinatesListBool (an executable duplicate-x detector for packed point lists), and distinctXCoordinatesBool (an executable duplicate-x detector for packed points). No other changes were made to the file.
CompPoly/Bivariate/GuruswamiSudan/Interpolation/WitnessDivisibility.lean: This new file introduces two definitions for checking Guruswami-Sudan interpolation witness constraints using a divisibility-based approach instead of per-point Hasse derivative evaluation. satisfiesMultiplicityConstraintsViaDivisibilityBool checks multiplicity constraints by recursively peeling digits from the base-(Y - R) expansion of Q via synthetic division (divByLinearYWith) and testing each digit for divisibility by the corresponding power of the vanishing polynomial G. interpolationWitnessIsValidViaDivisibilityBool combines this divisibility check with non-zero and weighted-degree bound checks, mirroring the existing interpolationWitnessIsValidBool. The file also provides divByLinearYWith, a variant of divByLinearY that takes an explicit multiplication context, and proves they agree via divByLinearYWith_eq_divByLinearY.
CompPoly/Bivariate/GuruswamiSudan/Interpolation/WitnessDivisibilityCorrectness.lean: This new file adds correctness proofs for the divisibility-based multiplicity and witness validity checkers used in Guruswami–Sudan interpolation. The key theorems satisfiesMultiplicityConstraintsViaDivisibilityBool_eq and interpolationWitnessIsValidViaDivisibilityBool_eq establish that these divisibility-based procedures agree with the pointwise Hasse checker satisfiesMultiplicityConstraintsBool and the direct witness validity checker interpolationWitnessIsValidBool on point sets with distinct x-coordinates. Supporting lemmas (e.g., witness_hasMultiplicity_quot, witness_viaDivisibility_iff, and several shift/coefficient identities) provide the algebraic machinery needed for the proof.
CompPoly/Bivariate/GuruswamiSudan/PolynomialCorrectness.lean: The eval_hasseDeriv_eval_hasseDeriv_toPoly theorem is changed from private to public by removing the private modifier. This makes the theorem accessible outside the module, which likely enables downstream reasoning about the relationship between univariate Hasse derivatives evaluated at specific points and the bivariate Hasse derivative in the Guruswami–Sudan context.
CompPoly/LinearAlgebra/PolynomialMatrix.lean: Added two new public imports: CompPoly.LinearAlgebra.PolynomialMatrix.Operations and CompPoly.LinearAlgebra.PolynomialMatrix.Approximant. This makes the operations and approximant submodules available to downstream files that open or import this module, extending the public API for polynomial matrices.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant.lean: This new file serves as an aggregation module for the CompPoly.LinearAlgebra.PolynomialMatrix.Approximant namespace, publicly importing five submodules: Approximant.Basic, Approximant.PMBasis, Approximant.PartialLinearization, Approximant.ModularEquation, and Approximant.Correctness. It opens a @[expose] public section, making the definitions and theorems from these submodules available to downstream code. The file itself contains no new definitions or proofs; its purpose is purely organizational, establishing a single import point for the approximant-basis polynomial-matrix infrastructure. No sorry or admit declarations are introduced by this diff.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/Basic.lean: This is a new file, CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/Basic.lean, which introduces the foundational data structures and utility functions for X-adic approximant problems over polynomial matrices. It defines the structure XAdicProblem (carrying an array of orders and a polynomial matrix), along with helper functions: maxOrder (maximum order), totalOrder (sum of orders), lowerOrders (truncate each order to d), residualOrders (orders minus d), updateShiftByRows (update a shift array based on row degrees), residualMatrixWithProduct (compute the residual matrix using an explicit product kernel), and residualMatrix (a specialized variant using MulLowContext). No sorry or admit remain in the file.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/Correctness.lean: This file introduces two theorems, modularSolutionBasis_sound and modularSolutionBasis_complete_minimal, which expose the correctness contracts of ModularSolutionBasisContext. modularSolutionBasis_sound states that any row from the basis satisfies the modular equation; modularSolutionBasis_complete_minimal asserts that given a non-zero solution row respecting the moduli, matrix width, shift, size, shifted degree, and degree bound, the basis contains a row whose shifted degree does not exceed the bound, and all basis rows respect the solution width. Both theorems delegate their proofs to the corresponding methods (sound and complete_minimal) on the context, which are now publicly accessible via this @[expose] section.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/ModularEquation.lean: Adds the new file CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/ModularEquation.lean (242 lines) as the umbrella module for the diagonal modular‑equation solver. It defines modularSolutionBasisContextViaPMBasis, which constructs a ModularSolutionBasisContext F from a PMBasisContext F by combining the filtered solution basis from the completeness development with a soundness proof via filteredSolutionBasisViaPMBasis_sound and a completeness proof that case‑analyses degreeGatePassed and uses lemmas such as me_verification_dominates, me_prodRow_facts, and me_adaptiveBasis_width. The proof is fully elaborated (no sorry or admit).
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/ModularEquation/Basic.lean: This new 769-line file introduces the diagonal modular-equation solution infrastructure for the CompPoly project. It defines the ModularEquation structure (with fields moduli and matrix) and its essential dimensions (solutionWidth, modularWidth), along with the exact-nullspace lift (exactNullspaceLift) and the associated X-adic problem (exactNullspaceProblem). A chunked variant is provided via chunkedPrincipalRows, chunkedExactNullspaceLift, chunkedExactNullspaceProblem, and chunkedExactNullspaceProblemForShift, together with entry-aware chunkedLiftOrders. The PivotDegreeProfile structure (with its insert, coversAll, discoveredAny methods) and discovery functions pivotDegreeProfileMergeRows, pivotDegreeProfileFromRows manage per-coordinate pivot-degree tracking. Several solver entry points are built: solutionBasisWithPlanViaPMBasis (generic plan), solutionBasisViaPMBasis (conservative), knownDegreeSolutionBasisViaPMBasis (reconstruction from discovered profile), unchunkedSolutionBasisViaPMBasis (debug), fullWindowSolutionBasisViaPMBasis (certified), windowedSolutionBasisViaPMBasis (certified, bounded), verificationSolutionBasisViaPMBasis, adaptiveSolutionBasis, discoverPivotDegreeProfileViaPMBasis, repairSolutionRowsViaPMBasis, knownDegreeFilteredSolutionBasisViaPMBasis, and the top-level filteredSolutionBasisViaPMBasis. The file also provides filterModularSolutionRows, modularResidualRows, helper functions for window bounds (pivotWindowCap, fullWindowDegreeBound, verificationWindowBound, gatedWindowBound), the adaptive loop state (AdaptiveSolveState), round logic (adaptiveSolutionRound, adaptiveSolutionLoop), escalation (escalateUnsettledBudgets), and settlement checks (coordinateSettled, allCoordinatesSettled). It proves several soundness theorems (rowSatisfiesModularBool_of_mem_filterModularSolutionRows, adaptiveSolutionRound_filtered_sound, adaptiveSolutionLoop_filtered_sound, adaptiveSolutionBasis_filtered_sound, filteredSolutionBasisViaPMBasis_sound) and defines the ModularSolutionBasisContext structure with a soundness and a completeness/minimality contract. No sorry or admit appear in the diff.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/ModularEquation/Completeness.lean: This new file establishes completeness for the filtered PM-basis modular solver, proving that any nonzero in-width modular solution with shifted degree within a certified verification window is dominated by a returned filtered row. Key content includes: helper lemmas on arrays, sums, polynomial degrees, row operations, and monic modular reduction (e.g., me_rowMul_toPoly, me_modByMonicWith_toPoly, me_rowSatisfies_iff); width-discipline theorems (me_solutionBasisWithPlan_width, me_adaptiveRound_width, me_adaptiveLoop_width, me_adaptiveBasis_width); a fallback solution theorem me_prodRow_facts using the modulus product; and the main theorem me_verification_dominates, which constructs a lifted exact-nullspace row, applies pmCtx.complete_minimal and pmCtx.sound, then truncates to a principal row satisfying the modular equations with degree ≤ e. No sorry or admit is present.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis.lean: This new file adds three PMBasisContext F definitions that combine a divide‑and‑conquer runtime (kernelLeafRuntimeWithLowAndCompose) with the pmBasis function and correctness proofs (pmBasis_kernelLeaf_approximates and pmBasis_kernelLeaf_complete_minimal) to provide fully verified approximant‑basis contexts. The first definition, kernelLeafPMBasisContextWithLowAndCompose, accepts separate leaf and composition cutoffs; the second, kernelLeafPMBasisContextWithLow, sets both cutoffs equal; the third, kernelLeafPMBasisContext, derives the low‑product context automatically from a given multiplication context using PolynomialMatrix.MulLowContext.fromMulContext. The file publicly imports the underlying correctness module and acts as an umbrella for the recursive PM‑basis development. No sorry or admit appear in the definitions.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/Correctness.lean: This new file proves the soundness and shifted minimality of the kernel‑leaf recursive PM‑basis. It contains the theorems pmBasisWithFuelCore_kernelLeaf_rows and pmBasis_kernelLeaf_approximates, which state that every row of the fuel‑bounded core (and hence the full basis) satisfies the X‑adic approximant conditions and has the principal row width. The theorem pmBasisWithFuelCore_kernelLeaf_rowSpan_complete establishes generation completeness: every nonzero solution row lies in the row span of the core. The final theorem pmBasis_kernelLeaf_complete_minimal proves shifted minimality: every nonzero solution row is shifted‑degree dominated by some row of the root‑normalized basis, leveraging private lemmas on pivot tables and missing‑pivot completion to show that the completed reduction is shifted weak‑Popov. No sorry or admit appears in the file.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/KernelLeaf.lean: This file introduces the entire KernelLeaf module for the scalar-kernel PM-basis leaf in an X-adic approximant problem. Key additions include: leafDegreeCap (caps coefficient degree at max 1 (maxOrder problem)), coefficientEquationIndices and coefficientMatrix / coefficientMatrixRow / coefficientMatrixRows for building the dense scalar coefficient matrix, scalarRrefRowsLoop / scalarRrefRows / basisVectorForFreeColumnRows / homogeneousKernelBasisRows for its RREF and kernel basis, vectorToPolynomialRow to map kernel vectors back to polynomial rows, kernelLeafCompletionRows / missingCompletionRows / completeMissingPivotRows for monomial completion rows, cancelKernelLeafLeadingTerm / kernelLeafConflict? / reduceKernelLeafStep / reduceKernelLeafFuel for shifted reduction of kernel rows, reduceKernelLeafRowsByPivots / reduceKernelLeafWithFuel / reduceKernelLeafRows / insertKernelLeafRowIncremental / reduceKernelLeafRowsIncremental for pivot-table and incremental reduction strategies, kernelLeafBasis which composes these to produce the full classical scalar-kernel leaf basis, and compactNonzeroRows for filtering zero rows. No sorry or admit are present.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/KernelLeafCompleteness.lean: This new file, KernelLeafCompleteness.lean (601 lines), supplies the completeness half of the kernel-leaf basis soundness work, proving that every nonzero solution row of an X-adic problem lies in the row module spanned by kernelLeafBasis problem shift. It introduces several supporting private lemmas (e.g., pm_coeff_C_mul, pm_coeff_finset_sum, pm_truncateX_eq_zero_of_coeff, and pm_rowGet_monomialUnitRow to detail structural properties used in the decomposition) and the main theorem kernelLeafBasis_rowSpan_complete. The primary decomposition is staged through three private theorems: pm_highRow_mem_rowSpan_union (rows with all coefficients below the leaf-degree cap are generated by the scalar-kernel rows), pm_lowRow_mem_rowSpan_union (rows with all coefficients at or above the cap are generated by monomial completion rows), and pm_solution_mem_rowSpan_union which combines them. The proof finally reduces the row span of the union configuration to kernelLeafBasis using reduceKernelLeafRowsIncremental_rowSpan_superset and matrix-width arguments. The new file contains no sorry or admit.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/KernelLeafScalar.lean: This new file adds the scalar kernel leaf correctness module for the PM-basis approximant. It defines scalarDot and OrthRows to express orthogonality over the first cols coordinates, proves soundness (homogeneousKernelBasisRows_dot_eq_zero) — that every vector in the emitted basis is orthogonal to all input rows — and completeness (homogeneousKernelBasisRows_complete) — that any orthogonal vector is an F-linear combination of those basis vectors, with coefficients given by its values at free columns. Supporting lemmas characterize elementary row operations (addScaledScalarRow_getD, normalizeScalarRow_getD, scalarDot_addScaledScalarRow, scalarDot_eq_pivot_mul_normalize), prove that scalarRrefRows satisfies an explicit RREF shape contract (ScalarRrefSpec with mono, pivots_lt, unit, tail_zero), and show that orthogonality is preserved forward through all RREF steps and invertible backward. No sorry or admit statements remain.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/KernelLeafSoundness.lean: This new file KernelLeafSoundness.lean proves soundness properties for the kernel-leaf basis construction in the X-adic approximant framework. It adds the theorem kernelLeafBasis_rows, which states that every row of the kernel-leaf basis satisfies the RowApproximates condition and has the principal row width. Supporting lemmas include pivotRows_invariant, reduceKernelLeafRowsByPivots_invariant, and reduceKernelLeafRowsIncremental_invariant, which propagate predicates (such as the soundness property) through pivot-table reduction and incremental reduction. The file also proves vectorToPolynomialRow_approximates (reconstructed vectors from the homogeneous kernel basis satisfy the X-adic conditions), vectorToPolynomialRow_rowToCoefficientVector (the round-trip between polynomial rows and their packed coefficient vectors is identity for well-formed rows), and coefficientMatrixRows_dot_eq_zero_of_approximates (the converse: approximating polynomial rows yield coefficient vectors orthogonal to all scalar coefficient rows). The private lemmas pm_foldl_push_toList, pm_doubleFoldl_toList, mem_coefficientEquationIndices, pm_sum_range_mul, coefficientMatrixRow_getD, rowToCoefficientVector_getD, mem_coefficientEquationIndices_bounds, and pm_pack_index provide combinatorial and algebraic infrastructure. No sorry or admit are present.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/KernelLeafSpan.lean: This file adds a new module (1216 lines) establishing row-span preservation for the kernel-leaf pivot-table reduction in the PMBasis approximant construction. It proves that cancelKernelLeafLeadingTerm is the Mulders–Storjohann cancellation (cancelKernelLeafLeadingTerm_eq_cancelShifted), respects row span membership in both directions, and strictly decreases the shifted-row measure. The main function insertKernelLeafPivotRowWithFuel is shown to preserve slot-width and leading-position invariants (insertKernelLeafPivotRowWithFuel_pivotInv), not to erase occupied slots (insertKernelLeafPivotRowWithFuel_persist), to increase the pivot-table measure by at most the inserted row's measure (insertKernelLeafPivotRowWithFuel_measure_le), and to keep the carried row and all stored rows in the row span of the final pivot rows when the fuel bound is sufficient (insertKernelLeafPivotRowWithFuel_rowSpan). These per-insertion lemmas are lifted to the full fold over all source rows in insertKernelLeaf_foldl_rowSpan and insertKernelLeaf_foldl_pivotInv, and the total fuel is bounded in sum_shiftedRowMeasure_lt_reduceKernelLeafFuel. The two top-level soundness theorems reduceKernelLeafRowsByPivots_rowSpan_superset and reduceKernelLeafRowsIncremental_rowSpan_superset assert that every nonzero source row belongs to the row span of the reduced matrix. Supporting infrastructure includes rowIsZero_eq_zeroRow, wellFormed_of_sizes, pivotTableMeasure (with update/empty lemmas), and rowSpan_pivotRows_trans for lifting membership across successive pivot tables.
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/Recursion.lean: This new file introduces the recursive PM-basis driver for polynomial matrix approximants. It defines the PMBasisRuntime structure holding multiplication contexts and leaf‑basis data, three factory functions (kernelLeafRuntimeWithLowAndCompose, kernelLeafRuntimeWithLow, kernelLeafRuntime) that instantiate the runtime with the kernel‑leaf solver, and the fuel‑bounded divide‑and‑conquer algorithm pmBasisWithFuelCore. Root normalization is provided by pmBasisNormalizeRoot (weak‑Popov reduction plus completion of missing pivot rows), and the entry point pmBasis packages everything together. Two theorems (completeMissingPivotRows_size_pos, pmBasisNormalizeRoot_size_pos) guarantee that the resulting basis is non‑empty whenever the problem matrix is non‑empty. Finally, the PMBasisContext structure bundles the runtime with the basis function and the soundness/completeness contract fields (sound, complete_minimal).
CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PMBasis/XAdicSoundness.lean: This new file (791 lines) adds the RowApproximates predicate and a comprehensive toolkit of theorems that characterize it and prove its closure under all row operations used in the leaf reduction, completion, and composition steps of the X-adic approximant driver.

Key definitions and theorems introduced:

RowApproximates definition: a row approximates an X-adic problem when each column product vanishes under truncateX to the required order.
truncateX_eq_zero_iff_X_pow_dvd: equivalence between truncateX order p = 0 and X^order ∣ p.toPoly.
rowApproximates_iff: reformulation using divisibility of toPoly sums, one column at a time.
Closure theorems: rowApproximates_rowSub, rowApproximates_rowScaleCoeffX, rowApproximates_cancelKernelLeafLeadingTerm, insertKernelLeafPivotRowWithFuel_approximates, pivotRows_approximates, reduceKernelLeafRowsByPivots_approximates, missingCompletionRows_approximates, completeMissingPivotRows_approximates.
rowApproximates_monomialUnitRow: monomial unit rows of sufficiently high degree satisfy every X-adic condition.
rowApproximates_composed: soundness of one PM-basis composition step — a residual-approximant row times a lower-approximant basis approximates the full problem.
Supporting lemmas: pm_toPoly_finset_sum, rowGet_rowMulMatrixWith_toPoly, polynomialScaleCoeffX_toPoly, coeffXPower_toPoly, divXTrunc_coeff, etc.

The file contains no sorry or admit statements.

CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PartialLinearization.lean: This new file (CompPoly/LinearAlgebra/PolynomialMatrix/Approximant/PartialLinearization.lean) introduces the core data structures and executable helpers for partial linearization — a technique that sizes expanded X-adic problem dimensions locally per coordinate rather than using one global oversized order. Specifically, it defines:
Chunk/Delta computation: ceilDivFallback, modulusDegreeMass, chunkDelta, and linearizedOrders for determining the chunk size from moduli degrees.
Shift management: maxShiftDegree, principalShiftOffset, quotientShift, liftedPrincipalShift, and exactNullspaceShift for constructing coordinate shifts used in the exact-nullspace lift.
Principal chunk structures and construction: the PrincipalChunk structure; functions principalChunkCount, principalChunks, principalUnitChunks, fallbackPivotDegree, pivotDegreeAt, principalChunkCountFromPivotDegree, and principalChunksFromPivotDegrees to generate chunk plans from either a shifted-degree profile or a discovered pivot-degree profile.
Partial linearization plans: the PartialLinearizationPlan structure; builders partialLinearizationPlan, partialLinearizationPlanFromPivotDegrees, and unchunkedPartialLinearizationPlan (the latter disabling chunking for principal coordinates).
Polynomial and row operations: xPowPolynomial, shiftPolynomialX, shiftRowX, chunkedExactNullspaceShift, compressChunkedPrincipalRow, and compressChunkedPrincipalRows for shifting, chunked shift construction, and compressing chunked rows back to principal coordinates.

No sorry or admit are present; all definitions are fully implemented in this initial file.

CompPoly/LinearAlgebra/PolynomialMatrix/MuldersStorjohannCorrectness/Fast.lean: The diff refines the docstring comment describing the fast reducer, rephrasing it to say 'once per conflict scan' instead of 'once per scan'. In the body of muldersStorjohannReduceWithFuelFast_eq, the some case of the shiftedLeadingConflict? match now binds the matched value as pair (instead of using an underscore), and the simp block below it is unchanged. No sorry or admit are introduced.
CompPoly/LinearAlgebra/PolynomialMatrix/MuldersStorjohannCorrectness/Reduction.lean: The diff adds the theorem muldersStorjohannReduceWithFuel_eq_of_no_conflict with a complete proof by induction on the fuel parameter. The theorem states that if two invocations of muldersStorjohannReduceWithFuel with distinct fuel values f and g both yield a matrix for which shiftedLeadingConflict? returns none under the given shift, then the two resulting matrices are equal. This shows that the fueled reduction function is deterministic once a conflict-free matrix is reached—the output does not depend on how much extra fuel remains.
CompPoly/LinearAlgebra/PolynomialMatrix/MuldersStorjohannCorrectness/WeakPopovMinimal.lean: This new file introduces two theorems that establish a predictable-degree property for shifted weak-Popov matrices and re-derive the least-row minimality guarantee of the Mulders-Storjohann reducer. shiftedWeakPopov_least_row_minimal shows that for any well-formed matrix B satisfying ShiftedWeakPopov B shift, every member row of RowSpan B with a defined shifted degree is bounded below by the shifted degree of some row in MatrixRows B, without requiring any alignment between the shift and the matrix width. muldersStorjohannReduce_least_row_minimal_of_weakPopov then applies this general result to muldersStorjohannReduce M shift (using muldersStorjohannReduce_wellFormed, muldersStorjohannReduce_weakPopov, and muldersStorjohannReduce_rowSpan_eq) to prove that the reducer output contains a row whose shifted degree is a lower bound for any row-span member's shifted degree, assuming the shift size matches the matrix width. The proof is complete with no sorry or admit.
CompPoly/LinearAlgebra/PolynomialMatrix/Operations.lean: This new file defines a comprehensive library of executable operations for polynomial rows and row-major polynomial matrices over a type F. It introduces truncateX and its correctness theorem truncateX_coeff for X-adic truncation; a structure MulLowContext with mulLow and mulLow_eq for low-product multiplication; basic matrix constructors (ofFn, zero, identity); element-wise arithmetic (add, sub, transpose, block, joinSquareBlocks); matrix multiplication via mulWith and mul using explicit CPolynomial.MulContext; utilities for padding, trimming, coefficient caps, and column truncation (padSquare, trimShape, polynomialCoeffCap, productCoeffCap, rowTruncateColumns, truncateColumns); Strassen-style matrix multiplication with output-column truncation (mulTruncColumnStrassenWith, mulTruncColumnStrassenWithFuel); bounded multiplication from inferred degree caps (mulBoundedWith, rowMulMatrixBoundedWith); full Strassen multiplication (mulStrassenWith, mulStrassenWithFuel); modular reduction by diagonal moduli (modDiagonalWith, rowModDiagonalWith, modByMonicWith); and shifted-degree row selection via leastShiftedDegreeRow?, leastShiftedDegreeChoice?, RowChoice, and betterRowChoice. No sorry or admit appear anywhere in the diff.
CompPoly/LinearAlgebra/PolynomialMatrix/RowSelection.lean: The file RowSelection.lean is added, providing correctness facts for the least-shifted-degree row selection helpers in PolynomialMatrix.Operations. It defines the predicate RowChoiceValid (index, row, degree validity w.r.t. matrix and shift) and proves private lemmas about betterRowChoice (degree order) and the fold function leastShiftedDegreeFold (preserving degree bounds and valid choices). The public theorems leastShiftedDegreeChoice?_some_valid, leastShiftedDegreeChoice?_degree_le, leastShiftedDegreeChoice?_some_of_degree, and leastShiftedDegreeRow?_some_valid then establish that leastShiftedDegreeChoice? returns a valid choice, that its degree is ≤ the shifted degree of any row, that such a choice always exists when a row has a shifted degree, and that leastShiftedDegreeRow? corresponds to such a valid choice. All proofs are complete, with no sorry or admit.
CompPoly/LinearAlgebra/PolynomialMatrix/StrassenCorrectness.lean: This new file, StrassenCorrectness.lean, provides formal correctness proofs for the polynomial-matrix product algorithms defined in Operations.lean. It establishes that the naive row-by-matrix product (rowGet_rowMulMatrixWith) computes entrywise convolution sums, that the degree-capped bounded product equals the naive product (mulBoundedWith_eq_mulWith), and that the fuel-bounded Strassen recursion (mulStrassenWithFuel_eq_mulWith) and its column-truncated variant (mulTruncColumnStrassenWithFuel_eq_truncateColumns) both coincide with the corresponding naive products. The file also contains many supporting lemmas on array access, foldl sums, truncateX arithmetic, ofFn matrix construction, and the seven-term Strassen sum identities that appear in the block-matrix expansion.
tests/CompPolyTests.lean: Added two public import statements to tests/CompPolyTests.lean: CompPolyTests.Bivariate.GuruswamiSudan.Interpolation.ApproximantBasis and CompPolyTests.LinearAlgebra.PolynomialMatrix.Approximant. These re-export the respective modules' tests, incorporating new test coverage for the approximant basis construction within the Guruswami–Sudan interpolation framework and for polynomial matrix approximant routines from the linear algebra subdirectory.
tests/CompPolyTests/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis.lean: This file adds a comprehensive test suite for the Guruswami–Sudan interpolation module. It defines concrete parameters, helper contexts, and a series of #guard assertions that verify: (1) basic parameter properties (e.g., interpolationYCap, interpolationWidth, interpolationShifts, distinctXCoordinatesBool); (2) the structure and values of constructed GSModularData (moduli sizes, matrix dimensions, specific matrix entries, row modularity checks); (3) that approximantBasisPositiveInterpolate returns none for duplicate x‑coordinates; (4) that approximantBasisInterpolate succeeds and produces a witness satisfying interpolationWitnessIsValidBool for several parameter/point combinations (including small and non‑codeword stress cases); (5) that the higher‑level approxContext5.interpolate succeeds with the same witness validity; and (6) that gsCore returns a list of bounded size. No sorry or admit are present; all tests use #guard for automatic checking.
tests/CompPolyTests/LinearAlgebra/PolynomialMatrix/Approximant.lean: The file tests/CompPolyTests/LinearAlgebra/PolynomialMatrix/Approximant.lean is newly added and provides executable #guard checks for the X-adic approximant problem sizing, recursive PM-basis plumbing, partial-linearization orders, and exact-nullspace lifts. It defines private test data (e.g., F3 := ZMod 3, problem, fullRankProblem, moduli, equation, chunkPlan, profileChunkPlan, productionPMCtx, discoveredProfile, knownDegreePlan, knownDegreeRows, productionRows, debugUnchunkedRows, leastChoiceRows) and then asserts properties such as the correctness of maxOrder, totalOrder, lowerOrders, residualOrders, leafDegreeCap, coefficientMatrix dimensions, kernelLeafBasis output, rowsContainLeadingPosition, missingCompletionRows, matrix multiplication via mulBoundedWith/mulStrassenWith/mulTruncColumnStrassenWith vs. mulWith/mulTruncColumnWith, pmBasis size and width, modulusDegreeMass, chunkDelta, linearizedOrders, chunkPlan chunk structure, chunkedExactNullspaceShift, profileFromRows.degrees, chunkedExactNullspaceLift dimensions and entries, compressChunkedPrincipalRow, exactNullspaceLift dimensions and entries, and the correctness of knownDegreeCompressedRows, knownDegreeRows, knownDegreeFilteredRows, productionRows, debugUnchunkedRows and leastShiftedDegreeChoice?.
2 file(s) filtered as noise (lockfiles, generated, or trivial): ROADMAP.md, docs/wiki/coding-theory.md

Last updated: 2026-08-10 19:48 UTC.

Re-land olympichek's approximant-basis and hybrid Guruswami-Sudan interpolation backends from #255 onto the roots re-land stack (#290). - PolynomialMatrix.Approximant: PM-Basis, modular key equations, partial linearization, with soundness/completeness - GS ApproximantBasis + Hybrid (budgeted Lee fallback) as GSInterpContext - WitnessDivisibility quasi-linear multiplicity check - Named KoalaBear contexts in Implementations; matrix ops/Strassen helpers - Module-system port; shortened ApproximantBasis leaf paths for lint - Docs/ROADMAP: four interpolation backends documented Co-authored-by: Derek Sorensen <d@dhsorens.com>

The approximant/hybrid stack elaborated 70 declarations with overlapping instance parameters. `main` and #290 are warning-free, so this was a regression against a clean baseline and against docs/wiki/typeclass-minimization.md. Two distinct causes: - 63x `[Field F]` with a redundant `[Nontrivial F]`, from eight `variable` lines carrying both. Removed the redundant binder and the matching entries in the dependent `omit ... in` lines. - 7x `[Field F]` with a redundant `[Zero F]`, on declarations sitting inside a `variable ... [Field F]` scope. This is the harmful case: Lean reports the two can infer conflicting `Zero F`, an instance diamond. Removed `[Zero F]` from the six `ModularEquation` accessors and from `pmBasisFuel`. The `[Zero F]` on the `ModularEquation` and `AdaptiveSolveState` structures is kept: those rebind `F` themselves, do not overlap, and are correct typeclass minimization. No signature is weakened. Every affected declaration already carried `[Field F]` through the enclosing `variable`, so the removed binders were duplicates rather than assumptions. Verified: lake build (0 warnings, 0 errors), lake test, lint-style, update-lib/check-imports, check-docs-integrity.

This was referenced Aug 7, 2026

feat(bivariate): approximant-basis and hybrid interpolation for GS decoder #255

Open

feat(univariate): Shoup and Las Vegas root-search backends #290

Open

olympichek and others added 2 commits August 10, 2026 20:41

dhsorens force-pushed the re-land/gs-approximant branch from b451fac to d07299b Compare August 10, 2026 19:41

Navigation Menu

Uh oh!

feat(bivariate): approximant-basis and hybrid GS interpolation - #291

feat(bivariate): approximant-basis and hybrid GS interpolation#291
dhsorens wants to merge 2 commits into
re-land/roots-shoup-lasvegasfrom
re-land/gs-approximant

dhsorens commented Aug 7, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Aug 7, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Aug 7, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

dhsorens commented Aug 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Stack

Attribution

Supersedes

Idiom notes

Test plan

Uh oh!

github-actions Bot commented Aug 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Build Timing Report

Incremental Rebuild Signal

Slowest Current Build Files (warm library build)

Uh oh!

github-actions Bot commented Aug 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 PR Summary

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

dhsorens commented Aug 7, 2026 •

edited

Loading

github-actions Bot commented Aug 7, 2026 •

edited

Loading

github-actions Bot commented Aug 7, 2026 •

edited

Loading