structure Hex.PrimeChoiceData : Type

Data produced by modular prime selection: the selected prime, the image of the input polynomial over that prime field, and its modular factors.

• p : Nat

  The selected prime modulus.

• bounds : ZMod64.Bounds self.p

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

• fModP : FpPoly self.p

  The input polynomial reduced modulo p.

• factorsModP : Array (FpPoly self.p)

  Its monic irreducible factors over the prime field.

@[instance_reducible]

instance Hex.instInhabitedPrimeChoiceData : Inhabited PrimeChoiceData

Equations

• Hex.instInhabitedPrimeChoiceData = { default := { p := 3, bounds := Hex.bounds_three, fModP := 0, factorsModP := #[] } }

structure Hex.LiftData : Type

Data produced by Hensel lifting and consumed by integer recombination: the prime, the requested lift precision, and the lifted integer factors.

• p : Nat

  The prime underlying the Hensel modulus.

• p_pos : 0 < self.p

  Positivity of the prime, retained for arithmetic bounds.

• k : Nat

  The exponent in the lifting modulus p ^ k.

• liftedFactors : Array ZPoly

  The modular factors lifted to integer polynomials modulo p ^ k.

structure Hex.FactorNormalizationData : Type

Executable normalization data for the public integer factorization API.

The public input is first split into its integer content, primitive part, initial X power, and primitive square-free part. The Berlekamp-Zassenhaus prime/lift/factorization computation runs on squareFreeCore; the other fields are reassembled around the resulting factors of the square-free part.

• content : Int

  The signed-independent integer content of the input.

• primitive : ZPoly

  The content-free input with normalized sign.

• xPower : Nat

  The largest exponent of X dividing the primitive input.

• xFreePrimitive : ZPoly

  The primitive input after removing its initial power of X.

• squareFreeCore : ZPoly

  The primitive product of the distinct nonzero irreducible factors.

• repeatedPart : ZPoly

  The primitive repeated-factor contribution.

structure Hex.ZPoly.ToMonicData : Type

Executable data for the integer scaling transform that sends a primitive polynomial with positive leading coefficient to a monic integer polynomial with the same roots (scaled by the leading coefficient).

If core has degree n and leading coefficient c, monic is the coefficientwise integer polynomial c^(n-1) * core (X / c): lower coefficient a_i becomes a_i * c^(n-1-i) and the leading coefficient is normalised to 1.

• core : ZPoly

  The primitive positive-leading polynomial being transformed.

• leadingCoeff : Int

  The leading coefficient of core.

• degree : Nat

  The degree of core.

• monic : ZPoly

  The integral monic polynomial obtained by the scaling transform.

def Hex.ZPoly.ToMonicData.transformedCoeffs (core : ZPoly) (degree : Nat) : Array Int

Coefficients of the degree-dependent transformed polynomial.

Equations

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

def Hex.ZPoly.ToMonicData.transformedCore (core : ZPoly) (degree : Nat) : ZPoly

The degree-dependent transform used for repeated-factor recovery.

Equations

• Hex.ZPoly.ToMonicData.transformedCore core degree = { coeffs := Hex.ZPoly.ToMonicData.transformedCoeffs core degree, normalized := ⋯ }

@[simp]

theorem Hex.ZPoly.ToMonicData.transformedCoeffs_size (core : ZPoly) (degree : Nat) : (transformedCoeffs core degree).size = degree + 1

The transformed coefficient array has one entry per degree up to and including the prescribed top degree.

theorem Hex.ZPoly.ToMonicData.transformedCoeffs_getD_top (core : ZPoly) (degree : Nat) : (transformedCoeffs core degree).getD degree 0 = 1

The transformed coefficient array's top entry is one. Not @[simp]: the getD left-hand side is not simp-normal (simp rewrites it to a getElem access through transformedCoeffs_size); transformedCore_coeff_top applies it explicitly.

@[simp]

theorem Hex.ZPoly.ToMonicData.transformedCore_size (core : ZPoly) (degree : Nat) : DensePoly.size (transformedCore core degree) = degree + 1

The transformed polynomial stores degree + 1 coefficients.

theorem Hex.ZPoly.ToMonicData.transformedCore_coeff_top (core : ZPoly) (degree : Nat) : DensePoly.coeff (transformedCore core degree) degree = 1

The coefficient in the prescribed top degree of the transformed polynomial is one.

theorem Hex.ZPoly.ToMonicData.transformedCore_monic (core : ZPoly) (degree : Nat) : DensePoly.Monic (transformedCore core degree)

The transformed polynomial is monic in the prescribed degree.

@[simp]

theorem Hex.ZPoly.ToMonicData.transformedCore_degree_getD (core : ZPoly) (degree : Nat) : DensePoly.natDegree (transformedCore core degree) = degree

The transformed polynomial's degree is the prescribed degree.

def Hex.ZPoly.toMonic (core : ZPoly) : ToMonicData

Build the ToMonicData packet for a square-free part by the integer scaling transform.

Equations

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

@[simp]

theorem Hex.ZPoly.toMonic_core (core : ZPoly) : core.toMonic.core = core

The packet records its source polynomial unchanged.

@[simp]

theorem Hex.ZPoly.toMonic_leadingCoeff (core : ZPoly) : core.toMonic.leadingCoeff = DensePoly.leadingCoeff core

The packet records the source's leading coefficient.

@[simp]

theorem Hex.ZPoly.toMonic_degree (core : ZPoly) : core.toMonic.degree = DensePoly.natDegree core

The packet records the source's degree.

theorem Hex.ZPoly.toMonic_monic_isMonic (core : ZPoly) : DensePoly.Monic core.toMonic.monic

The polynomial stored by toMonic is monic, including the degenerate constant branches.

theorem Hex.ZPoly.toMonic_monic_isMonic_of_pos_degree (core : ZPoly) (_hpos_lc : 0 < DensePoly.leadingCoeff core) (_hdegree : 0 < core.toMonic.degree) : DensePoly.Monic core.toMonic.monic

The monic field of toMonic core is monic once the source has positive degree.

theorem Hex.ZPoly.toMonic_monic_degree_eq_of_pos_degree (core : ZPoly) (_hpos_lc : 0 < DensePoly.leadingCoeff core) (_hdegree : 0 < core.toMonic.degree) : DensePoly.natDegree core.toMonic.monic = core.toMonic.degree

The monic field preserves the recorded degree in nonconstant cases.

theorem Hex.ZPoly.toMonic_monic_eq_core_of_leadingCoeff_eq_one (core : ZPoly) (hmonic : DensePoly.leadingCoeff core = 1) : core.toMonic.monic = core

Applying toMonic to an already-monic polynomial leaves its monic field equal to the original.

structure Hex.Factorization : Type

Public factorization result for an integer polynomial Hex.ZPoly.

The scalar carries the input's signed content: for nonzero inputs this is sign(lc f) * ZPoly.content f, while zero inputs use scalar 0. Polynomial factors are primitive, positive-leading-coefficient factors stored with explicit multiplicities; factor order remains operational, with the mathematical contract expressed by multiplying the scalar and stored factors.

• scalar : Int

  Signed scalar absorbing both sign and integer content.

• factors : Array (ZPoly × Nat)

  Polynomial factors paired with explicit positive multiplicities.

def Hex.instDecidableEqFactorization.decEq (x✝ x✝¹ : Factorization) : Decidable (x✝ = x✝¹)

Equations

• Hex.instDecidableEqFactorization.decEq { scalar := a, factors := a_1 } { scalar := b, factors := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Hex.instDecidableEqFactorization : DecidableEq Factorization

Equations

• Hex.instDecidableEqFactorization = Hex.instDecidableEqFactorization.decEq

def Hex.Factorization.polyPow (f : ZPoly) : Nat → ZPoly

Natural powers of an integer polynomial.

Equations

• Hex.Factorization.polyPow f 0 = 1
• Hex.Factorization.polyPow f n.succ = Hex.Factorization.polyPow f n * f

def Hex.Factorization.factorPower (f : ZPoly) (n : Nat) : ZPoly

Public wrapper for the polynomial power used by Factorization.product.

Equations

• Hex.Factorization.factorPower f n = Hex.Factorization.polyPow f n

@[simp]

theorem Hex.Factorization.factorPower_zero (f : ZPoly) : factorPower f 0 = 1

The zeroth factor power is one.

@[simp]

theorem Hex.Factorization.factorPower_succ (f : ZPoly) (n : Nat) : factorPower f (n + 1) = factorPower f n * f

Each successive factor power multiplies by the factor once more.

def Hex.Factorization.product (φ : Factorization) : ZPoly

Expand multiplicity pairs into the ordered polynomial product.

Equations

• φ.product = Array.foldl (fun (acc : Hex.ZPoly) (factor : Hex.ZPoly × Nat) => acc * Hex.Factorization.polyPow factor.fst factor.snd) (Hex.DensePoly.C φ.scalar) φ.factors

@[simp]

theorem Hex.Factorization.product_mk_empty (scalar : Int) : { scalar := scalar, factors := #[] }.product = DensePoly.C scalar

A factorization with no polynomial factors multiplies to its scalar.

theorem Hex.Factorization.product_eq_foldl_factorPower (φ : Factorization) : φ.product = Array.foldl (fun (acc : ZPoly) (factor : ZPoly × Nat) => acc * factorPower factor.fst factor.snd) (DensePoly.C φ.scalar) φ.factors

Characterize product using the public factorPower wrapper instead of the private recursion used internally.

def Hex.normalizeForFactor (f : ZPoly) : FactorNormalizationData

Compute the normalization data required before the square-free computation.

Equations

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

def Hex.ZPoly.contentPrimitive (f : ZPoly) : Int × ZPoly

Compute an integer polynomial's content and primitive part together. The logical surface is the ordinary pair of operations.

Equations

• f.contentPrimitive = (f.content, f.primitivePart)

def Hex.ZPoly.contentPrimitiveImpl (f : ZPoly) : Int × ZPoly

One-pass runtime implementation of ZPoly.contentPrimitive: compute the coefficient gcd once, then reuse it for both the content and coefficient division.

Equations

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

theorem Hex.ZPoly.contentPrimitive_eq_impl_value (f : ZPoly) : f.contentPrimitive = f.contentPrimitiveImpl

Pointwise agreement between the specification contentPrimitive and its single-pass compiled implementation.

@[csimp]

theorem Hex.ZPoly.contentPrimitive_eq_impl : contentPrimitive = contentPrimitiveImpl

@[csimp] bridge routing compiled contentPrimitive calls to the single-pass implementation.

theorem Hex.prime_499 : Nat.Prime 499

Certified trial prime for the modular square-free fast path. 499 is a cheap fixed choice: it is large enough that a distinct-root input rarely reduces non-square-free at it, but it carries no guarantee (a rationally square-free input whose discriminant is divisible by 499 reduces non-square-free and simply takes the exact fallback -- never a wrong answer).

instance Hex.bounds_499 : ZMod64.Bounds 499

The trial prime 499 fits the word-arithmetic bounds of ZMod64.

def Hex.modularSquareFreeCoreFires (q : ZPoly) : Bool

The prepared-input form of the modular square-free trial.

Equations

• Hex.modularSquareFreeCoreFires q = (!Hex.DensePoly.isZero q && q.leadingCoeffModP 499 != 0 && q.separableModP 499)

def Hex.normalizeForFactorFast (f : ZPoly) : FactorNormalizationData

Fast implementation of normalizeForFactor: a machine-word 𝔽_p square-freeness trial on the primitive x-free square-free part. When it fires (the input is square-free over ℚ) the decomposition is trivial; otherwise it falls back to the exact rational computation, inlined rather than a self-call so the @[csimp] rewrite below does not make the fallback recurse. Proven equal to normalizeForFactor.

Equations

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

@[csimp]

theorem Hex.normalizeForFactor_eq_normalizeForFactorFast : normalizeForFactor = normalizeForFactorFast

@[csimp] bridge routing compiled normalization through the modular square-free fast path; the guard's soundness lemma makes both sides agree.

def Hex.xPowerFactorArray (power : Nat) : Array ZPoly

The factor X with the requested multiplicity, omitted at multiplicity zero.

Equations

• Hex.xPowerFactorArray power = (List.replicate power Hex.ZPoly.X).toArray

def Hex.repeatedPartFactorArray (repeatedPart : ZPoly) : Array ZPoly

The repeated part as a singleton factor array, omitting the unit polynomial.

Equations

• Hex.repeatedPartFactorArray repeatedPart = if repeatedPart = 1 then #[] else #[repeatedPart]

def Hex.signedContentScalar (f : ZPoly) : Int

The signed content carried by the scalar part of a factorization.

Equations

• Hex.signedContentScalar f = if f = 0 then 0 else if Hex.DensePoly.leadingCoeff f < 0 then -f.content else f.content

def Hex.normalizeFactorSign (f : ZPoly) : ZPoly

Normalize a polynomial factor's sign by negating it whenever the leading coefficient is negative. The result has nonnegative leading coefficient and is associated to the input over ℤ.

Equations

• Hex.normalizeFactorSign f = if Hex.DensePoly.leadingCoeff f < 0 then Hex.DensePoly.scale (-1) f else f

def Hex.shouldRecordPolynomialFactor (f : ZPoly) : Bool

A polynomial factor is recorded by the factorization routines only when it is not zero and not a unit (±1). Exposed publicly so that Mathlib-side lemmas can transport the predicate into ¬ IsUnit over Polynomial ℤ.

Equations

• Hex.shouldRecordPolynomialFactor f = (decide (f ≠ 0) && decide (f ≠ 1) && decide (f ≠ Hex.DensePoly.C (-1)))

def Hex.bumpFactorMultiplicity (f : ZPoly) : List (ZPoly × Nat) → List (ZPoly × Nat)

Increase the multiplicity of f, or append it with multiplicity one.

Equations

• Hex.bumpFactorMultiplicity f [] = [(f, 1)]
• Hex.bumpFactorMultiplicity f (entry :: entries) = if entry.fst = f then (entry.fst, entry.snd + 1) :: entries else entry :: Hex.bumpFactorMultiplicity f entries

def Hex.collectFactorMultiplicities (factors : Array ZPoly) : Array (ZPoly × Nat)

Collect equal factors and their multiplicities in first-occurrence order.

Equations

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

def Hex.polynomialNormalizationPrefixFactors (d : FactorNormalizationData) : Array ZPoly

The X-power and repeated-part factors preceding the square-free factors.

Equations

• Hex.polynomialNormalizationPrefixFactors d = Hex.xPowerFactorArray d.xPower ++ Hex.repeatedPartFactorArray d.repeatedPart

def Hex.normalizationPrefixFactors (d : FactorNormalizationData) : Array ZPoly

Factors that come from normalization before the primitive square-free part is factored.

Equations

• Hex.normalizationPrefixFactors d = Hex.contentFactorArray✝ d.content ++ Hex.xPowerFactorArray d.xPower ++ Hex.repeatedPartFactorArray d.repeatedPart

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

Reassemble normalization factors around the factors of the primitive square-free part.

Equations

• Hex.reassembleNormalizedFactors d coreFactors = Hex.normalizationPrefixFactors d ++ coreFactors

def Hex.exactQuotient? (target candidate : ZPoly) : Option ZPoly

Exact-division check on integer polynomials: returns the quotient when quot * candidate = target exactly, and rejects unit candidates so iterated calls cannot loop forever on ±1.

Equations

• Hex.exactQuotient? target candidate = if (Hex.DensePoly.isZero candidate || decide (candidate = 1)) = true then none else target.divExact? candidate

theorem Hex.exactQuotient?_product {target candidate quotient : ZPoly} (hquot : exactQuotient? target candidate = some quotient) : quotient * candidate = target

Successful exact-division extracts a multiplication witness: exactQuotient? target candidate = some quotient implies quotient * candidate = target. Forward companion of exactQuotient?_eq_some_of_mul_eq_monic_of_pos_degree.

def Hex.consumeExactPower (target candidate : ZPoly) : Nat → ZPoly × Nat

Greedy peel of candidate^? out of target via repeated exact division. Returns (residual, multiplicity) with the invariant candidate ^ multiplicity * residual = target. The recursion is bounded by fuel, which the caller chooses based on the source degree.

Equations

• One or more equations did not get rendered due to their size.
• Hex.consumeExactPower target candidate 0 = (target, 0)

def Hex.expandRepeatedPartFactorsAux : List ZPoly → ZPoly → Nat → Array ZPoly × ZPoly

Fold consumeExactPower over a list of candidate factors, accumulating emitted copies and tracking the residual that has not yet been factored. Invariant: polyProduct emitted * residual = initialRepeatedPart.

Equations

• One or more equations did not get rendered due to their size.
• Hex.expandRepeatedPartFactorsAux [] x✝¹ x✝ = (#[], x✝¹)

def Hex.expandRepeatedPartFactorArray (rp : ZPoly) (coreFactors : Array ZPoly) : Array ZPoly × ZPoly

Compute (emitted, residual) where each candidate factor q from coreFactors appears in emitted to the maximum multiplicity such that q^k exactly divides the running repeated-part. The fuel is the source size, which dominates any irreducible's multiplicity in repeatedPart.

Equations

• Hex.expandRepeatedPartFactorArray rp coreFactors = Hex.expandRepeatedPartFactorsAux coreFactors.toList rp (Hex.DensePoly.size rp + 1)