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.

structure CompPoly.GuruswamiSudan.GSInterpParams : Type

Parameters for the CompPoly interpolation step.

• messageDegree : ℕ
• multiplicity : ℕ
• weightedDegreeBound : ℕ

@[instance_reducible]

instance CompPoly.GuruswamiSudan.instReprGSInterpParams : Repr GSInterpParams

def CompPoly.GuruswamiSudan.instReprGSInterpParams.repr : GSInterpParams → ℕ → Std.Format

def CompPoly.GuruswamiSudan.instBEqGSInterpParams.beq : GSInterpParams → GSInterpParams → Bool

@[instance_reducible]

instance CompPoly.GuruswamiSudan.instBEqGSInterpParams : BEq GSInterpParams

def CompPoly.GuruswamiSudan.instDecidableEqGSInterpParams.decEq (x✝ x✝¹ : GSInterpParams) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance CompPoly.GuruswamiSudan.instDecidableEqGSInterpParams : DecidableEq GSInterpParams

def CompPoly.GuruswamiSudan.yWeight (params : GSInterpParams) : ℕ

The GS weighted degree uses weights (1, messageDegree - 1).

def CompPoly.GuruswamiSudan.degreeLt {F : Type u_1} [Zero F] (p : CPolynomial F) (k : ℕ) : Prop

p.degree < k, treating the zero polynomial as degree bot.

def CompPoly.GuruswamiSudan.DistinctXCoordinates {F : Type u_1} (points : Array (F × F)) : Prop

Packed input points have no duplicate x-coordinates.

def CompPoly.GuruswamiSudan.ValidInterpolationWitness {F : Type u_1} [CommSemiring F] [BEq F] [LawfulBEq F] [Nontrivial F] [DecidableEq F] (points : Array (F × F)) (params : GSInterpParams) (Q : CBivariate F) : Prop

Semantic interpolation witness used by backend contracts and core completeness statements.

structure CompPoly.GuruswamiSudan.LinearKernelContext (F : Type u_1) [Field F] [BEq F] [LawfulBEq F] : Type u_1

A dense homogeneous linear-kernel backend.

The operation returns a nonzero kernel witness in the backend's chosen normalization when it can find one. Completeness is stated in the negative form needed by dense interpolation systems: if no witness is returned, no nonzero homogeneous solution exists.

• homogeneousWitness : DenseMatrix F → Option (Array F)
• witness_width {M : DenseMatrix F} {v : Array F} : self.homogeneousWitness M = some v → M.VectorWidth v
• witness_sound {M : DenseMatrix F} {v : Array F} : M.WellFormed → self.homogeneousWitness M = some v → M.IsHomogeneousSolution v
• witness_nonzero {M : DenseMatrix F} {v : Array F} : self.homogeneousWitness M = some v → DenseMatrix.NonzeroVector v
• witness_complete {M : DenseMatrix F} : M.WellFormed → self.homogeneousWitness M = none → ∀ (v : Array F), M.VectorWidth v → M.IsHomogeneousSolution v → ¬DenseMatrix.NonzeroVector v

def CompPoly.GuruswamiSudan.denseLinearKernelContext (F : Type u_1) [Field F] [BEq F] [LawfulBEq F] : LinearKernelContext F

The dense Gaussian-elimination homogeneous-kernel backend.

The executable witness is computed by the in-place reduction DenseMatrix.homogeneousWitnessInPlace, which mutates the matrix array instead of copying it on every row operation. It returns the same witness as the copying DenseMatrix.homogeneousWitness (DenseMatrix.homogeneousWitnessInPlace_eq), so the backend contract is discharged by the copying-kernel correctness lemmas.

structure CompPoly.GuruswamiSudan.GSInterpContext (F : Type u_1) [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] : Type u_1

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.

• interpolate : Array (F × F) → GSInterpParams → Option (CBivariate F)
• sound (points : Array (F × F)) (params : GSInterpParams) (Q : CBivariate F) : self.interpolate points params = some Q → ValidInterpolationWitness points params Q
• complete (points : Array (F × F)) (params : GSInterpParams) : DistinctXCoordinates points → (∃ (Q : CBivariate F), ValidInterpolationWitness points params Q) → ∃ (Q : CBivariate F), self.interpolate points params = some Q

structure CompPoly.GuruswamiSudan.FieldRootContext (F : Type u_1) [Field F] [BEq F] [LawfulBEq F] : Type u_1

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.

• rootsInField : CPolynomial F → Array F
• sound (p : CPolynomial F) (a : F) : a ∈ (self.rootsInField p).toList → CPolynomial.eval a p = 0
• complete (p : CPolynomial F) (a : F) : p ≠ 0 → CPolynomial.eval a p = 0 → a ∈ (self.rootsInField p).toList

structure CompPoly.GuruswamiSudan.GSRootContext (F : Type u_1) [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] : Type u_1

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.

• rootsYDegreeLt : CBivariate F → ℕ → Array (CPolynomial F)
• sound (Q : CBivariate F) (k : ℕ) (p : CPolynomial F) : p ∈ (self.rootsYDegreeLt Q k).toList → degreeLt p k ∧ Q.composeY p = 0
• complete (Q : CBivariate F) (k : ℕ) (p : CPolynomial F) : Q ≠ 0 → degreeLt p k → Q.composeY p = 0 → p ∈ (self.rootsYDegreeLt Q k).toList