chore: merge Lean 4.30 version bump into gs-bivariate-rr

CompPoly.lean

@@ -3,6 +3,25 @@ import CompPoly.Bivariate.CMvEquiv
 import CompPoly.Bivariate.Deriv
 import CompPoly.Bivariate.Factor
 import CompPoly.Bivariate.FactorMonic
+import CompPoly.Bivariate.GuruswamiSudan.Compose
+import CompPoly.Bivariate.GuruswamiSudan.Context
+import CompPoly.Bivariate.GuruswamiSudan.Hasse
+import CompPoly.Bivariate.GuruswamiSudan.Monomials
+import CompPoly.Bivariate.GuruswamiSudan.Polynomial
+import CompPoly.Bivariate.GuruswamiSudan.PolynomialCorrectness
+import CompPoly.Bivariate.GuruswamiSudan.Root
+import CompPoly.Bivariate.GuruswamiSudan.Root.Basic
+import CompPoly.Bivariate.GuruswamiSudan.Root.Common
+import CompPoly.Bivariate.GuruswamiSudan.Root.Common.Lemmas
+import CompPoly.Bivariate.GuruswamiSudan.Root.FieldRoots
+import CompPoly.Bivariate.GuruswamiSudan.Root.FieldRoots.FiniteField
+import CompPoly.Bivariate.GuruswamiSudan.Root.FieldRoots.KoalaBear
+import CompPoly.Bivariate.GuruswamiSudan.Root.RothRuckenstein.Algorithm
+import CompPoly.Bivariate.GuruswamiSudan.Root.RothRuckenstein.Correctness
+import CompPoly.Bivariate.GuruswamiSudan.Root.RothRuckenstein.Lemmas
+import CompPoly.Bivariate.GuruswamiSudan.Root.ShiftedSubstitution
+import CompPoly.Bivariate.GuruswamiSudan.Root.ShiftedSubstitution.Lemmas
+import CompPoly.Bivariate.GuruswamiSudan.Util
 import CompPoly.Bivariate.ToPoly
 import CompPoly.Data.Array.Lemmas
 import CompPoly.Data.Classes.DCast
@@ -99,6 +118,7 @@ import CompPoly.Univariate.BatchEval.Correctness
 import CompPoly.Univariate.BatchEval.Naive
 import CompPoly.Univariate.BatchEval.SubproductTree
 import CompPoly.Univariate.CMvEquiv
+import CompPoly.Univariate.Context
 import CompPoly.Univariate.Deriv
 import CompPoly.Univariate.DivisionCorrectness
 import CompPoly.Univariate.EuclideanAlgorithm
@@ -107,6 +127,7 @@ import CompPoly.Univariate.Linear
 import CompPoly.Univariate.ManyEval
 import CompPoly.Univariate.ManyEval.Basic
 import CompPoly.Univariate.ManyEval.Correctness
+import CompPoly.Univariate.Modular
 import CompPoly.Univariate.NTT.BabyBear
 import CompPoly.Univariate.NTT.Domain
 import CompPoly.Univariate.NTT.Evaluation
@@ -133,10 +154,23 @@ import CompPoly.Univariate.NTTFast.Plan
 import CompPoly.Univariate.Quotient.Core
 import CompPoly.Univariate.Quotient.Equiv
 import CompPoly.Univariate.Raw
+import CompPoly.Univariate.Raw.Context
 import CompPoly.Univariate.Raw.Core
 import CompPoly.Univariate.Raw.Division
+import CompPoly.Univariate.Raw.Modular
 import CompPoly.Univariate.Raw.Ops
 import CompPoly.Univariate.Raw.Proofs
+import CompPoly.Univariate.Roots
+import CompPoly.Univariate.Roots.Backend
+import CompPoly.Univariate.Roots.Context
+import CompPoly.Univariate.Roots.Correctness
+import CompPoly.Univariate.Roots.Enumeration
+import CompPoly.Univariate.Roots.Extraction
+import CompPoly.Univariate.Roots.RootProduct
+import CompPoly.Univariate.Roots.SmoothSubgroup
+import CompPoly.Univariate.Roots.SmoothSubgroup.Basic
+import CompPoly.Univariate.Roots.SmoothSubgroup.Correctness
+import CompPoly.Univariate.Roots.Splitter
 import CompPoly.Univariate.ToPoly
 import CompPoly.Univariate.ToPoly.Core
 import CompPoly.Univariate.ToPoly.Degree

CompPoly/Bivariate/GuruswamiSudan/Compose.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.Hasse
+
+/-!
+# Guruswami-Sudan Bivariate Composition
+
+Re-exports `CBivariate.composeY` and related coefficient/truncated evaluators.
+-/

CompPoly/Bivariate/GuruswamiSudan/Context.lean

@@ -0,0 +1,110 @@
+/-
+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.Deriv
+import CompPoly.Bivariate.GuruswamiSudan.Compose
+
+/-!
+# Guruswami-Sudan Backend Contexts
+
+Explicit executable contexts for the CompPoly Guruswami-Sudan core. The
+contexts package replaceable operations together with the contracts used by the
+public correctness theorems.
+-/
+
+namespace CompPoly
+
+namespace GuruswamiSudan
+
+/-- Parameters for the CompPoly interpolation step. -/
+structure GSInterpParams where
+  messageDegree : Nat
+  multiplicity : Nat
+  weightedDegreeBound : Nat
+deriving Repr, BEq, DecidableEq
+
+/-- The GS weighted degree uses weights `(1, messageDegree - 1)`. -/
+def yWeight (params : GSInterpParams) : Nat :=
+  params.messageDegree - 1
+
+/-- `p.degree < k`, treating the zero polynomial as degree `bot`. -/
+def degreeLt {F : Type*} [Zero F] (p : CPolynomial F) (k : Nat) : Prop :=
+  p.degree < (k : WithBot Nat)
+
+/-- Packed input points have no duplicate `x`-coordinates. -/
+def DistinctXCoordinates {F : Type*} (points : Array (Prod F F)) : Prop :=
+  (points.toList.map fun point ↦ point.1).Nodup
+
+/-- Semantic interpolation witness used by backend contracts and core
+completeness statements. -/
+def ValidInterpolationWitness {F : Type*}
+    [CommSemiring F] [BEq F] [LawfulBEq F] [Nontrivial F] [DecidableEq F]
+    (points : Array (Prod F F)) (params : GSInterpParams) (Q : CBivariate F) : Prop :=
+  Q ≠ 0 ∧
+    CBivariate.natWeightedDegree Q 1 (yWeight params) ≤ params.weightedDegreeBound ∧
+      ∀ point, point ∈ points.toList →
+        CBivariate.hasMultiplicity Q params.multiplicity point.1 point.2
+
+/-- Guruswami-Sudan-facing interpolation backend.
+
+The backend packages the executable interpolation operation together with the
+contract fields used by callers, using the explicit context style used by
+univariate multiplication and remainder backends.
+-/
+structure GSInterpContext (F : Type*) [Field F] [BEq F] [LawfulBEq F]
+    [DecidableEq F] where
+  interpolate : Array (Prod F F) → GSInterpParams → Option (CBivariate F)
+  sound :
+    ∀ points params Q,
+      interpolate points params = some Q →
+        ValidInterpolationWitness points params Q
+  complete :
+    ∀ points params,
+      DistinctXCoordinates points →
+      (exists Q, ValidInterpolationWitness points params Q) →
+        exists Q, interpolate points params = some Q
+
+/-- Executable root finder for univariate field polynomials.
+
+Completeness is only required for nonzero polynomials. A zero univariate
+polynomial vanishes on every field element, so an unconditional array-valued
+complete root finder would have to enumerate the whole field.
+-/
+structure FieldRootContext (F : Type*) [Field F] [BEq F] [LawfulBEq F] where
+  rootsInField : CPolynomial F → Array F
+  sound :
+    ∀ p a,
+      a ∈ (rootsInField p).toList →
+        CPolynomial.eval a p = 0
+  complete :
+    ∀ p a,
+      p ≠ 0 →
+      CPolynomial.eval a p = 0 →
+        a ∈ (rootsInField p).toList
+
+/-- Guruswami-Sudan-facing bounded-degree root backend.
+
+Completeness is only required for nonzero bivariate input. The zero bivariate
+polynomial has every degree-bounded univariate polynomial as a root, which is not
+a finite output contract for large fields.
+-/
+structure GSRootContext (F : Type*) [Field F] [BEq F] [LawfulBEq F]
+    [DecidableEq F] where
+  rootsYDegreeLt : CBivariate F → Nat → Array (CPolynomial F)
+  sound :
+    ∀ Q k p,
+      p ∈ (rootsYDegreeLt Q k).toList →
+        degreeLt p k ∧ CBivariate.composeY Q p = 0
+  complete :
+    ∀ Q k p,
+      Q ≠ 0 →
+      degreeLt p k →
+      CBivariate.composeY Q p = 0 →
+        p ∈ (rootsYDegreeLt Q k).toList
+
+end GuruswamiSudan
+
+end CompPoly

CompPoly/Bivariate/GuruswamiSudan/Hasse.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.Monomials
+
+/-!
+# Guruswami-Sudan Hasse Derivatives
+
+Re-exports executable Hasse derivatives and multiplicity checks on `CBivariate`.
+-/

CompPoly/Bivariate/GuruswamiSudan/Monomials.lean

@@ -0,0 +1,14 @@
+/-
+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.Polynomial
+
+/-!
+# Guruswami-Sudan Bivariate Monomials
+
+Re-exports dense coefficient-grid and weighted-monomial helpers used by the
+Guruswami-Sudan interpolation matrix.
+-/