def Hex.ZPoly.X : ZPoly

The integer polynomial X.

Equations

• Hex.ZPoly.X = Hex.DensePoly.monomial 1 1

structure Hex.ZPoly.XPowerData : Type

Data from extracting the largest visible power of X from a dense integer polynomial.

• power : Nat

  The largest exponent of X dividing the input.

• core : ZPoly

  The quotient after removing that power of X.

def Hex.ZPoly.extractXPower (f : ZPoly) : XPowerData

Remove the initial zero-coefficient run from a dense integer polynomial.

Dense coefficients are stored in ascending degree order, so the initial zero run is exactly the executable power of X dividing the polynomial.

Equations

• One or more equations did not get rendered due to their size.

def Hex.ZPoly.leadingCoeffModP (f : ZPoly) (p : Nat) [ZMod64.Bounds p] : ZMod64 p

The integer leading coefficient reduced to the candidate prime field.

Equations

• f.leadingCoeffModP p = Hex.ZMod64.ofNat p (Hex.ZPoly.intModNat (Hex.DensePoly.leadingCoeff f) p)

def Hex.leadingCoeffAdmissible (f : ZPoly) (p : Nat) [ZMod64.Bounds p] : Prop

The candidate prime does not divide the integer leading coefficient.

Equations

• Hex.leadingCoeffAdmissible f p = (f.leadingCoeffModP p ≠ 0)

def Hex.gcdIsUnit {R : Type u} [Zero R] [DecidableEq R] (g : DensePoly R) : Bool

Executable test that a field-polynomial gcd is a unit.

DensePoly.gcd is the raw Euclidean representative, so over a field it may be any nonzero constant associate of 1. In normalized dense representation, nonzero constants are exactly the polynomials with one stored coefficient.

Equations

• Hex.gcdIsUnit g = (g.size == 1)

def Hex.squareFreeModP (f : ZPoly) (p : Nat) [ZMod64.Bounds p] : Prop

The modular image is square-free according to the executable gcd-unit criterion.

Equations

• Hex.squareFreeModP f p = (Hex.gcdIsUnit (Hex.DensePoly.gcd (Hex.ZPoly.modP p f) (Hex.DensePoly.derivative (Hex.ZPoly.modP p f))) = true)

def Hex.isGoodPrime (f : ZPoly) (p : Nat) [ZMod64.Bounds p] : Bool

Executable good-prime predicate for the Berlekamp-Zassenhaus computation.

It checks that the modulus is at least 3, that the integer leading coefficient survives reduction modulo p, and that the modular image is square-free.

Equations

• Hex.isGoodPrime f p = (decide (3 ≤ p) && f.leadingCoeffModP p != 0 && Hex.gcdIsUnit (Hex.DensePoly.gcd (Hex.ZPoly.modP p f) (Hex.DensePoly.derivative (Hex.ZPoly.modP p f))))

def Hex.isGoodPrimeImpl (f : ZPoly) (p : Nat) [ZMod64.Bounds p] : Bool

Compiled good-prime predicate using the inverse-cached finite-field GCD.

Equations

• Hex.isGoodPrimeImpl f p = (decide (3 ≤ p) && f.leadingCoeffModP p != 0 && Hex.gcdIsUnit ((Hex.ZPoly.modP p f).gcdCached (Hex.DensePoly.derivative (Hex.ZPoly.modP p f))))

@[csimp]

theorem Hex.isGoodPrime_eq_impl : isGoodPrime = isGoodPrimeImpl

Proof-backed compiled implementation of good-prime testing that computes one leading-coefficient inverse per polynomial remainder pass.

theorem Hex.isGoodPrime_of_admissible (f : ZPoly) (p : Nat) [ZMod64.Bounds p] (hp : 3 ≤ p) (hlc : f.leadingCoeffModP p ≠ 0) (hsq : gcdIsUnit (DensePoly.gcd (ZPoly.modP p f) (DensePoly.derivative (ZPoly.modP p f))) = true) : isGoodPrime f p = true

Assemble the executable good-prime result from its three mathematical components.

theorem Hex.bounds_three : ZMod64.Bounds 3

The ZMod64.Bounds instance witness for p = 3.

@[reducible, inline]

abbrev Hex.SmallPrimeCandidate : Type

The Berlekamp--Zassenhaus hot path uses the shared bundled prime supplied by hex-mod-arith; it carries both the runtime modulus and its dependent bounds and primality evidence.

Equations

• Hex.SmallPrimeCandidate = Hex.ZMod64.Prime

def Hex.tableCandidates (lo hi : Nat) (hhi : hi ≤ 2 ^ 31) : List SmallPrimeCandidate

The committed table primes in [lo, hi), bundled with the bounds and primality evidence required by ZMod64.

Equations

• One or more equations did not get rendered due to their size.

structure Hex.PrimeCandidateScore : Type

A scored admissible small-prime candidate for default prime selection.

• p : Nat

  Candidate prime.

• factorCount : Nat

  Smaller scores are preferred; equal scores retain the earlier smaller prime.

def Hex.smallPrimeCandidates : List SmallPrimeCandidate

The default small-prime prefix, represented by the committed table window [3, 72).

Equations

• Hex.smallPrimeCandidates = Hex.tableCandidates 3 72 Hex.smallPrimeCandidates._proof_1✝

def Hex.extendedSmallPrimeCandidates : List SmallPrimeCandidate

The remaining hot-path primes, represented by the committed table window [72, 501).

Equations

• Hex.extendedSmallPrimeCandidates = Hex.tableCandidates 72 501 Hex.extendedSmallPrimeCandidates._proof_1✝

def Hex.hotPathCandidates : List SmallPrimeCandidate

The direct planner's prime candidate list: the deterministic small-prime prefix followed by every prime up to 499.

Equations

• Hex.hotPathCandidates = Hex.smallPrimeCandidates ++ Hex.extendedSmallPrimeCandidates

def Hex.hotPathPrimorial : Nat

Product of the fixed hot-path candidate primes.

Equations

• Hex.hotPathPrimorial = (List.map (fun (c : Hex.SmallPrimeCandidate) => c.m) Hex.hotPathCandidates).prod

theorem Hex.hotPathPrimeValues_nodup : (List.map (fun (c : SmallPrimeCandidate) => c.m) hotPathCandidates).Nodup

The fixed hot-path list contains no repeated prime values.

theorem Hex.mem_hotPathCandidates_prime {c : SmallPrimeCandidate} (hc : c ∈ hotPathCandidates) : Nat.Prime c.m ∧ 3 ≤ c.m ∧ c.m ≤ 500

Soundness of the hot-path prime candidate list: every entry carries a prime in the closed range [3, 500]. The primality conjunct is the structure field; the bounds come from the two table windows.

theorem Hex.exists_mem_hotPathCandidates_of_prime {p : Nat} (hprime : Nat.Prime p) (hge : 3 ≤ p) (hle : p ≤ 500) : ∃ (c : SmallPrimeCandidate), c ∈ hotPathCandidates ∧ c.m = p

Coverage of the hot-path prime candidate list: every prime p with 3 ≤ p ≤ 500 appears as the .m field of some candidate, by completeness of the committed table.

def Hex.monicModularImage {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : FpPoly p

Coerce an admissible nonzero modular image to its monic representative by dividing by its leading coefficient. monicModularImage f = scale c⁻¹ f where c = leadingCoeff f; the zero image maps to zero so the operation is total.

Equations

• Hex.monicModularImage f = if Hex.DensePoly.isZero f = true then 0 else Hex.DensePoly.scale (Hex.DensePoly.leadingCoeff f)⁻¹ f

theorem Hex.monicModularImage_monic {p : Nat} [ZMod64.Bounds p] (hp : Nat.Prime p) (f : FpPoly p) (hgood : DensePoly.isZero f = false) : DensePoly.Monic (monicModularImage f)

Normalizing a nonzero polynomial over a prime field produces a monic polynomial.

theorem Hex.isZero_false_of_ne_zero {p : Nat} [ZMod64.Bounds p] {f : FpPoly p} (hf : f ≠ 0) : DensePoly.isZero f = false

A nonzero FpPoly p translates to isZero = false.

theorem Hex.monicModularImage_ne_zero_of_ne_zero {p : Nat} [ZMod64.Bounds p] (hp : Nat.Prime p) {f : FpPoly p} (hf : f ≠ 0) : monicModularImage f ≠ 0

monicModularImage of a nonzero polynomial is nonzero (it's a unit scalar of the original).

theorem Hex.monicModularImage_eq_self_of_monic {p : Nat} [ZMod64.Bounds p] (hp : Nat.Prime p) (f : FpPoly p) (hmonic : DensePoly.Monic f) : monicModularImage f = f

monicModularImage is the identity on monic polynomials: dividing by a leading coefficient of 1 is a no-op.

theorem Hex.monicModularImage_mul_of_nonzero {p : Nat} [ZMod64.Bounds p] (hp : Nat.Prime p) {a b : FpPoly p} (ha : a ≠ 0) (hb : b ≠ 0) : monicModularImage (a * b) = monicModularImage a * monicModularImage b

Multiplicativity of monicModularImage on nonzero polynomials. The leading coefficient of a product is the product of leading coefficients (no-zero-divisors over a prime field), so dividing both sides by their leading coefficients agrees with dividing the product by its leading coefficient.

theorem Hex.factorProduct_map_monicModularImage_eq_monicModularImage_factorProduct {p : Nat} [ZMod64.Bounds p] (hp : Nat.Prime p) (l : List (FpPoly p)) (hne : ∀ (g : FpPoly p), g ∈ l → g ≠ 0) : Berlekamp.factorProduct (List.map monicModularImage l) = monicModularImage (Berlekamp.factorProduct l)

monicModularImage is multiplicative across Hex.Berlekamp.factorProduct on lists of nonzero factors: pulling each factor through monicModularImage before taking the product agrees with applying monicModularImage to the raw product. Inductive consequence of monicModularImage_mul_of_nonzero plus monicModularImage_eq_self_of_monic at the base case factorProduct [] = 1.

def Hex.modularFactorDegreesAt? (f : ZPoly) (p : Nat) : Option (Array Nat)

Return the sorted degrees of the Berlekamp factors of f mod p at an explicit small prime supported by the executable prime-selection list.

This testing-facing surface deliberately reuses the production small-prime computation. For complete linear splits, it records the explicit root-degree evidence directly so pinned conformance checks are not sensitive to the current Berlekamp witness splitting surface. It returns none if p is unsupported or the leading coefficient vanishes modulo p; the Berlekamp branch also requires the usual good-prime predicate.

Equations

• One or more equations did not get rendered due to their size.

def Hex.choosePrimeScore? (f : ZPoly) : Option PrimeCandidateScore

Scan the fixed hot-path prime list and return the best admissible scored candidate, if any.

Equations

• Hex.choosePrimeScore? f = List.foldl (Hex.choosePrimeScoreStep✝ f) none Hex.hotPathCandidates

def Hex.choosePrime (f : ZPoly) : Nat

Choose a small admissible prime for the Berlekamp-Zassenhaus computation.

The search is bounded to a fixed ascending list of small primes. Candidate scores use the currently available executable modular factor surface; strict score improvement replaces the incumbent, so equal scores keep the smaller earlier prime.

theorem Hex.choosePrimeScore?_isGoodPrime (f : ZPoly) (score : PrimeCandidateScore) (hscore : choosePrimeScore? f = some score) : ∃ (hbounds : ZMod64.Bounds score.p), isGoodPrime f score.p = true

Any score the hot-path walk returns records a prime that passes the good-prime check for f.

theorem Hex.choosePrime_isGoodPrime_of_selected (f : ZPoly) (score : PrimeCandidateScore) (hscore : choosePrimeScore? f = some score) (hchoose : choosePrime f = score.p) : ∃ (hbounds : ZMod64.Bounds (choosePrime f)), isGoodPrime f (choosePrime f) = true

When choosePrime returns the winning score's prime, that prime passes the good-prime check for f.

theorem Hex.isGoodPrime_ge_three (f : ZPoly) (p : Nat) [ZMod64.Bounds p] (hgood : isGoodPrime f p = true) : 3 ≤ p

A successful good-prime check certifies the modulus is at least three.

theorem Hex.isGoodPrime_leadingCoeffAdmissible (f : ZPoly) (p : Nat) [ZMod64.Bounds p] (hgood : isGoodPrime f p = true) : leadingCoeffAdmissible f p

A successful good-prime check certifies leading-coefficient admissibility.

theorem Hex.isGoodPrime_squareFreeModP (f : ZPoly) (p : Nat) [ZMod64.Bounds p] (hgood : isGoodPrime f p = true) : squareFreeModP f p

A successful good-prime check certifies the modular square-free precondition.

theorem Hex.isGoodPrime_modP_isZero_false (f : ZPoly) (p : Nat) [ZMod64.Bounds p] (hgood : isGoodPrime f p = true) : DensePoly.isZero (ZPoly.modP p f) = false

A successful good-prime check rules out a vanishing modular image: the leading coefficient survives reduction modulo p, so the modular image retains at least one stored coefficient.

theorem Hex.leadingCoeffAdmissible_size_pos (f : ZPoly) (p : Nat) [ZMod64.Bounds p] (hadm : leadingCoeffAdmissible f p) : 0 < DensePoly.size f

leadingCoeffAdmissible forces the source polynomial to have at least one stored coefficient: the empty coefficient array would force leadingCoeffModP to vanish.

theorem Hex.modP_ne_zero_of_leadingCoeffAdmissible (f : ZPoly) (p : Nat) [ZMod64.Bounds p] (hadm : leadingCoeffAdmissible f p) : ZPoly.modP p f ≠ 0

Under leadingCoeffAdmissible, the modular image is nonzero. Companion of isGoodPrime_modP_isZero_false but with the weaker admissibility hypothesis (no square-free or 3 ≤ p requirement).

theorem Hex.size_modP_eq_of_leadingCoeffAdmissible (f : ZPoly) (p : Nat) [ZMod64.Bounds p] (hadm : leadingCoeffAdmissible f p) : DensePoly.size (ZPoly.modP p f) = DensePoly.size f

Under leadingCoeffAdmissible, the modular image has the same size as the input: the top coefficient survives reduction, so the trailing-zero trim does nothing.

theorem Hex.degree?_modP_eq_of_leadingCoeffAdmissible (f : ZPoly) (p : Nat) [ZMod64.Bounds p] (hadm : leadingCoeffAdmissible f p) : DensePoly.degree? (ZPoly.modP p f) = DensePoly.degree? f

Under leadingCoeffAdmissible, the modular image has the same degree? as the input.

theorem Hex.leadingCoeff_modP_eq_leadingCoeffModP_of_admissible (f : ZPoly) (p : Nat) [ZMod64.Bounds p] (hadm : leadingCoeffAdmissible f p) : DensePoly.leadingCoeff (ZPoly.modP p f) = f.leadingCoeffModP p

Under leadingCoeffAdmissible, the leading coefficient of the modular image matches leadingCoeffModP.