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

CompPoly.lean

@@ -12,10 +12,20 @@ import CompPoly.Bivariate.GuruswamiSudan.Executable
 import CompPoly.Bivariate.GuruswamiSudan.Filter
 import CompPoly.Bivariate.GuruswamiSudan.FilterCorrectness
 import CompPoly.Bivariate.GuruswamiSudan.Implementations
+import CompPoly.Bivariate.GuruswamiSudan.Interpolation
+import CompPoly.Bivariate.GuruswamiSudan.Interpolation.ApproximantBasis
+import CompPoly.Bivariate.GuruswamiSudan.Interpolation.ApproximantBasis.Algorithm
+import CompPoly.Bivariate.GuruswamiSudan.Interpolation.ApproximantBasis.Basic
+import CompPoly.Bivariate.GuruswamiSudan.Interpolation.ApproximantBasis.Correctness
+import CompPoly.Bivariate.GuruswamiSudan.Interpolation.ApproximantBasis.Correctness.ModularData
+import CompPoly.Bivariate.GuruswamiSudan.Interpolation.ApproximantBasis.Correctness.Multiplicity
 import CompPoly.Bivariate.GuruswamiSudan.Interpolation.Basic
 import CompPoly.Bivariate.GuruswamiSudan.Interpolation.Correctness
 import CompPoly.Bivariate.GuruswamiSudan.Interpolation.Dense.Algorithm
 import CompPoly.Bivariate.GuruswamiSudan.Interpolation.Dense.Correctness
+import CompPoly.Bivariate.GuruswamiSudan.Interpolation.Hybrid
+import CompPoly.Bivariate.GuruswamiSudan.Interpolation.Hybrid.Algorithm
+import CompPoly.Bivariate.GuruswamiSudan.Interpolation.Hybrid.Correctness
 import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan
 import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Algorithm
 import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Basic
@@ -29,6 +39,8 @@ import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.
 import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.Rows
 import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.Selection
 import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.Soundness
+import CompPoly.Bivariate.GuruswamiSudan.Interpolation.WitnessDivisibility
+import CompPoly.Bivariate.GuruswamiSudan.Interpolation.WitnessDivisibilityCorrectness
 import CompPoly.Bivariate.GuruswamiSudan.Polynomial
 import CompPoly.Bivariate.GuruswamiSudan.PolynomialCorrectness
 import CompPoly.Bivariate.GuruswamiSudan.Root.Alekhnovich.Algorithm
@@ -114,6 +126,22 @@ import CompPoly.LinearAlgebra.Dense.RowOpsCorrectness
 import CompPoly.LinearAlgebra.Dense.RrefSemantics
 import CompPoly.LinearAlgebra.Dense.RrefShape
 import CompPoly.LinearAlgebra.PolynomialMatrix
+import CompPoly.LinearAlgebra.PolynomialMatrix.Approximant
+import CompPoly.LinearAlgebra.PolynomialMatrix.Approximant.Basic
+import CompPoly.LinearAlgebra.PolynomialMatrix.Approximant.Correctness
+import CompPoly.LinearAlgebra.PolynomialMatrix.Approximant.ModularEquation
+import CompPoly.LinearAlgebra.PolynomialMatrix.Approximant.ModularEquation.Basic
+import CompPoly.LinearAlgebra.PolynomialMatrix.Approximant.ModularEquation.Completeness
+import CompPoly.LinearAlgebra.PolynomialMatrix.Approximant.PMBasis
+import CompPoly.LinearAlgebra.PolynomialMatrix.Approximant.PMBasis.Correctness
+import CompPoly.LinearAlgebra.PolynomialMatrix.Approximant.PMBasis.KernelLeaf
+import CompPoly.LinearAlgebra.PolynomialMatrix.Approximant.PMBasis.KernelLeafCompleteness
+import CompPoly.LinearAlgebra.PolynomialMatrix.Approximant.PMBasis.KernelLeafScalar
+import CompPoly.LinearAlgebra.PolynomialMatrix.Approximant.PMBasis.KernelLeafSoundness
+import CompPoly.LinearAlgebra.PolynomialMatrix.Approximant.PMBasis.KernelLeafSpan
+import CompPoly.LinearAlgebra.PolynomialMatrix.Approximant.PMBasis.Recursion
+import CompPoly.LinearAlgebra.PolynomialMatrix.Approximant.PMBasis.XAdicSoundness
+import CompPoly.LinearAlgebra.PolynomialMatrix.Approximant.PartialLinearization
 import CompPoly.LinearAlgebra.PolynomialMatrix.Basic
 import CompPoly.LinearAlgebra.PolynomialMatrix.Degree
 import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohann
@@ -127,9 +155,13 @@ import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.Meas
 import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.Minimal
 import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.Reduction
 import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.RowOps
+import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.WeakPopovMinimal
+import CompPoly.LinearAlgebra.PolynomialMatrix.Operations
+import CompPoly.LinearAlgebra.PolynomialMatrix.RowSelection
 import CompPoly.LinearAlgebra.PolynomialMatrix.RowSpan
 import CompPoly.LinearAlgebra.PolynomialMatrix.Shifted
 import CompPoly.LinearAlgebra.PolynomialMatrix.ShiftedReduction
+import CompPoly.LinearAlgebra.PolynomialMatrix.StrassenCorrectness
 import CompPoly.Multilinear.Basic
 import CompPoly.Multilinear.Equiv
 import CompPoly.Multilinear.ManyEval

CompPoly/Bivariate/Deriv.lean

@@ -345,6 +345,29 @@ theorem hasMultiplicity_succ [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial
   intro h i j hij
   exact h i j (by omega)
 
+/-- `toPoly` is injective on canonical bivariate polynomials. -/
+theorem toPoly_injective [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R]
+    [DecidableEq R] {P Q : CBivariate R} (h : toPoly P = toPoly Q) : P = Q := by
+  rw [← toPoly_ofPoly P, ← toPoly_ofPoly Q, h]
+
+/-- The generic Taylor shift is additive. -/
+theorem shiftC_add [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R]
+    (a b : R) (P Q : CBivariate R) :
+    shiftC a b (P + Q) = shiftC a b P + shiftC a b Q := by
+  apply toPoly_injective
+  rw [toPoly_add, shiftC_toPoly, shiftC_toPoly, shiftC_toPoly, toPoly_add]
+  unfold Polynomial.Bivariate.shift
+  rw [Polynomial.add_comp, Polynomial.map_add]
+
+/-- The generic Taylor shift is multiplicative. -/
+theorem shiftC_mul [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R]
+    [DecidableEq R] (a b : R) (P Q : CBivariate R) :
+    shiftC a b (P * Q) = shiftC a b P * shiftC a b Q := by
+  apply toPoly_injective
+  rw [toPoly_mul, shiftC_toPoly, shiftC_toPoly, shiftC_toPoly, toPoly_mul]
+  unfold Polynomial.Bivariate.shift
+  rw [Polynomial.mul_comp, Polynomial.map_mul]
+
 /-- The decidable check agrees with the propositional multiplicity. -/
 theorem hasMultiplicity_iff_check [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R]
     [DecidableEq R] (Q : CBivariate R) (r : ℕ) (a b : R) :

CompPoly/Bivariate/GuruswamiSudan/Implementations.lean

@@ -6,18 +6,21 @@ Authors: Valerii Huhnin
 
 import CompPoly.Bivariate.GuruswamiSudan.Executable
 import CompPoly.Bivariate.GuruswamiSudan.Interpolation.Dense.Correctness
+import CompPoly.Bivariate.GuruswamiSudan.Interpolation.Hybrid.Correctness
 import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness
-import CompPoly.Bivariate.GuruswamiSudan.Root.FieldRoots.KoalaBear
+import CompPoly.Bivariate.GuruswamiSudan.Root.Alekhnovich.Correctness
 import CompPoly.Bivariate.GuruswamiSudan.Root.RothRuckenstein.Correctness
+import CompPoly.Bivariate.GuruswamiSudan.Root.FieldRoots.KoalaBear
 import CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.Fast
 import CompPoly.Univariate.BatchEval.Context
 import CompPoly.Univariate.NTT.KoalaBear
 
 /-!
 # Guruswami-Sudan Concrete Implementations
 
-Named concrete dense and Lee-O'Sullivan interpolation/Roth-Ruckenstein
-implementations and correctness theorem specializations for the decoder surface.
+Named concrete dense-interpolation/Roth-Ruckenstein implementations and
+correctness theorem specializations for the implementations exercised by the
+benchmark suite.
 -/
 
 namespace CompPoly
@@ -36,6 +39,13 @@ def fastKoalaBearDenseInterpContext : GSInterpContext KoalaBear.Fast.Field :=
 def koalaBearNttFastMulContext : CPolynomial.MulContext KoalaBear.Field :=
   CPolynomial.MulContext.nttFast CPolynomial.NTT.KoalaBear.bestDomainForLength?
 
+/-- NTTFast-backed low univariate multiplication over canonical KoalaBear. -/
+def koalaBearNttFastLowMulContext :
+    PolynomialMatrix.MulLowContext KoalaBear.Field :=
+  PolynomialMatrix.MulLowContext.raw koalaBearNttFastMulContext
+    (CPolynomial.NTTFast.FastMulLow.withFallback
+      CPolynomial.NTT.KoalaBear.bestDomainForLength?)
+
 /-- NTTFast-backed univariate monic remainders over canonical KoalaBear. -/
 def koalaBearNttFastModContext : CPolynomial.ModContext KoalaBear.Field :=
   CPolynomial.ModContext.reversalNttFast CPolynomial.NTT.KoalaBear.bestDomainForLength?
@@ -49,6 +59,13 @@ def koalaBearNttFastBatchEvalContext : CPolynomial.BatchEvalContext KoalaBear.Fi
 def fastKoalaBearNttFastMulContext : CPolynomial.MulContext KoalaBear.Fast.Field :=
   CPolynomial.MulContext.nttFast CPolynomial.NTT.KoalaBear.fastBestDomainForLength?
 
+/-- NTTFast-backed low univariate multiplication over native-word fast KoalaBear. -/
+def fastKoalaBearNttFastLowMulContext :
+    PolynomialMatrix.MulLowContext KoalaBear.Fast.Field :=
+  PolynomialMatrix.MulLowContext.raw fastKoalaBearNttFastMulContext
+    (CPolynomial.NTTFast.FastMulLow.withFallback
+      CPolynomial.NTT.KoalaBear.fastBestDomainForLength?)
+
 /-- NTTFast-backed univariate monic remainders over native-word fast KoalaBear. -/
 def fastKoalaBearNttFastModContext : CPolynomial.ModContext KoalaBear.Fast.Field :=
   CPolynomial.ModContext.reversalNttFast CPolynomial.NTT.KoalaBear.fastBestDomainForLength?
@@ -90,6 +107,117 @@ def fastKoalaBearLeeSubproductInterpContext : GSInterpContext KoalaBear.Fast.Fie
     fastKoalaBearNttFastBatchEvalContext
     (PolynomialMatrix.muldersStorjohannFastReducerContext KoalaBear.Fast.Field)
 
+/-- PM-basis scalar-kernel cutoff for the approximant-basis interpolation backend.
+
+The recursive solver handles all larger orders with low-product residuals and
+block matrix composition; dense scalar linear algebra is reserved for
+small bounded leaves. -/
+def approximantPMBasisLeafCutoff : Nat := 8
+
+/-- Polynomial-matrix basis-composition cutoff for the approximant backend.
+The current GS interpolation shapes are narrow enough that direct bounded
+composition is faster than recursing Strassen down to unit blocks. -/
+def approximantPMBasisComposeLeafCutoff : Nat := 8
+
+/-- Recursive approximant-basis PM-basis context over canonical KoalaBear. -/
+def koalaBearApproximantPMBasisContext :
+    PolynomialMatrix.Approximant.PMBasisContext KoalaBear.Field :=
+  PolynomialMatrix.Approximant.kernelLeafPMBasisContextWithLowAndCompose
+    koalaBearNttFastMulContext koalaBearNttFastLowMulContext
+    approximantPMBasisLeafCutoff approximantPMBasisComposeLeafCutoff
+
+/-- Diagonal modular-equation solution context over canonical KoalaBear. -/
+def koalaBearApproximantSolutionContext :
+    PolynomialMatrix.Approximant.ModularSolutionBasisContext KoalaBear.Field :=
+  PolynomialMatrix.Approximant.modularSolutionBasisContextViaPMBasis
+    koalaBearNttFastMulContext koalaBearNttFastModContext
+    koalaBearApproximantPMBasisContext
+
+/-- Approximant-basis interpolation over canonical KoalaBear. -/
+def koalaBearApproximantBasisDirectInterpContext : GSInterpContext KoalaBear.Field :=
+  ApproximantBasis.approximantBasisInterpContext
+    (CPolynomial.VanishingPolynomialContext.direct (F := KoalaBear.Field))
+    (CPolynomial.BatchEvalContext.horner KoalaBear.Field)
+    koalaBearApproximantSolutionContext
+
+/-- Approximant-basis interpolation over canonical KoalaBear with
+subproduct-tree vanishing setup. -/
+def koalaBearApproximantBasisSubproductInterpContext : GSInterpContext KoalaBear.Field :=
+  ApproximantBasis.approximantBasisInterpContext
+    (CPolynomial.VanishingPolynomialContext.subproduct
+      koalaBearNttFastMulContext)
+    koalaBearNttFastBatchEvalContext
+    koalaBearApproximantSolutionContext
+
+/-- Default approximant-basis interpolation over canonical KoalaBear. -/
+def koalaBearApproximantBasisInterpContext : GSInterpContext KoalaBear.Field :=
+  koalaBearApproximantBasisSubproductInterpContext
+
+/-- Recursive approximant-basis PM-basis context over native-word fast KoalaBear. -/
+def fastKoalaBearApproximantPMBasisContext :
+    PolynomialMatrix.Approximant.PMBasisContext KoalaBear.Fast.Field :=
+  PolynomialMatrix.Approximant.kernelLeafPMBasisContextWithLowAndCompose
+    fastKoalaBearNttFastMulContext fastKoalaBearNttFastLowMulContext
+    approximantPMBasisLeafCutoff approximantPMBasisComposeLeafCutoff
+
+/-- Diagonal modular-equation solution context over native-word fast KoalaBear. -/
+def fastKoalaBearApproximantSolutionContext :
+    PolynomialMatrix.Approximant.ModularSolutionBasisContext KoalaBear.Fast.Field :=
+  PolynomialMatrix.Approximant.modularSolutionBasisContextViaPMBasis
+    fastKoalaBearNttFastMulContext fastKoalaBearNttFastModContext
+    fastKoalaBearApproximantPMBasisContext
+
+/-- Approximant-basis interpolation over native-word fast KoalaBear. -/
+def fastKoalaBearApproximantBasisDirectInterpContext :
+    GSInterpContext KoalaBear.Fast.Field :=
+  ApproximantBasis.approximantBasisInterpContext
+    (CPolynomial.VanishingPolynomialContext.direct (F := KoalaBear.Fast.Field))
+    (CPolynomial.BatchEvalContext.horner KoalaBear.Fast.Field)
+    fastKoalaBearApproximantSolutionContext
+
+/-- Approximant-basis interpolation over native-word fast KoalaBear with
+subproduct-tree vanishing setup. -/
+def fastKoalaBearApproximantBasisSubproductInterpContext :
+    GSInterpContext KoalaBear.Fast.Field :=
+  ApproximantBasis.approximantBasisInterpContext
+    (CPolynomial.VanishingPolynomialContext.subproduct
+      fastKoalaBearNttFastMulContext)
+    fastKoalaBearNttFastBatchEvalContext
+    fastKoalaBearApproximantSolutionContext
+
+/-- Default approximant-basis interpolation over native-word fast KoalaBear. -/
+def fastKoalaBearApproximantBasisInterpContext :
+    GSInterpContext KoalaBear.Fast.Field :=
+  fastKoalaBearApproximantBasisSubproductInterpContext
+
+/-- Mulders-Storjohann step budget for the hybrid interpolation backend: the
+ski-rental rent/buy break-even, set near the cost ratio between one
+approximant-fallback solve and one reduction step. Both scale with the input
+mass, so the ratio is proportional to `ℓ^(ω−1)` (with `ℓ + 1` the module
+width) and independent of `n` and `m` under softly-linear multiplication;
+the constant is calibrated from the `n = 5040` long-code benchmark shape. -/
+def hybridReductionStepBudget (params : GSInterpParams) : Nat :=
+  500 * leeOSullivanWidth params * leeOSullivanWidth params
+
+/-- Hybrid interpolation (budgeted Lee-O'Sullivan reduction with approximant
+fallback) over canonical KoalaBear. -/
+def koalaBearHybridInterpContext : GSInterpContext KoalaBear.Field :=
+  Hybrid.hybridInterpContext
+    (CPolynomial.VanishingPolynomialContext.subproduct koalaBearNttFastMulContext)
+    koalaBearNttFastBatchEvalContext
+    koalaBearApproximantSolutionContext
+    hybridReductionStepBudget
+
+/-- Hybrid interpolation (budgeted Lee-O'Sullivan reduction with approximant
+fallback) over native-word fast KoalaBear. -/
+def fastKoalaBearHybridInterpContext : GSInterpContext KoalaBear.Fast.Field :=
+  Hybrid.hybridInterpContext
+    (CPolynomial.VanishingPolynomialContext.subproduct
+      fastKoalaBearNttFastMulContext)
+    fastKoalaBearNttFastBatchEvalContext
+    fastKoalaBearApproximantSolutionContext
+    hybridReductionStepBudget
+
 /-- Roth-Ruckenstein root backend over canonical KoalaBear. -/
 def koalaBearRothRootContext : GSRootContext KoalaBear.Field :=
   rothRuckensteinRootContext KoalaBear.Field koalaBearFieldRootContext
@@ -106,6 +234,22 @@ def fastKoalaBearRothRootContext : GSRootContext KoalaBear.Fast.Field :=
 def fastKoalaBearRothNttFastRootContext : GSRootContext KoalaBear.Fast.Field :=
   rothRuckensteinRootContext KoalaBear.Fast.Field fastKoalaBearNttFastFieldRootContext
 
+/-- Alekhnovich root backend over canonical KoalaBear. -/
+def koalaBearAlekhnovichRootContext : GSRootContext KoalaBear.Field :=
+  alekhnovichRootContext KoalaBear.Field koalaBearFieldRootContext
+
+/-- Alekhnovich root backend over canonical KoalaBear with NTTFast field roots. -/
+def koalaBearAlekhnovichNttFastRootContext : GSRootContext KoalaBear.Field :=
+  alekhnovichRootContext KoalaBear.Field koalaBearNttFastFieldRootContext
+
+/-- Alekhnovich root backend over native-word fast KoalaBear. -/
+def fastKoalaBearAlekhnovichRootContext : GSRootContext KoalaBear.Fast.Field :=
+  alekhnovichRootContext KoalaBear.Fast.Field fastKoalaBearFieldRootContext
+
+/-- Alekhnovich root backend over native-word fast KoalaBear with NTTFast field roots. -/
+def fastKoalaBearAlekhnovichNttFastRootContext : GSRootContext KoalaBear.Fast.Field :=
+  alekhnovichRootContext KoalaBear.Fast.Field fastKoalaBearNttFastFieldRootContext
+
 /-- Filtered dense/Roth context over canonical KoalaBear. -/
 def koalaBearDenseRothContext : GSFilteredCoreContext KoalaBear.Field :=
   filteredCoreContextOfInterpRootContexts koalaBearDenseInterpContext koalaBearRothRootContext

CompPoly/Bivariate/GuruswamiSudan/Interpolation.lean

@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2026 CompPoly Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Valerii Huhnin
+-/
+
+import CompPoly.Bivariate.GuruswamiSudan.Interpolation.Correctness
+import CompPoly.Bivariate.GuruswamiSudan.Interpolation.Dense.Correctness
+import CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness
+import CompPoly.Bivariate.GuruswamiSudan.Interpolation.ApproximantBasis.Correctness
+import CompPoly.Bivariate.GuruswamiSudan.Interpolation.Hybrid.Correctness
+
+/-!
+# Guruswami-Sudan Interpolation
+
+Public interpolation surface for certified Guruswami-Sudan interpolation
+backends.
+-/

CompPoly/Bivariate/GuruswamiSudan/Interpolation/ApproximantBasis.lean

@@ -0,0 +1,13 @@
+/-
+Copyright (c) 2026 CompPoly Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Valerii Huhnin
+-/
+
+import CompPoly.Bivariate.GuruswamiSudan.Interpolation.ApproximantBasis.Basic
+import CompPoly.Bivariate.GuruswamiSudan.Interpolation.ApproximantBasis.Algorithm
+import CompPoly.Bivariate.GuruswamiSudan.Interpolation.ApproximantBasis.Correctness
+
+/-!
+# Approximant-Basis Guruswami-Sudan Interpolation
+-/