Alekhnovich Root Search Correctness

Public correctness surface for the Alekhnovich bounded bivariate root backend [Ale05].

References

• [M. Alekhnovich, Linear Diophantine Equations Over Polynomials and Soft Decoding of Reed-Solomon Codes, IEEE Transactions on Information Theory 51(7), 2257-2265, 2005][Ale05]

theorem CompPoly.GuruswamiSudan.alekhnovichRootsYDegreeLt_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 ∈ (alekhnovichRootsYDegreeLt fieldRoots Q k).toList) : degreeLt p k ∧ Q.composeY p = 0

Soundness of Alekhnovich root filtering.

theorem CompPoly.GuruswamiSudan.alekhnovichRootsYDegreeLt_complete_of_candidate_mem {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) (hmem : p ∈ (alekhnovichRootCandidates fieldRoots Q k).toList) (hdegree : degreeLt p k) (hroot : Q.composeY p = 0) : p ∈ (alekhnovichRootsYDegreeLt fieldRoots Q k).toList

The exact final filter keeps any true bounded root that the Alekhnovich candidate generator has already produced.

theorem CompPoly.GuruswamiSudan.RootMod.substituteYPolynomialPlusXPowerY {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {Q : CBivariate F} {f g : CPolynomial F} {t N : ℕ} (hroot : RootMod Q (f + shiftPolynomialByXPower g t) N) : RootMod (GuruswamiSudan.substituteYPolynomialPlusXPowerY Q f t) g N

Shifted substitution preserves modular roots below N before truncation.

theorem CompPoly.GuruswamiSudan.RootMod.substituteYPolynomialPlusXPowerYTruncated {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {Q : CBivariate F} {f g : CPolynomial F} {t N : ℕ} (hroot : RootMod Q (f + shiftPolynomialByXPower g t) N) : RootMod (GuruswamiSudan.substituteYPolynomialPlusXPowerYTruncated Q f t N) g N

Truncated shifted substitution has the same coefficients below N as exact shifted substitution, so it preserves modular roots below N.

theorem CompPoly.GuruswamiSudan.RootMod.stripXAdicFactor {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {Q : CBivariate F} {p : CPolynomial F} {s N : ℕ} (horder : Q.xAdicOrder? = some s) (hroot : RootMod Q p (s + N)) : RootMod Q.stripXAdicFactor p N

Stripping a visible X-adic valuation transports a modular root of Q to a shorter modular root of the stripped residual.

theorem CompPoly.GuruswamiSudan.alekhnovichRootPrefixesWithFuel_complete {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {fieldRoots : FieldRootContext F} {Q : CBivariate F} {N fuel : ℕ} {p : CPolynomial F} (hfuel : N < fuel) (hroot : RootMod Q p N) : ∃ rootPrefix ∈ (alekhnovichRootPrefixesWithFuel fieldRoots fuel Q N).toList, MatchesRootPrefix p rootPrefix

Recursive Alekhnovich prefix coverage for modular roots.

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

Candidate generation coverage for the Alekhnovich-only recursive suffix completion.

theorem CompPoly.GuruswamiSudan.composeY_eq_zero_of_rootMod_of_substitutionDegreeBound {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {Q : CBivariate F} {p : CPolynomial F} {k N : ℕ} (hbound : SubstitutionDegreeBound Q k N) (hdegree : degreeLt p k) (hroot : RootMod Q p N) : Q.composeY p = 0

The finite modular-root predicate is exact once the substitution degree is bounded below the checked precision.

theorem CompPoly.GuruswamiSudan.alekhnovichRootCandidates_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 ∈ (alekhnovichRootCandidates fieldRoots Q k).toList

Completeness of Alekhnovich candidate generation for exact bounded roots.

theorem CompPoly.GuruswamiSudan.alekhnovichRootsYDegreeLt_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 ∈ (alekhnovichRootsYDegreeLt fieldRoots Q k).toList

Completeness of Alekhnovich bounded-degree root finding from a complete field-root backend.

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

Alekhnovich roots packaged with an explicit univariate field-root backend.