def Hex.certifyIrreducible? (f : ZPoly) : Option ZPolyIrreducibilityCertificate

Build a checked multi-prime degree-obstruction certificate for a primitive, positive-degree integer polynomial. Prime blocks are added only until every possible proper factor degree is obstructed.

Equations

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

theorem Hex.certifies_of_certifyIrreducible?_eq_some {f : ZPoly} {cert : ZPolyIrreducibilityCertificate} (h : certifyIrreducible? f = some cert) : cert.certifies f = true

A certificate returned by the generator passes the complete executable irreducibility check, including primality, primitivity, and positive degree.

structure Hex.PrimeChoiceDataScore : Type

A successful modular factorization paired with its number of factors.

• data : PrimeChoiceData

  The modular factorization data.

• factorCount : Nat

  The number of factors in data.factorsModP.

def Hex.probePrimeData? (f : ZPoly) (c : SmallPrimeCandidate) : Option PrimeChoiceData

Factor f at one explicit small-prime candidate, returning the same PrimeChoiceData payload used by the production selector when the candidate is good.

This is a diagnostic surface for attributing adaptive-prime work and inspecting the modular degree information already computed by a trial. It deliberately shares primeChoiceDataScore with the selector so benchmark instrumentation cannot drift to a different modular computation.

Equations

• Hex.probePrimeData? f c = Option.map (fun (x : Hex.PrimeChoiceDataScore) => x.data) (Hex.primeChoiceDataScore✝ f c)

def Hex.choosePrimeDataScoreStep (f : ZPoly) (best : Option PrimeChoiceDataScore) (c : SmallPrimeCandidate) : Option PrimeChoiceDataScore

Keep the prime factorization with the lower recombination score.

Equations

• Hex.choosePrimeDataScoreStep f (some old) c = some old
• Hex.choosePrimeDataScoreStep f none c = Hex.primeChoiceDataScore✝ f c

def Hex.choosePrimeData? (f : ZPoly) : Option PrimeChoiceData

Optional prime selection: returns some with the chosen PrimeChoiceData when the fixed candidate search finds a good prime for f, and none otherwise.

The search first folds choosePrimeDataScoreStep over the deterministic small-prime prefix. If that prefix selects an admissible prime, the original tie-breaking is preserved. If the prefix exhausts without selecting any prime, the search folds over the fixed extended prime list through 499, covering every odd prime in the hot-path interval [3, 500].

def Hex.choosePrimeDataAdaptive? (f : ZPoly) (extra : Nat) : Option PrimeChoiceData

Select the first good prime, except that a split modular image receives a bounded search for a good prime with fewer modular factors, with the early-stop policy implemented by improvePrimeData?.

Equations

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

theorem Hex.choosePrimeDataAdaptive?_prime (f : ZPoly) (extra : Nat) (data : PrimeChoiceData) (hdata : choosePrimeDataAdaptive? f extra = some data) : Nat.Prime data.p

Adaptive prime selection returns only prime moduli.

theorem Hex.choosePrimeDataAdaptive?_p_le_500 (f : ZPoly) (extra : Nat) (data : PrimeChoiceData) (hdata : choosePrimeDataAdaptive? f extra = some data) : data.p ≤ 500

Every prime returned by the adaptive selector is at most 500: its look-ahead only rearranges the fixed small-prime candidate lists.

theorem Hex.choosePrimeDataAdaptive?_fModP_eq (f : ZPoly) (extra : Nat) (data : PrimeChoiceData) (hdata : choosePrimeDataAdaptive? f extra = some data) : data.fModP = ZPoly.modP data.p f

Adaptive prime selection caches the reduction of its input polynomial.

theorem Hex.choosePrimeDataAdaptive?_isGoodPrime (f : ZPoly) (extra : Nat) (data : PrimeChoiceData) (hdata : choosePrimeDataAdaptive? f extra = some data) : isGoodPrime f data.p = true

Adaptive prime selection returns a prime satisfying the admissibility test.

theorem Hex.choosePrimeData?_prime (f : ZPoly) (data : PrimeChoiceData) (hdata : choosePrimeData? f = some data) : Nat.Prime data.p

Ordinary prime selection returns only prime moduli.

theorem Hex.choosePrimeData?_p_le_500 (f : ZPoly) (data : PrimeChoiceData) (hdata : choosePrimeData? f = some data) : data.p ≤ 500

Every prime returned by the fixed hot-path search is at most 500.

theorem Hex.choosePrimeData?_fModP_eq (f : ZPoly) (data : PrimeChoiceData) (hdata : choosePrimeData? f = some data) : data.fModP = ZPoly.modP data.p f

Ordinary prime selection caches the reduction of its input polynomial.

theorem Hex.choosePrimeData?_isGoodPrime (f : ZPoly) (data : PrimeChoiceData) (hdata : choosePrimeData? f = some data) : isGoodPrime f data.p = true

When choosePrimeData? f succeeds, the selected prime is a good prime for f in the executable sense (modulus at least three, leading coefficient survives reduction, modular image is square-free).

theorem Hex.mem_hotPathCandidates_isGoodPrime_false_of_choosePrimeData?_none {f : ZPoly} (hf : choosePrimeData? f = none) {c : SmallPrimeCandidate} (hc : c ∈ hotPathCandidates) : isGoodPrime f c.m = false

When choosePrimeData? f returns none, every candidate in the hot-path prime list fails the executable good-prime predicate Hex.isGoodPrime f.

This records that failure of the fixed candidate fold means every retained candidate was tried and rejected.

theorem Hex.choosePrimeData?_ne_none_of_good {f : ZPoly} {c : SmallPrimeCandidate} (hc : c ∈ hotPathCandidates) (hgood : isGoodPrime f c.m = true) : choosePrimeData? f ≠ none

A good member of the fixed hot-path list forces prime selection to succeed. This is the direct contrapositive of the selector's complete failure certificate.

theorem Hex.choosePrimeDataAdaptive?_ne_none_of_good {f : ZPoly} {c : SmallPrimeCandidate} {extra : Nat} (hc : c ∈ hotPathCandidates) (hgood : isGoodPrime f c.m = true) : choosePrimeDataAdaptive? f extra ≠ none

A good member of the fixed hot-path list also forces the adaptive selector to succeed; its look-ahead changes only which successful record is returned.

def Hex.factorsModPBerlekampForm (f : ZPoly) (data : PrimeChoiceData) : Prop

Invariant capturing that data.factorsModP is exactly the Berlekamp factor output for the monic modular image used by prime selection. Phrased as an existential bundling the prime witness and the nonzero-image proof so that it threads through the executable prime-selection fold; the Lean.Grind.Field instance required by Berlekamp.berlekampFactor is constructed explicitly from hprime, so callers can match it against any field instance built from the same prime witness via proof irrelevance of ZMod64.PrimeModulus.

Equations

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

theorem Hex.probePrimeData?_prime (f : ZPoly) (c : SmallPrimeCandidate) (data : PrimeChoiceData) (hdata : probePrimeData? f c = some data) : Nat.Prime data.p

Primality provenance for one explicit diagnostic/degree-obstruction trial.

theorem Hex.probePrimeData?_p_le (f : ZPoly) (c : SmallPrimeCandidate) (data : PrimeChoiceData) (hc : c.m ≤ 500) (hdata : probePrimeData? f c = some data) : data.p ≤ 500

An explicit trial inherits any proved upper bound on its candidate prime.

theorem Hex.probePrimeData?_isGoodPrime (f : ZPoly) (c : SmallPrimeCandidate) (data : PrimeChoiceData) (hdata : probePrimeData? f c = some data) : isGoodPrime f data.p = true

Good-prime provenance for one explicit diagnostic/degree-obstruction trial.

theorem Hex.probePrimeData?_fModP_eq (f : ZPoly) (c : SmallPrimeCandidate) (data : PrimeChoiceData) (hdata : probePrimeData? f c = some data) : data.fModP = ZPoly.modP data.p f

Modular-image provenance for one explicit trial.

theorem Hex.probePrimeData?_form (f : ZPoly) (c : SmallPrimeCandidate) (data : PrimeChoiceData) (hdata : probePrimeData? f c = some data) : factorsModPBerlekampForm f data

Berlekamp-factor provenance for one explicit trial.

theorem Hex.choosePrimeDataAdaptive?_form (f : ZPoly) (extra : Nat) (data : PrimeChoiceData) (hdata : choosePrimeDataAdaptive? f extra = some data) : ∃ (hzero : DensePoly.isZero (ZPoly.modP data.p f) = false), data.factorsModP = (List.map monicModularImage (Berlekamp.berlekampFactor (monicModularImage (ZPoly.modP data.p f)) ⋯).factors).toArray

Adaptive selection returns the certified Berlekamp factorization of the modular image.

theorem Hex.choosePrimeData?_factorsModP_berlekamp_form (f : ZPoly) (data : PrimeChoiceData) (hdata : choosePrimeData? f = some data) : ∃ (hzero : DensePoly.isZero (ZPoly.modP data.p f) = false), data.factorsModP = (List.map monicModularImage (Berlekamp.berlekampFactor (monicModularImage (ZPoly.modP data.p f)) ⋯).factors).toArray

When choosePrimeData? f succeeds, the stored modular factor array is exactly the Berlekamp factor output for the monic modular image of the selected candidate. Mirrors the _prime / _fModP_eq / _isGoodPrime provenance chains, exposing the executable surface used by the small-mod singleton irreducibility composition.

theorem Hex.choosePrimeData?_berlekampFactor_factors_length_le_one_of_small (f : ZPoly) (data : PrimeChoiceData) (hdata : choosePrimeData? f = some data) (hsmall : data.factorsModP.size ≤ 1) : ∃ (hzero : DensePoly.isZero (ZPoly.modP data.p f) = false), (Berlekamp.berlekampFactor (monicModularImage (ZPoly.modP data.p f)) ⋯).factors.length ≤ 1

Small-mod singleton executable branch fact for the selected monic modular image.

When choosePrimeData? succeeds and the public factorsModP field has size at most one, the underlying Berlekamp factor list for monicModularImage (ZPoly.modP data.p f) also has length at most one. This is the Mathlib-free shape fact needed before applying Berlekamp soundness in a caller that already imports the heavier Rabin proof module.

def Hex.henselLiftData (f : ZPoly) (B : Nat) (d : PrimeChoiceData) : LiftData

Lift the chosen modular factors to the requested precision for integer recombination.

Equations

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

@[simp]

theorem Hex.henselLiftData_p (f : ZPoly) (B : Nat) (d : PrimeChoiceData) : (henselLiftData f B d).p = d.p

The lift data keeps the selected prime.

@[simp]

theorem Hex.henselLiftData_k (f : ZPoly) (B : Nat) (d : PrimeChoiceData) : (henselLiftData f B d).k = B

The lift data keeps the requested precision exponent.