def Hex.reassemblePolynomialFactors (d : FactorNormalizationData) (coreFactors : Array ZPoly) : Array ZPoly

Reassemble normalization-prefix and square-free factors around the supplied factors of the square-free part, expanding each square-free factor q to its multiplicity in d.repeatedPart so the recorded Factorization carries the right exponents for higher-multiplicity inputs. Falls back to the un-expanded polynomialNormalizationPrefixFactors shape when the expansion does not fully consume repeatedPart (e.g. when the BZ computation emitted the raw primitive square-free part as a single square-free factor).

Equations

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

def Hex.factorizationOfFactors (f : ZPoly) (factors : Array ZPoly) : Factorization

Package a verified factor array as a factorization with collected multiplicities.

Equations

• Hex.factorizationOfFactors f factors = { scalar := Hex.signedContentScalar f, factors := Hex.collectFactorMultiplicities factors }

structure Hex.PrimeFactorData : Type

Per-prime modular irreducibility evidence for integer irreducibility certificates.

The factor array records the modular factors observed at this prime. The degree list and Rabin certificates are zipped with those concrete factors so the checker can validate certificate metadata and the executable Rabin witness against the polynomial it is meant to certify.

• p : Nat

  The prime characteristic of this factorization.

• bounds : ZMod64.Bounds self.p

  Word-arithmetic bounds witness for p, available for instance search.

• factorDegrees : Array Nat

  The degrees of the modular irreducible factors.

• factorPolys : Array (FpPoly self.p)

  The modular irreducible factors themselves.

• factorCerts : Array Berlekamp.IrreducibilityCertificate

  Rabin certificates paired with factorPolys.

structure Hex.DegreeObstruction : Type

Evidence that a candidate integer factor degree is impossible for one recorded prime block.

If an integer factor has degree targetDegree, then reducing modulo any good prime gives a product of modular irreducible factors whose degrees sum to targetDegree. The checker validates an obstruction by confirming that the referenced prime block has no subset of recorded factor degrees with this sum.

• targetDegree : Nat

  The proposed integer factor degree ruled out by this obstruction.

• primeIndex : Nat

  The index of the prime factorization whose subset sums rule it out.

structure Hex.ZPolyIrreducibilityCertificate : Type

Checker-first certificate data for irreducibility over Z[x].

Each entry groups all modular degree and irreducibility-certificate data for a single prime so the checker can validate the prime and degree metadata before the later proof layer interprets the degree obstruction mathematically.

• perPrime : Array PrimeFactorData

  Modular factorizations used by the certificate.

• degreeObstructions : Array DegreeObstruction

  Obstructions covering every possible proper factor degree.

def Hex.PrimeFactorData.degreeSum (d : PrimeFactorData) : Nat

Sum the recorded modular factor degrees for one prime.

Equations

• d.degreeSum = List.foldl (fun (acc n : Nat) => acc + n) 0 d.factorDegrees.toList

def Hex.PrimeFactorData.factorProduct (d : PrimeFactorData) : FpPoly d.p

Ordered product of the recorded modular factors for one prime.

Equations

• d.factorProduct = Array.foldl (fun (x1 x2 : Hex.FpPoly d.p) => x1 * x2) 1 d.factorPolys

def Hex.PrimeFactorData.containsDegree (d : PrimeFactorData) (n : Nat) : Bool

Does the recorded degree multiset contain n?

Equations

• d.containsDegree n = d.factorDegrees.toList.any fun (degree : Nat) => degree == n

def Hex.PrimeFactorData.hasSubsetDegreeAux : List Nat → Nat → Bool

Test whether a submultiset of the listed degrees sums to the target.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PrimeFactorData.hasSubsetDegreeAux [] x✝ = (x✝ == 0)

def Hex.PrimeFactorData.hasSubsetDegree (d : PrimeFactorData) (target : Nat) : Bool

Does some subset of this prime block's modular factor degrees sum to target?

Equations

• d.hasSubsetDegree target = Hex.PrimeFactorData.hasSubsetDegreeAux d.factorDegrees.toList target

def Hex.PrimeFactorData.checkCertAtFactor (d : PrimeFactorData) (degree : Nat) (factor : FpPoly d.p) (cert : Berlekamp.IrreducibilityCertificate) : Bool

Check one nested finite-field irreducibility certificate against its degree slot and the concrete modular factor occupying that slot.

Equations

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

def Hex.PrimeFactorData.checkFactorCerts (d : PrimeFactorData) : Bool

Check that nested certificates match the enclosing prime, degree array, and concrete modular factor array.

Equations

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

def Hex.PrimeFactorData.checkForPolynomial (f : ZPoly) (d : PrimeFactorData) : Bool

Check one prime block against the integer polynomial being certified.

Equations

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

def Hex.ZPolyIrreducibilityCertificate.candidateFactorDegrees (f : ZPoly) : List Nat

Nontrivial integer factor degrees that must be ruled out for f.

Equations

• Hex.ZPolyIrreducibilityCertificate.candidateFactorDegrees f = List.map (fun (i : Nat) => i + 1) (List.range (Hex.DensePoly.natDegree f / 2))

def Hex.ZPolyIrreducibilityCertificate.primeDataAt? (cert : ZPolyIrreducibilityCertificate) (idx : Nat) : Option PrimeFactorData

Look up a per-prime block by the index stored in an obstruction.

Equations

• cert.primeDataAt? idx = match List.drop idx cert.perPrime.toList with | [] => none | primeData :: tail => some primeData

def Hex.DegreeObstruction.checkForCertificate (f : ZPoly) (cert : ZPolyIrreducibilityCertificate) (obs : DegreeObstruction) : Bool

Check one degree obstruction against the certificate's per-prime degree data.

The target must be one of the nontrivial candidate degrees for f, and the referenced prime block must have no subset of modular factor degrees summing to that target.

Equations

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

def Hex.ZPolyIrreducibilityCertificate.hasObstructionFor (f : ZPoly) (cert : ZPolyIrreducibilityCertificate) (targetDegree : Nat) : Bool

Does the obstruction array contain a valid obstruction for targetDegree?

Equations

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

def Hex.ZPolyIrreducibilityCertificate.checkDegreeObstructions (f : ZPoly) (cert : ZPolyIrreducibilityCertificate) : Bool

Check that every candidate nontrivial factor degree is ruled out.

Equations

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

def Hex.checkIrreducibleCert (f : ZPoly) (cert : ZPolyIrreducibilityCertificate) : Bool

Executable surface checker for integer-polynomial irreducibility certificates.

This validates all computational alignment data available at this layer: every prime block must use an admissible prime for f, its recorded modular factors must multiply back to the modular image, each nested finite-field certificate must match the enclosing prime and its concrete factor, and every nontrivial integer factor degree must be excluded by explicit per-prime degree data.

Equations

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

def Hex.ZPolyIrreducibilityCertificate.certifies (cert : ZPolyIrreducibilityCertificate) (f : ZPoly) : Bool

Does this certificate establish integer irreducibility? Besides checking its modular factorizations and degree obstructions, this includes the three mathematical side conditions needed to interpret them: every modulus is prime, the polynomial is primitive, and its degree is positive.

Equations

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

def Hex.PrimeFactorData.checkCertAtFactorLinear (d : PrimeFactorData) (degree : Nat) (factor : FpPoly d.p) (cert : Berlekamp.IrreducibilityCertificate) : Bool

Kernel-reducible counterpart of checkCertAtFactor.

Identical metadata alignment checks, but the nested Rabin certificate is replayed through Berlekamp.checkIrreducibilityCertificateLinearIncremental, whose pow-chain validation costs O(n · p) kernel multiplications per factor instead of the O(Σ p^k) recomputation against the committed FpPoly.frobeniusXPowMod. The incremental comparison is preferred over Berlekamp.checkIrreducibilityCertificateLinear because certificate replay targets degrees where p^n overwhelms any kernel budget while n · p stays cheap.

Equations

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

def Hex.PrimeFactorData.checkFactorCertsLinear (d : PrimeFactorData) : Bool

Kernel-reducible counterpart of checkFactorCerts, replaying each nested certificate through checkCertAtFactorLinear.

Equations

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

def Hex.PrimeFactorData.checkForPolynomialLinear (f : ZPoly) (d : PrimeFactorData) : Bool

Kernel-reducible counterpart of checkForPolynomial, replaying the nested certificates through checkFactorCertsLinear.

Equations

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

theorem Hex.PrimeFactorData.checkCertAtFactor_of_linear (d : PrimeFactorData) (degree : Nat) (factor : FpPoly d.p) (cert : Berlekamp.IrreducibilityCertificate) (hp : Nat.Prime d.p) (hcheck : d.checkCertAtFactorLinear degree factor cert = true) : d.checkCertAtFactor degree factor cert = true

checkCertAtFactorLinear implies checkCertAtFactor once the block's prime is genuinely prime: the two differ only in the nested pow-chain replay, which Berlekamp.checkIrreducibilityCertificate_of_linearIncremental identifies with the committed checker.

theorem Hex.PrimeFactorData.checkFactorCerts_of_linear (d : PrimeFactorData) (hp : Nat.Prime d.p) (hcheck : d.checkFactorCertsLinear = true) : d.checkFactorCerts = true

checkFactorCertsLinear implies checkFactorCerts once the block's prime is genuinely prime.

theorem Hex.PrimeFactorData.checkForPolynomial_of_linear (f : ZPoly) (d : PrimeFactorData) (hp : Nat.Prime d.p) (hcheck : checkForPolynomialLinear f d = true) : checkForPolynomial f d = true

checkForPolynomialLinear implies checkForPolynomial once the block's prime is genuinely prime.

def Hex.checkIrreducibleCertLinear (f : ZPoly) (cert : ZPolyIrreducibilityCertificate) : Bool

Kernel-reducible counterpart of checkIrreducibleCert: the same surface checks, with every nested Rabin certificate replayed through the incremental pow-chain checker so decide can reduce a literal certificate without re-running the committed FpPoly.frobeniusXPowMod in the kernel.

Consumers discharge this checker on literal certificate data and cross to the committed checker (hence to checkIrreducibleCert's soundness theorem) via checkIrreducibleCert_of_linear.

Equations

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

theorem Hex.checkIrreducibleCert_of_linear (f : ZPoly) (cert : ZPolyIrreducibilityCertificate) (hprime : ∀ (primeData : PrimeFactorData), primeData ∈ cert.perPrime.toList → Nat.Prime primeData.p) (hcheck : checkIrreducibleCertLinear f cert = true) : checkIrreducibleCert f cert = true

The kernel-reducible integer checker implies the committed one, given that every recorded block prime is genuinely prime. Primality feeds the pow-chain recurrence X^(p^(k+1)) ≡ (X^(p^k))^p (mod f) that identifies the incremental replay with the committed Frobenius routine.