Finite-Field Root Contexts

Explicit contexts for executable univariate root finding over finite fields. The algorithms use the cardinality carried here; downstream proofs use the finite-field and splitter contracts without unfolding concrete implementations.

structure CompPoly.CPolynomial.Roots.FiniteField.FiniteFieldContext (F : Type u_1) [Field F] : Type

Finite-field facts needed by executable root extraction.

• q : ℕ
• finite : Finite F
• card_eq : Nat.card F = self.q
• frobenius_fixed (a : F) : a ^ self.q = a

def CompPoly.CPolynomial.Roots.FiniteField.IsLinearFactor {F : Type u_1} [Field F] (factor : CPolynomial F) : Prop

A polynomial represented as a nonconstant linear factor.

def CompPoly.CPolynomial.Roots.FiniteField.IsLinearRootFactorCandidate {F : Type u_1} [Field F] (factor : CPolynomial F) (a : F) : Prop

A linear factor whose extracted root is a.

structure CompPoly.CPolynomial.Roots.FiniteField.LinearFactorProductSplitter (F : Type u_1) [Field F] [BEq F] [LawfulBEq F] : Type u_1

A deterministic splitter for squarefree products of linear factors.

The executable function consumes the field cardinality and the current factor. Completeness of the public root backend depends on splitter completeness for every linear-factor product reached by the recursion.

• splitLinearFactors : ℕ → CPolynomial F → Array (CPolynomial F)
• validInput : ℕ → CPolynomial F → Prop

  The precondition under which complete is claimed for the splitter input.

  Root backends should establish this predicate for the field-root product they pass to the splitter. Executable splitters may remain defensive outside this predicate, but completeness is only part of the contract under it.

• sound (q : ℕ) (p factor : CPolynomial F) : factor ∈ (self.splitLinearFactors q p).toList → IsLinearFactor factor
• complete (q : ℕ) (p : CPolynomial F) (a : F) : self.validInput q p → p ≠ 0 → eval a p = 0 → ∃ factor ∈ (self.splitLinearFactors q p).toList, IsLinearRootFactorCandidate factor a