Smooth Multiplicative-Subgroup Splitter Correctness

Correctness theorems for the smooth cyclic splitter, including executable contracts and adapter theorems.

theorem CompPoly.CPolynomial.Roots.FiniteField.finiteFieldRootProductWith_smoothSplitterInput {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : Raw.MulContext F) (D : Raw.ModContext F) (ctx : FiniteFieldContext F) (generator : F) (schedule : Array ℕ) {p : CPolynomial F} (hp : p ≠ 0) : smoothSplitterInput ctx.q generator schedule (finiteFieldRootProductWith M D ctx p)

Field-root products satisfy the generic smooth-splitter input predicate.

theorem CompPoly.CPolynomial.Roots.FiniteField.smoothLinearFactorProductSplitterWith_sound {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : Raw.MulContext F) (D : Raw.ModContext F) (ctx : SmoothCyclicRootContext F) {q : ℕ} {p factor : CPolynomial F} (h : factor ∈ ((smoothLinearFactorProductSplitterWith M D ctx).splitLinearFactors q p).toList) : IsLinearFactor factor

Soundness theorem for a smooth context adapted to the splitter interface.

theorem CompPoly.CPolynomial.Roots.FiniteField.smoothLinearFactorProductSplitterWith_complete {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : Raw.MulContext F) (D : Raw.ModContext F) (ctx : SmoothCyclicRootContext F) {q : ℕ} {p : CPolynomial F} {a : F} (hvalid : (smoothLinearFactorProductSplitterWith M D ctx).validInput q p) (hp : p ≠ 0) (hroot : eval a p = 0) : ∃ factor ∈ ((smoothLinearFactorProductSplitterWith M D ctx).splitLinearFactors q p).toList, IsLinearRootFactorCandidate factor a

Completeness theorem for a smooth context adapted to the splitter interface.

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

Zero-root extraction is sound for the emitted X factor.

theorem CompPoly.CPolynomial.Roots.FiniteField.smoothLeafLinearFactors_complete {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (E : BatchEvalContext F) {alpha gamma a : F} {order : ℕ} {p : CPolynomial F} (hcoset : ∃ k < order, a = alpha * gamma ^ k) (hroot : eval a p = 0) : ∃ factor ∈ (smoothLeafLinearFactors E alpha gamma order p).toList, IsLinearRootFactorCandidate factor a

Smooth leaf extraction is complete for roots in the enumerated coset.

theorem CompPoly.CPolynomial.Roots.FiniteField.smoothCosetLinearFactorsWithSchedule_sound {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : Raw.MulContext F) (D : Raw.ModContext F) (E : BatchEvalContext F) (schedule : List ℕ) (order : ℕ) (alpha gamma : F) (p factor : CPolynomial F) : factor ∈ (smoothCosetLinearFactorsWithSchedule M D E schedule order alpha gamma p).toList → IsLinearFactor factor

Schedule-driven smooth coset recursion emits only represented nonconstant linear factors.

theorem CompPoly.CPolynomial.Roots.FiniteField.smoothLinearFactorsAlgorithmWith_sound {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 factor : CPolynomial F} (h : factor ∈ (smoothLinearFactorsAlgorithmWith M D E q generator schedule p).toList) : IsLinearFactor factor

The top-level smooth splitter emits only represented nonconstant linear factors.

theorem CompPoly.CPolynomial.Roots.FiniteField.smooth_coset_split_root_partition_mod {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {alpha gamma : F} {order ell k : ℕ} (hgamma_pow : gamma ^ order = 1) (hell_dvd : ell ∣ order) : (alpha * gamma ^ k) ^ (order / ell) = alpha ^ (order / ell) * (gamma ^ (order / ell)) ^ (k % ell)

A smooth coset split maps the residue class k % ell to the child-coset equation.

theorem CompPoly.CPolynomial.Roots.FiniteField.smooth_coset_split_root_partition {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {alpha gamma x : F} {order ell : ℕ} (hgamma_order : orderOf gamma = order) (hell_dvd : ell ∣ order) (hell_pos : 0 < ell) (hx : ∃ k < order, x = alpha * gamma ^ k) : ∃ j < ell, x ^ (order / ell) = alpha ^ (order / ell) * (gamma ^ (order / ell)) ^ j

A smooth coset split partitions roots according to the child-coset equation.

theorem CompPoly.CPolynomial.Roots.FiniteField.exists_generator_pow_of_order_eq_card_sub_one {F : Type u_1} [Field F] [Finite F] [DecidableEq F] {q : ℕ} {generator a : F} (hcard : Nat.card F = q) (hgen : orderOf generator = q - 1) (ha : a ≠ 0) : ∃ k < q - 1, a = generator ^ k

A finite-field generator of order #F - 1 enumerates all nonzero elements.

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

Roots of p are contained in the explicit coset alpha * <gamma> of order order.

theorem CompPoly.CPolynomial.Roots.FiniteField.smooth_schedule_recursion_preserves_coset_invariant {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : Raw.MulContext F) (D : Raw.ModContext F) {order ell j : ℕ} {alpha gamma : F} {p : CPolynomial F} (hchild_alpha_ne_zero : alpha * gamma ^ j ≠ 0) (hchild_order_pos : 0 < order / ell) (hchild_generator_order : orderOf (gamma ^ ell) = order / ell) (hchild_roots : ∀ (x : F), eval x (p.gcdMonic (xPowModWith M D p (order / ell) - C (alpha ^ (order / ell) * (gamma ^ (order / ell)) ^ j))).monicNormalize = 0 → ∃ k < order / ell, x = alpha * gamma ^ j * (gamma ^ ell) ^ k) : SmoothCosetInvariant (alpha * gamma ^ j) (gamma ^ ell) (order / ell) (p.gcdMonic (xPowModWith M D p (order / ell) - C (alpha ^ (order / ell) * (gamma ^ (order / ell)) ^ j))).monicNormalize

Schedule recursion preserves the smooth coset invariant.

def CompPoly.CPolynomial.Roots.FiniteField.SmoothScheduleDivides : List ℕ → ℕ → Prop

Schedule factors divide the current coset order along executable smooth recursion.

@[instance_reducible]

instance CompPoly.CPolynomial.Roots.FiniteField.instDecidableSmoothScheduleDivides (schedule : List ℕ) (order : ℕ) : Decidable (SmoothScheduleDivides schedule order)

theorem CompPoly.CPolynomial.Roots.FiniteField.smooth_schedule_reaches_singleton {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (ctx : SmoothCyclicRootContext F) : List.foldl (fun (order ell : ℕ) => order / ell) (ctx.q - 1) ctx.schedule.toList = 1

The declared smooth schedule reaches singleton cosets.

theorem CompPoly.CPolynomial.Roots.FiniteField.smoothCosetLinearFactorsWithSchedule_complete {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (M : Raw.MulContext F) (D : Raw.ModContext F) (E : BatchEvalContext F) (schedule : List ℕ) (order : ℕ) (alpha gamma : F) (p : CPolynomial F) (a : F) : SmoothScheduleDivides schedule order → gamma ^ order = 1 → p ≠ 0 → eval a p = 0 → (∃ k < order, a = alpha * gamma ^ k) → ∃ factor ∈ (smoothCosetLinearFactorsWithSchedule M D E schedule order alpha gamma p).toList, IsLinearRootFactorCandidate factor a

Path completeness for the schedule-driven smooth coset recursion.

theorem CompPoly.CPolynomial.Roots.FiniteField.smoothLinearFactorsAlgorithmWith_complete {F : Type u_1} [Field F] [Finite F] [DecidableEq F] [BEq F] [LawfulBEq F] (M : Raw.MulContext F) (D : Raw.ModContext F) (E : BatchEvalContext F) (q : ℕ) (generator : F) (schedule : Array ℕ) (hcard : Nat.card F = q) (hgenerator : orderOf generator = q - 1) (hschedule : SmoothScheduleDivides schedule.toList (q - 1)) {p : CPolynomial F} {a : F} (hp : p ≠ 0) (hroot : eval a p = 0) : ∃ factor ∈ (smoothLinearFactorsAlgorithmWith M D E q generator schedule p).toList, IsLinearRootFactorCandidate factor a

Completeness of the top-level smooth linear-factor splitter.