Exhaustive Finite-Field Root Enumeration

Reusable lazy field-enumeration contexts for finite-field root search. The context stores an indexing function rather than an array of all elements; array inputs are adapted through fieldEnumerationOfArray for tests and small callers.

structure CompPoly.CPolynomial.Roots.FiniteField.FieldEnumeration (F : Type u_1) : Type u_1

A lazy complete enumeration of a finite field.

• size : ℕ
• elem : Fin self.size → F
• complete (a : F) : ∃ (i : Fin self.size), self.elem i = a

def CompPoly.CPolynomial.Roots.FiniteField.ContainsAllFieldElements {F : Type u_1} (elements : Array F) : Prop

An array contains every field element. Duplicate entries are allowed.

def CompPoly.CPolynomial.Roots.FiniteField.fieldEnumerationOfArray {F : Type u_1} (elements : Array F) (hElements : ContainsAllFieldElements elements) : FieldEnumeration F

Adapt an explicit element array to a lazy enumeration context.

def CompPoly.CPolynomial.Roots.FiniteField.rootsInFieldByEnumeration {F : Type u_1} [Semiring F] [BEq F] (enumeration : FieldEnumeration F) (p : CPolynomial F) : Array F

Roots by exhaustive evaluation over a lazy field enumeration.

theorem CompPoly.CPolynomial.Roots.FiniteField.rootsInFieldByEnumeration_sound {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {enumeration : FieldEnumeration F} {p : CPolynomial F} {a : F} (h : a ∈ (rootsInFieldByEnumeration enumeration p).toList) : eval a p = 0

Exhaustive enumeration only returns actual roots.

theorem CompPoly.CPolynomial.Roots.FiniteField.rootsInFieldByEnumeration_complete {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (enumeration : FieldEnumeration F) {p : CPolynomial F} {a : F} (hroot : eval a p = 0) : a ∈ (rootsInFieldByEnumeration enumeration p).toList

Complete enumeration finds every root.

def CompPoly.CPolynomial.Roots.FiniteField.enumeratedLinearFactors {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (enumeration : FieldEnumeration F) (p : CPolynomial F) : Array (CPolynomial F)

Linear factors for every enumerated root of p.

theorem CompPoly.CPolynomial.Roots.FiniteField.enumeratedLinearFactors_sound {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {enumeration : FieldEnumeration F} {p factor : CPolynomial F} (h : factor ∈ (enumeratedLinearFactors enumeration p).toList) : IsLinearFactor factor

Every factor emitted by exhaustive enumeration is represented linear.

theorem CompPoly.CPolynomial.Roots.FiniteField.enumeratedLinearFactors_complete {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (enumeration : FieldEnumeration F) {p : CPolynomial F} {a : F} (hroot : eval a p = 0) : ∃ factor ∈ (enumeratedLinearFactors enumeration p).toList, IsLinearRootFactorCandidate factor a

Exhaustive enumeration emits the linear factor for every root.

def CompPoly.CPolynomial.Roots.FiniteField.enumeratingLinearFactorProductSplitter {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (enumeration : FieldEnumeration F) : LinearFactorProductSplitter F

Exhaustive enumeration packaged as a linear-factor product splitter.