Smooth Multiplicative-Subgroup Linear-Factor Splitting

Executable splitter for field-root products over finite fields whose multiplicative group admits a smooth cyclic refinement schedule, following the subgroup-refinement root-finding method of [MOV92].

The generic root pipeline consumes a LinearFactorProductSplitter. This module provides a contract-bearing smooth context plus an adapter from that context to the shared splitter interface.

References

• [Menezes, A. J., van Oorschot, P. C., and Vanstone, S. A., Subgroup Refinement Algorithms for Root Finding in GF(q)][MOV92]

def CompPoly.CPolynomial.Roots.FiniteField.smoothSplitterInput {F : Type u_1} [Field F] (q : ℕ) (_generator : F) (_schedule : Array ℕ) (p : CPolynomial F) : Prop

Splitter-input predicate for a smooth cyclic splitter.

This predicate records the mathematical input contract for the splitter. The field-root pipeline proves it for gcd(p, X^q - X) values before using the splitter completeness theorem.

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

Package the executable smooth splitter with its field and schedule facts.

• q : ℕ
• generator : F
• schedule : Array ℕ
• leafEvaluator : BatchEvalContext F
• validInput : CPolynomial F → Prop
• card_eq : Nat.card F = self.q
• generator_order : orderOf self.generator = self.q - 1
• schedule_complete : List.foldl (fun (order ell : ℕ) => order / ell) (self.q - 1) self.schedule.toList = 1
• splitLinearFactorsWith : Raw.MulContext F → Raw.ModContext F → CPolynomial F → Array (CPolynomial F)
• sound (M : Raw.MulContext F) (D : Raw.ModContext F) (p factor : CPolynomial F) : factor ∈ (self.splitLinearFactorsWith M D p).toList → IsLinearFactor factor
• complete (M : Raw.MulContext F) (D : Raw.ModContext F) (p : CPolynomial F) (a : F) : self.validInput p → p ≠ 0 → eval a p = 0 → ∃ factor ∈ (self.splitLinearFactorsWith M D p).toList, IsLinearRootFactorCandidate factor a

def CompPoly.CPolynomial.Roots.FiniteField.smoothCosetPoints {F : Type u_1} [Field F] (alpha gamma : F) (order : ℕ) : Array F

Ordered elements of the coset alpha * <gamma> with the supplied order.

def CompPoly.CPolynomial.Roots.FiniteField.linearFactorsFromLeafValues {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (points values : Array F) : Array (CPolynomial F)

Emit linear factors for the points whose evaluated value is zero.

def CompPoly.CPolynomial.Roots.FiniteField.smoothLeafLinearFactors {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (E : BatchEvalContext F) (alpha gamma : F) (order : ℕ) (p : CPolynomial F) : Array (CPolynomial F)

Leaf extraction by evaluating all elements of the current coset.

def CompPoly.CPolynomial.Roots.FiniteField.smoothCosetLinearFactorsWithSchedule {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : Raw.MulContext F) (D : Raw.ModContext F) (E : BatchEvalContext F) : List ℕ → ℕ → F → F → CPolynomial F → Array (CPolynomial F)

Schedule-driven nonzero-root refinement inside one multiplicative coset.

def CompPoly.CPolynomial.Roots.FiniteField.smoothNonzeroLinearFactorsWith {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : Raw.MulContext F) (D : Raw.ModContext F) (E : BatchEvalContext F) (q : ℕ) (generator : F) (schedule : Array ℕ) (p : CPolynomial F) : Array (CPolynomial F)

Nonzero root extraction by smooth multiplicative-subgroup refinement.

def CompPoly.CPolynomial.Roots.FiniteField.smoothLinearFactorsAlgorithmWith {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : Raw.MulContext F) (D : Raw.ModContext F) (E : BatchEvalContext F) (q : ℕ) (generator : F) (schedule : Array ℕ) (p : CPolynomial F) : Array (CPolynomial F)

Smooth linear-factor splitting algorithm, including separate handling of root 0.

def CompPoly.CPolynomial.Roots.FiniteField.smoothCyclicRootContextOf {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (q : ℕ) (generator : F) (schedule : Array ℕ) (leafEvaluator : BatchEvalContext F) (validInput : CPolynomial F → Prop) (card_eq : Nat.card F = q) (generator_order : orderOf generator = q - 1) (schedule_complete : List.foldl (fun (order ell : ℕ) => order / ell) (q - 1) schedule.toList = 1) (sound : ∀ (M : Raw.MulContext F) (D : Raw.ModContext F) (p factor : CPolynomial F), factor ∈ (smoothLinearFactorsAlgorithmWith M D leafEvaluator q generator schedule p).toList → IsLinearFactor factor) (complete : ∀ (M : Raw.MulContext F) (D : Raw.ModContext F) (p : CPolynomial F) (a : F), validInput p → p ≠ 0 → eval a p = 0 → ∃ factor ∈ (smoothLinearFactorsAlgorithmWith M D leafEvaluator q generator schedule p).toList, IsLinearRootFactorCandidate factor a) : SmoothCyclicRootContext F

Build a smooth cyclic root context from executable constants and proof fields.

def CompPoly.CPolynomial.Roots.FiniteField.smoothLinearFactorProductSplitterWith {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : Raw.MulContext F) (D : Raw.ModContext F) (ctx : SmoothCyclicRootContext F) : LinearFactorProductSplitter F

Adapt a smooth cyclic context to the generic splitter interface.