feat(univariate): Shoup's trace splitter root search

CompPoly.lean

@@ -80,6 +80,47 @@ import CompPoly.Fields.Binary.BF128Ghash.Prelude
 import CompPoly.Fields.Binary.BF128Ghash.XPowTwoPowGcdCertificate
 import CompPoly.Fields.Binary.BF128Ghash.XPowTwoPowModCertificate
 import CompPoly.Fields.Binary.Common
+import CompPoly.Fields.Binary.Extension.Basic
+import CompPoly.Fields.Binary.Extension.Enumeration
+import CompPoly.Fields.Binary.Extension.Impl
+import CompPoly.Fields.Binary.Extension.Prelude
+import CompPoly.Fields.Binary.Extension.Primitive
+import CompPoly.Fields.Binary.GF2_32
+import CompPoly.Fields.Binary.GF2_32.Basic
+import CompPoly.Fields.Binary.GF2_32.Impl
+import CompPoly.Fields.Binary.GF2_32.Prelude
+import CompPoly.Fields.Binary.GF2_32.Primitive
+import CompPoly.Fields.Binary.GF2_32.PrimitivePowerCertificate
+import CompPoly.Fields.Binary.GF2_32.RootContexts
+import CompPoly.Fields.Binary.GF2_32.XPowTwoPowGcdCertificate
+import CompPoly.Fields.Binary.GF2_32.XPowTwoPowModCertificate
+import CompPoly.Fields.Binary.GF2_48
+import CompPoly.Fields.Binary.GF2_48.Basic
+import CompPoly.Fields.Binary.GF2_48.Impl
+import CompPoly.Fields.Binary.GF2_48.Prelude
+import CompPoly.Fields.Binary.GF2_48.Primitive
+import CompPoly.Fields.Binary.GF2_48.PrimitivePowerCertificate
+import CompPoly.Fields.Binary.GF2_48.RootContexts
+import CompPoly.Fields.Binary.GF2_48.XPowTwoPowGcdCertificate
+import CompPoly.Fields.Binary.GF2_48.XPowTwoPowModCertificate
+import CompPoly.Fields.Binary.GF2_64
+import CompPoly.Fields.Binary.GF2_64.Basic
+import CompPoly.Fields.Binary.GF2_64.Impl
+import CompPoly.Fields.Binary.GF2_64.Prelude
+import CompPoly.Fields.Binary.GF2_64.Primitive
+import CompPoly.Fields.Binary.GF2_64.PrimitivePowerCertificate
+import CompPoly.Fields.Binary.GF2_64.RootContexts
+import CompPoly.Fields.Binary.GF2_64.XPowTwoPowGcdCertificate
+import CompPoly.Fields.Binary.GF2_64.XPowTwoPowModCertificate
+import CompPoly.Fields.Binary.GF2_72
+import CompPoly.Fields.Binary.GF2_72.Basic
+import CompPoly.Fields.Binary.GF2_72.Impl
+import CompPoly.Fields.Binary.GF2_72.Prelude
+import CompPoly.Fields.Binary.GF2_72.Primitive
+import CompPoly.Fields.Binary.GF2_72.PrimitivePowerCertificate
+import CompPoly.Fields.Binary.GF2_72.RootContexts
+import CompPoly.Fields.Binary.GF2_72.XPowTwoPowGcdCertificate
+import CompPoly.Fields.Binary.GF2_72.XPowTwoPowModCertificate
 import CompPoly.Fields.Binary.Tower.Abstract.Algebra
 import CompPoly.Fields.Binary.Tower.Abstract.Basis
 import CompPoly.Fields.Binary.Tower.Abstract.Core
@@ -218,6 +259,10 @@ import CompPoly.Univariate.Roots.Correctness
 import CompPoly.Univariate.Roots.Enumeration
 import CompPoly.Univariate.Roots.Extraction
 import CompPoly.Univariate.Roots.RootProduct
+import CompPoly.Univariate.Roots.Shoup
+import CompPoly.Univariate.Roots.Shoup.Basic
+import CompPoly.Univariate.Roots.Shoup.Correctness
+import CompPoly.Univariate.Roots.Shoup.FrobeniusLinear
 import CompPoly.Univariate.Roots.SmoothSubgroup
 import CompPoly.Univariate.Roots.SmoothSubgroup.Basic
 import CompPoly.Univariate.Roots.SmoothSubgroup.Correctness

CompPoly/Fields/Binary/Extension/Basic.lean

@@ -0,0 +1,110 @@
+/-
+Copyright (c) 2026 CompPoly Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Valerii Huhnin
+-/
+
+import CompPoly.Fields.Binary.Extension.Prelude
+import Mathlib.FieldTheory.Finite.Basic
+import Mathlib.RingTheory.AdjoinRoot
+
+/-!
+# Direct Binary-Extension Quotient Fields
+
+Generic quotient/specification surface for direct binary extensions
+`GF(2)[X] / (X^m + tail)`.
+
+The field and cardinality instances are conditional on a future
+`Fact (Irreducible (polynomial data))`, so concrete modules can expose the type
+early while certificate files later make it a genuine finite field.
+-/
+
+namespace BinaryField
+
+namespace Extension
+
+open Polynomial AdjoinRoot
+
+noncomputable section
+
+/-- Quotient/specification carrier for a direct binary extension. -/
+abbrev SpecField (data : DefiningPolynomialData) : Type :=
+  AdjoinRoot (polynomial data)
+
+/-- The quotient specification is inhabited. -/
+instance instInhabitedSpecField (data : DefiningPolynomialData) :
+    Inhabited (SpecField data) :=
+  ⟨0⟩
+
+/-- Conditional field instance, available once irreducibility is certified. -/
+instance instFieldSpecField (data : DefiningPolynomialData)
+    [Fact (Irreducible (polynomial data))] :
+    Field (SpecField data) :=
+  AdjoinRoot.instField
+
+/-- Conditional nontriviality, available once irreducibility is certified. -/
+instance instNontrivialSpecField (data : DefiningPolynomialData)
+    [Fact (Irreducible (polynomial data))] :
+    Nontrivial (SpecField data) :=
+  inferInstance
+
+/-- Algebra structure over `GF(2)`. -/
+instance instAlgebraSpecField (data : DefiningPolynomialData) :
+    Algebra (ZMod 2) (SpecField data) :=
+  AdjoinRoot.instAlgebra (polynomial data)
+
+/-- Conditional characteristic-two instance, available once irreducibility is certified. -/
+instance instCharTwoSpecField (data : DefiningPolynomialData)
+    [Fact (Irreducible (polynomial data))] :
+    CharP (SpecField data) 2 := by
+  haveI : CharP (ZMod 2) 2 := inferInstance
+  exact charP_of_injective_algebraMap' (ZMod 2) 2
+
+/-- Canonical embedding of `GF(2)` into the quotient specification. -/
+def ofGF2 (data : DefiningPolynomialData) : ZMod 2 →+* SpecField data :=
+  algebraMap (ZMod 2) (SpecField data)
+
+/-- The quotient root/generator. -/
+def root (data : DefiningPolynomialData) : SpecField data :=
+  AdjoinRoot.root (polynomial data)
+
+/-- The quotient root satisfies the defining polynomial. -/
+theorem root_satisfies_polynomial (data : DefiningPolynomialData) :
+    eval₂ (algebraMap (ZMod 2) (SpecField data)) (root data)
+      (polynomial data) = 0 := by
+  unfold root
+  exact AdjoinRoot.eval₂_root (polynomial data)
+
+/-- Conditional finite type, available once irreducibility is certified. -/
+instance instFintypeSpecField (data : DefiningPolynomialData)
+    [Fact (Irreducible (polynomial data))] :
+    Fintype (SpecField data) := by
+  have hpoly_ne_zero : polynomial data ≠ 0 :=
+    Irreducible.ne_zero (Fact.out : Irreducible (polynomial data))
+  let pb := AdjoinRoot.powerBasis hpoly_ne_zero
+  letI : Module.Finite (ZMod 2) (SpecField data) := PowerBasis.finite pb
+  haveI : Finite (SpecField data) := by
+    have : Module.finrank (ZMod 2) (SpecField data) = pb.dim :=
+      PowerBasis.finrank pb
+    exact Finite.of_equiv (Fin pb.dim →₀ ZMod 2) (pb.basis.repr.toEquiv.symm)
+  exact Fintype.ofFinite (SpecField data)
+
+/-- Cardinality of a certified direct binary-extension quotient. -/
+theorem specField_card (data : DefiningPolynomialData)
+    [Fact (Irreducible (polynomial data))] :
+    Fintype.card (SpecField data) = 2 ^ data.degree := by
+  rw [Module.card_eq_pow_finrank (K := ZMod 2) (V := SpecField data)]
+  have hpoly_ne_zero : polynomial data ≠ 0 :=
+    Irreducible.ne_zero (Fact.out : Irreducible (polynomial data))
+  let pb := AdjoinRoot.powerBasis hpoly_ne_zero
+  rw [PowerBasis.finrank pb]
+  have h_pb_dim : pb.dim = (polynomial data).natDegree := by
+    rfl
+  rw [h_pb_dim, polynomial_natDegree]
+  norm_num
+
+end
+
+end Extension
+
+end BinaryField

CompPoly/Fields/Binary/Extension/Enumeration.lean

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2026 CompPoly Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Valerii Huhnin
+-/
+
+import CompPoly.Fields.Binary.Extension.Impl
+import CompPoly.Univariate.Roots.Enumeration
+
+/-!
+# Direct Binary-Extension Field Enumerations
+
+Lazy finite-field enumeration contexts for executable direct binary-extension
+carriers.
+-/
+
+namespace BinaryField
+
+namespace Extension
+
+namespace Concrete
+
+open CompPoly.CPolynomial.Roots.FiniteField
+
+variable (params : ExecutableParams)
+
+private theorem toNat_lt (a : ConcreteField params) :
+    toNat params a < fieldSize params.degree := by
+  simpa [toNat, toBitVec, fieldSize] using (toBitVec params a).isLt
+
+private theorem ofNat_toNat (a : ConcreteField params) :
+    ofNat params (toNat params a) = a := by
+  apply BitVec.eq_of_toNat_eq
+  simp [toNat, toBitVec, ofNat, ofBitVec]
+
+/-- Lazy complete enumeration for a direct executable binary-extension carrier. -/
+def fieldEnumeration : FieldEnumeration (ConcreteField params) where
+  size := fieldSize params.degree
+  elem i := ofNat params i.val
+  complete := by
+    intro a
+    exact ⟨⟨toNat params a, toNat_lt params a⟩, ofNat_toNat params a⟩
+
+end Concrete
+
+end Extension
+
+end BinaryField