Finite-Field Root Correctness

Theorem statements and certified context constructors for the executable finite-field root backend.

theorem CompPoly.CPolynomial.monicNormalize_root_iff {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {p : CPolynomial F} {a : F} (hp : p ≠ 0) : eval a p.monicNormalize = 0 ↔ eval a p = 0

Monic normalization preserves roots of nonzero polynomials.

theorem CompPoly.CPolynomial.monicNormalize_root_of_root {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {p : CPolynomial F} {a : F} (hp : eval a p = 0) : eval a p.monicNormalize = 0

Monic normalization preserves roots, including the zero polynomial case.

theorem CompPoly.CPolynomial.toPoly_monicNormalize_dvd_self {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (p : CPolynomial F) : p.monicNormalize.toPoly ∣ p.toPoly

The normalized polynomial divides the original polynomial.

theorem CompPoly.CPolynomial.gcdMonic_root_of_left_right {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {p q : CPolynomial F} {a : F} (hp : eval a p = 0) (hq : eval a q = 0) : eval a (p.gcdMonic q) = 0

The monic gcd contains every common root.

theorem CompPoly.CPolynomial.toPoly_gcdMonic_dvd_left {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (p q : CPolynomial F) : (p.gcdMonic q).toPoly ∣ p.toPoly

The monic gcd divides its left operand.

theorem CompPoly.CPolynomial.toPoly_gcdMonic_dvd_right {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (p q : CPolynomial F) : (p.gcdMonic q).toPoly ∣ q.toPoly

The monic gcd divides its right operand.

theorem CompPoly.CPolynomial.gcdMonic_root_iff_left_right {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {p q : CPolynomial F} {a : F} : eval a (p.gcdMonic q) = 0 ↔ eval a p = 0 ∧ eval a q = 0

The monic gcd vanishes exactly at common roots.

theorem CompPoly.CPolynomial.eval_div_eq_zero_of_dvd_of_root_of_ne_root {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {p q : CPolynomial F} {a : F} (hdiv : q.toPoly ∣ p.toPoly) (hp : eval a p = 0) (hq : eval a q ≠ 0) : eval a (p / q) = 0

A root of a dividend is a root of the exact quotient when the divisor does not vanish at that point.

theorem CompPoly.CPolynomial.monicNormalize_div_root_of_dvd_of_root_of_ne_root {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {p q : CPolynomial F} {a : F} (hdiv : q.toPoly ∣ p.toPoly) (hp : eval a p = 0) (hq : eval a q ≠ 0) : eval a (p / q).monicNormalize = 0

Monic normalization of an exact quotient preserves the quotient root from eval_div_eq_zero_of_dvd_of_root_of_ne_root.

theorem CompPoly.CPolynomial.normXgcd_root_of_left_right {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {p q : CPolynomial F} {a : F} (hp : eval a p = 0) (hq : eval a q = 0) : eval a (p.normXgcd q).1 = 0

The normalized extended gcd contains every common root.

theorem CompPoly.CPolynomial.eval_gcdMonic_eq_zero_iff_normXgcd_fst_eq_zero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (a : F) (p q : CPolynomial F) : eval a (p.gcdMonic q) = 0 ↔ eval a (p.normXgcd q).1 = 0

The specialized monic gcd and normalized extended gcd have the same root predicate.

theorem CompPoly.CPolynomial.normXgcd_fst_root_of_left_right {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {a : F} {p q : CPolynomial F} (hp : eval a p = 0) (hq : eval a q = 0) : eval a (p.normXgcd q).1 = 0

The normalized extended-gcd first component contains every common root.

theorem CompPoly.CPolynomial.linearRootOfFactor?_sound {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {factor : CPolynomial F} {a : F} (h : factor.linearRootOfFactor? = some a) : eval a factor = 0

Roots extracted from a linear factor satisfy that factor.

theorem CompPoly.CPolynomial.mem_validateRootCandidates_eval_eq_zero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {p : CPolynomial F} {candidates : Array F} {a : F} (h : a ∈ (p.validateRootCandidates candidates).toList) : eval a p = 0

Validation makes returned candidates sound for the original polynomial.

theorem CompPoly.CPolynomial.Roots.FiniteField.raw_eval_powModWith_eq_pow {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : Raw.MulContext F) (D : Raw.ModContext F) {modulus base : Raw F} {a : F} (hmod : Raw.eval a modulus = 0) (q : ℕ) : Raw.eval a (Raw.powModWith M D modulus base q) = Raw.eval a base ^ q

Raw modular exponentiation evaluates as ordinary exponentiation at roots of the modulus.

theorem CompPoly.CPolynomial.Roots.FiniteField.finiteFieldRootProductWith_complete {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : Raw.MulContext F) (D : Raw.ModContext F) (ctx : FiniteFieldContext F) {p : CPolynomial F} {a : F} (hp : p ≠ 0) (hroot : eval a p = 0) : eval a (finiteFieldRootProductWith M D ctx p) = 0

Every root of p is a root of the finite-field root product.

theorem CompPoly.CPolynomial.Roots.FiniteField.finiteFieldRootProduct_complete {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (ctx : FiniteFieldContext F) {p : CPolynomial F} {a : F} (hp : p ≠ 0) (hroot : eval a p = 0) : eval a (finiteFieldRootProduct ctx p) = 0

Every root of p is a root of the finite-field root product.

theorem CompPoly.CPolynomial.Roots.FiniteField.finiteFieldRootProduct_validated_sound {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (_ctx : FiniteFieldContext F) {p : CPolynomial F} {candidates : Array F} {a : F} (h : a ∈ (p.validateRootCandidates candidates).toList) : eval a p = 0

Every validated root extracted from the root product is a root of p.

theorem CompPoly.CPolynomial.Roots.FiniteField.rootsInFiniteFieldWith_sound {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : Raw.MulContext F) (D : Raw.ModContext F) (ctx : FiniteFieldContext F) (splitter : LinearFactorProductSplitter F) {p : CPolynomial F} {a : F} (h : a ∈ (rootsInFiniteFieldWith M D ctx splitter p).toList) : eval a p = 0

Returned finite-field roots are roots of the original polynomial.

theorem CompPoly.CPolynomial.Roots.FiniteField.rootsInFiniteField_sound {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (ctx : FiniteFieldContext F) (splitter : LinearFactorProductSplitter F) {p : CPolynomial F} {a : F} (h : a ∈ (rootsInFiniteField ctx splitter p).toList) : eval a p = 0

Returned finite-field roots are roots of the original polynomial.

theorem CompPoly.CPolynomial.Roots.FiniteField.linearFactor_isLinearFactor {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (a : F) : IsLinearFactor (linearFactor a)

Every explicit X - a factor is represented as a nonconstant linear factor.

theorem CompPoly.CPolynomial.Roots.FiniteField.linearFactor_isRepresentedLinearFactor {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (a : F) : isRepresentedLinearFactor (linearFactor a) = true

The represented-linear recognizer accepts every explicit X - a factor.

theorem CompPoly.CPolynomial.Roots.FiniteField.linearFactor_isRootFactorCandidate {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (a : F) : IsLinearRootFactorCandidate (linearFactor a) a

The explicit X - a factor represents the root a.

theorem CompPoly.CPolynomial.Roots.FiniteField.representedLinearFactor_candidate_of_root {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {p : CPolynomial F} {a : F} (hlin : isRepresentedLinearFactor p = true) (hroot : eval a p = 0) : IsLinearRootFactorCandidate p a

If the represented-linear recognizer accepts p, then any root of p is its root candidate.

theorem CompPoly.CPolynomial.Roots.FiniteField.eval_xPowModWith_eq_pow {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : Raw.MulContext F) (D : Raw.ModContext F) {p : CPolynomial F} {a : F} (hroot : eval a p = 0) (n : ℕ) : eval a (xPowModWith M D p n) = a ^ n

Evaluation of a modular X^n at a root of the modulus agrees with a^n.

theorem CompPoly.CPolynomial.Roots.FiniteField.rootsInFiniteFieldWith_complete {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : Raw.MulContext F) (D : Raw.ModContext F) (ctx : FiniteFieldContext F) (splitter : LinearFactorProductSplitter F) (splitterValid : ∀ {p : CPolynomial F}, p ≠ 0 → splitter.validInput ctx.q (finiteFieldRootProductWith M D ctx p)) {p : CPolynomial F} {a : F} (hp : p ≠ 0) (hroot : eval a p = 0) : a ∈ (rootsInFiniteFieldWith M D ctx splitter p).toList

Every root of a nonzero polynomial is returned by the finite-field backend.

theorem CompPoly.CPolynomial.Roots.FiniteField.rootsInFiniteField_complete {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (ctx : FiniteFieldContext F) (splitter : LinearFactorProductSplitter F) (splitterValid : ∀ {p : CPolynomial F}, p ≠ 0 → splitter.validInput ctx.q (finiteFieldRootProduct ctx p)) {p : CPolynomial F} {a : F} (hp : p ≠ 0) (hroot : eval a p = 0) : a ∈ (rootsInFiniteField ctx splitter p).toList

Every root of a nonzero polynomial is returned by the finite-field backend.

theorem CompPoly.CPolynomial.Roots.FiniteField.rootsInFiniteField_spec {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (ctx : FiniteFieldContext F) (splitter : LinearFactorProductSplitter F) (splitterValid : ∀ {p : CPolynomial F}, p ≠ 0 → splitter.validInput ctx.q (finiteFieldRootProduct ctx p)) {p : CPolynomial F} {a : F} (hp : p ≠ 0) : a ∈ (rootsInFiniteField ctx splitter p).toList ↔ eval a p = 0

The complete executable finite-field root pipeline is sound and complete for nonzero inputs under the finite-field and splitter contracts.