Roth-Ruckenstein Root Correctness

Correctness statements for the Roth-Ruckenstein root backend.

theorem CompPoly.GuruswamiSudan.rothRuckensteinRootsYDegreeLt_sound {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {fieldRoots : FieldRootContext F} {Q : CBivariate F} {k : ℕ} {p : CPolynomial F} (h : p ∈ (rothRuckensteinRootsYDegreeLt fieldRoots Q k).toList) : degreeLt p k ∧ Q.composeY p = 0

Soundness of Roth-Ruckenstein root filtering.

theorem CompPoly.GuruswamiSudan.initialCoefficientPolynomial_stripXAdicFactor_ne_zero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {Q : CBivariate F} (hQ : Q ≠ 0) : initialCoefficientPolynomial Q.stripXAdicFactor ≠ 0

Normalizing a nonzero bivariate polynomial exposes a nonzero initial coefficient equation for the residual-transform RR step.

theorem CompPoly.GuruswamiSudan.rothRuckensteinRootsYDegreeLt_complete {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {fieldRoots : FieldRootContext F} {Q : CBivariate F} {k : ℕ} {p : CPolynomial F} (hQ : Q ≠ 0) (hdegree : degreeLt p k) (hroot : Q.composeY p = 0) : p ∈ (rothRuckensteinRootsYDegreeLt fieldRoots Q k).toList

Completeness of Roth-Ruckenstein root finding from a complete field-root backend.

The nonzero-input hypothesis matches the backend completeness contract, which only promises finite output for nonzero bivariate equations.

def CompPoly.GuruswamiSudan.rothRuckensteinRootContext (F : Type u_1) [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (fieldRoots : FieldRootContext F) : GSRootContext F

Roth-Ruckenstein roots packaged with an explicit univariate field-root backend.

def CompPoly.GuruswamiSudan.transformedRothRuckensteinRootContext (F : Type u_1) [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (fieldRoots : FieldRootContext F) : GSRootContext F

Residual-transform Roth-Ruckenstein roots packaged as a backend.