35.5. HexIntFactor: certified integer factorization🔗

35.5.1. Introduction🔗

HexIntFactor factors natural numbers and turns the result into divisor, square-decomposition, multiplicative-order, and primitive-root data. Search is an explicitly bounded, untrusted producer. Its results become theorem inputs only after a small Boolean checker has replayed every prime certificate and the complete prime-power product.

The executable library is Mathlib-free. It depends on HexPrimality for kernel-replayable primality certificates and modular-order infrastructure, and on HexArith and HexBasic for bounded arithmetic and explicit random state. The companion HexIntFactorMathlib proves correspondence with Mathlib's factorization, divisor, squarefree, and ZMod order APIs.

35.5.2. Complete certificates🔗

A Hex.Nat.PrimePower stores an exponent and a HexPrimality certificate. Its base is the subject of that certificate, so the two cannot disagree. A Hex.Nat.Factorization is raw data: its subject and factor list are trusted only after replay.

def

Hex.Nat.PrimePower.prime (e : Hex.Nat.PrimePower) : ℕ
Hex.Nat.PrimePower.prime
  (e : Hex.Nat.PrimePower) : ℕ

The base of a prime-power entry.

def

Hex.Nat.checkFactorization (F : Hex.Nat.Factorization) : Bool
Hex.Nat.checkFactorization
  (F : Hex.Nat.Factorization) : Bool

Accept or reject a complete factorization certificate.

Hex.Nat.CheckedFactorization ties accepted raw data to the subject requested by its caller. The checker requires a positive subject, positive exponents, strictly ascending prime bases, successful primality replay, and an exact product. Product accumulation is bounded by the claimed subject, so an attacker-chosen exponent cannot first construct an arbitrarily large power.

The checked facts are exposed as characterizing theorems rather than requiring callers to unfold the checker:

theorem

Hex.Nat.checkFactorization_prod {F : Hex.Nat.Factorization}
  (h : Hex.Nat.checkFactorization F = true) :
  (List.map (fun e => e.prime ^ e.exponent) F.factors).prod = F.subject
Hex.Nat.checkFactorization_prod
  {F : Hex.Nat.Factorization}
  (h :
    Hex.Nat.checkFactorization F = true) :
  (List.map
        (fun e => e.prime ^ e.exponent)
        F.factors).prod =
    F.subject

The checked prime powers multiply to the claimed subject.

theorem

Hex.Nat.checkFactorization_prime {F : Hex.Nat.Factorization}
  (h : Hex.Nat.checkFactorization F = true) (e : Hex.Nat.PrimePower) :
  e ∈ F.factors → Hex.Nat.Prime e.prime
Hex.Nat.checkFactorization_prime
  {F : Hex.Nat.Factorization}
  (h :
    Hex.Nat.checkFactorization F = true)
  (e : Hex.Nat.PrimePower) :
  e ∈ F.factors → Hex.Nat.Prime e.prime

Every listed base is prime.

theorem

Hex.Nat.checkFactorization_primeSupport {F : Hex.Nat.Factorization}
  (h : Hex.Nat.checkFactorization F = true) {q : ℕ}
  (hq : Hex.Nat.Prime q) : q ∣ F.subject ↔ ∃ e ∈ F.factors, e.prime = q
Hex.Nat.checkFactorization_primeSupport
  {F : Hex.Nat.Factorization}
  (h :
    Hex.Nat.checkFactorization F = true)
  {q : ℕ} (hq : Hex.Nat.Prime q) :
  q ∣ F.subject ↔
    ∃ e ∈ F.factors, e.prime = q

The listed bases are exactly the prime support of the subject.

theorem

Hex.Nat.checkFactorization_multiplicity {F : Hex.Nat.Factorization}
  (h : Hex.Nat.checkFactorization F = true) {e : Hex.Nat.PrimePower}
  (he : e ∈ F.factors) {k : ℕ} :
  e.prime ^ k ∣ F.subject ↔ k ≤ e.exponent
Hex.Nat.checkFactorization_multiplicity
  {F : Hex.Nat.Factorization}
  (h :
    Hex.Nat.checkFactorization F = true)
  {e : Hex.Nat.PrimePower}
  (he : e ∈ F.factors) {k : ℕ} :
  e.prime ^ k ∣ F.subject ↔ k ≤ e.exponent

A listed prime power occurs with exactly its claimed multiplicity.

The support theorem is complete because the checker proves both the product identity and primality of every listed base. Strict ordering additionally makes the representation canonical and makes each recorded exponent the exact multiplicity.

35.5.3. Checked arithmetic from a factorization🔗

Once a factorization is checked, divisor enumeration and the usual arithmetic functions require no further search. Divisors are returned in ascending order; the count and generalized divisor sum use prime-power product formulas rather than enumerating the entire list.

def

Hex.Nat.divisors {n : ℕ} (F : Hex.Nat.CheckedFactorization n) : Array ℕ
Hex.Nat.divisors {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) :
  Array ℕ

Positive divisors, in ascending order.

def

Hex.Nat.numDivisors {n : ℕ} (F : Hex.Nat.CheckedFactorization n) : ℕ
Hex.Nat.numDivisors {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) : ℕ

Number of positive divisors, τ(n) = ∏ (eᵢ + 1).

def

Hex.Nat.sigma {n : ℕ} (F : Hex.Nat.CheckedFactorization n) (k : ℕ) : ℕ
Hex.Nat.sigma {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n)
  (k : ℕ) : ℕ

Generalized divisor sum σ_k.

def

Hex.Nat.totient {n : ℕ} (F : Hex.Nat.CheckedFactorization n) : ℕ
Hex.Nat.totient {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) : ℕ

Euler's totient from a checked prime-power decomposition.

def

Hex.Nat.radical {n : ℕ} (F : Hex.Nat.CheckedFactorization n) : ℕ
Hex.Nat.radical {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) : ℕ

Product of the distinct prime divisors.

The square decomposition writes the subject as a squarefree factor times the square of a greatest possible divisor.

def

Hex.Nat.squarefreePart {n : ℕ} (F : Hex.Nat.CheckedFactorization n) : ℕ
Hex.Nat.squarefreePart {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) : ℕ

Squarefree part, computed from the odd certified multiplicities.

def

Hex.Nat.squareDivisor {n : ℕ} (F : Hex.Nat.CheckedFactorization n) : ℕ
Hex.Nat.squareDivisor {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) : ℕ

Largest square-divisor root, computed from certified multiplicities.

theorem

Hex.Nat.squarefreePart_mul_square {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) :
  Hex.Nat.squarefreePart F * Hex.Nat.squareDivisor F ^ 2 = n
Hex.Nat.squarefreePart_mul_square {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) :
  Hex.Nat.squarefreePart F *
      Hex.Nat.squareDivisor F ^ 2 =
    n

Canonical squarefree-times-square decomposition.

theorem

Hex.Nat.squareDivisor_spec {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) :
  Hex.Nat.squareDivisor F ^ 2 ∣ n ∧
    ∀ (d : ℕ), d ^ 2 ∣ n → d ∣ Hex.Nat.squareDivisor F
Hex.Nat.squareDivisor_spec {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) :
  Hex.Nat.squareDivisor F ^ 2 ∣ n ∧
    ∀ (d : ℕ),
      d ^ 2 ∣ n →
        d ∣ Hex.Nat.squareDivisor F

squareDivisor is the largest square divisor root.

35.5.4. Worked example🔗

The following block is elaborated with the manual. The certificate for 12 = 2² · 3 uses the small-prime certificates supplied by HexPrimality; ordinary kernel reduction checks the factorization before any arithmetic consumer can use it.

open Hex Hex.Nat

namespace HexIntFactorChapter

set_option maxRecDepth 100000

def twelve : CheckedFactorization 12 :=
  ⟨⟨12, [⟨2, .small 2⟩, ⟨1, .small 3⟩]⟩,
    rfl, by⊢ checkFactorization
    { subject := 12,
      factors := [{ exponent := 2, cert := PrimeCert.small 2 }, { exponent := 1, cert := PrimeCert.small 3 }] } =
  true decideAll goals completed! 🐙⟩

#guard checkFactorization twelve.raw
#guard divisors twelve == #[1, 2, 3, 4, 6, 12]
#guard sigma twelve 1 == 28
#guard totient twelve == 4
#guard radical twelve == 6
#guard squarefreePart twelve == 3
#guard squareDivisor twelve == 2

end HexIntFactorChapter

35.5.5. Search, fuel, and failure🔗

def

Hex.Nat.factor? (n : ℕ) (r : Hex.Rand)
  (fuel : ℕ := Hex.Nat.defaultFuel n) :
  Except Hex.Nat.FactorFailure
    (Hex.Nat.CheckedFactorization n × Hex.Rand)
Hex.Nat.factor? (n : ℕ) (r : Hex.Rand)
  (fuel : ℕ := Hex.Nat.defaultFuel n) :
  Except Hex.Nat.FactorFailure
    (Hex.Nat.CheckedFactorization n ×
      Hex.Rand)

Complete factorization when the checked partial residual is 1.

factor? first applies structural reductions and table trial division, then uses primality search, Brent rho, Pollard p − 1, and stage-one ECM as the input requires. Its Hex.Rand argument and returned random state make every random draw explicit. The default fuel scales with bit length but does not claim to make a partial search total.

def

Hex.Nat.defaultFuel (n : ℕ) : ℕ
Hex.Nat.defaultFuel (n : ℕ) : ℕ

Default search budget, scaled by input bit length.

The Hex.Nat.FactorStop cases distinguish zero, ordinary exhaustion, and rejection of a producer's output by a checker. A Hex.Nat.FactorFailure retains exact attempt accounting, the advanced random state, and either the last checked partial snapshot or the rejected raw candidate. This makes retry policy observable without treating exhaustion as a false mathematical result.

def

Hex.Nat.factorPartial? (n : ℕ) (r : Hex.Rand)
  (fuel : ℕ := Hex.Nat.defaultFuel n) :
  Except Hex.Nat.FactorFailure
    (Hex.Nat.CheckedPartialFactorization n × Hex.Rand)
Hex.Nat.factorPartial? (n : ℕ)
  (r : Hex.Rand)
  (fuel : ℕ := Hex.Nat.defaultFuel n) :
  Except Hex.Nat.FactorFailure
    (Hex.Nat.CheckedPartialFactorization
        n ×
      Hex.Rand)

Return checked partial data for positive input, or expose a rejected internal candidate.

def

Hex.Nat.checkPartial (F : Hex.Nat.PartialFactorization) : Bool
Hex.Nat.checkPartial
  (F : Hex.Nat.PartialFactorization) :
  Bool

Accept or reject partial factorization data.

theorem

Hex.Nat.checkPartial_prod {F : Hex.Nat.PartialFactorization}
  (h : Hex.Nat.checkPartial F = true) :
  (List.map (fun e => e.prime ^ e.exponent) F.factors).prod *
      F.residual =
    F.subject
Hex.Nat.checkPartial_prod
  {F : Hex.Nat.PartialFactorization}
  (h : Hex.Nat.checkPartial F = true) :
  (List.map
          (fun e => e.prime ^ e.exponent)
          F.factors).prod *
      F.residual =
    F.subject

Accepted partial data reconstructs its subject exactly.

A partial factorization certifies every listed prime power and the exact residual product, but makes no primality claim about the residual. Residual one promotes directly to a complete certificate without replaying the entire checker:

theorem

Hex.Nat.checkFactorization_of_checkPartial
  {F : Hex.Nat.PartialFactorization} (h : Hex.Nat.checkPartial F = true)
  (hr : F.residual = 1) :
  Hex.Nat.checkFactorization
      { subject := F.subject, factors := F.factors } =
    true
Hex.Nat.checkFactorization_of_checkPartial
  {F : Hex.Nat.PartialFactorization}
  (h : Hex.Nat.checkPartial F = true)
  (hr : F.residual = 1) :
  Hex.Nat.checkFactorization
      { subject := F.subject,
        factors := F.factors } =
    true

A checked partial factorization with residual one is already a complete factorization certificate; no second checker replay is needed.

Specialized entry points expose the split routes for callers that need route control or diagnostics. factorPower? adds a checked cyclotomic pre-split for numbers of the form b ^ n − 1 or b ^ n + 1; failed subproblems may fall back to generic search, while checker rejection is propagated.

35.5.6. Orders, primitive roots, and Carmichael exponents🔗

An Hex.Nat.OrderCert claims that a residue has a specified least positive order. Its factorization field must be a complete checked factorization of that order. The checker verifies the full power is one and that removing each distinct prime divisor from the exponent is not.

def

Hex.Nat.checkOrder (c : Hex.Nat.OrderCert) : Bool
Hex.Nat.checkOrder
  (c : Hex.Nat.OrderCert) : Bool

Replay an exact multiplicative-order certificate.

theorem

Hex.Nat.checkOrder_iff {c : Hex.Nat.OrderCert} :
  Hex.Nat.checkOrder c = true ↔
    1 < c.modulus ∧
      0 < c.order ∧
        c.orderFac.subject = c.order ∧
          Hex.Nat.checkFactorization c.orderFac = true ∧
            HexArith.powModNat c.base c.order c.modulus =
                1 % c.modulus ∧
              ∀ e ∈ c.orderFac.factors,
                HexArith.powModNat c.base (c.order / e.prime)
                    c.modulus ≠
                  1 % c.modulus
Hex.Nat.checkOrder_iff
  {c : Hex.Nat.OrderCert} :
  Hex.Nat.checkOrder c = true ↔
    1 < c.modulus ∧
      0 < c.order ∧
        c.orderFac.subject = c.order ∧
          Hex.Nat.checkFactorization
                c.orderFac =
              true ∧
            HexArith.powModNat c.base
                  c.order c.modulus =
                1 % c.modulus ∧
              ∀ e ∈ c.orderFac.factors,
                HexArith.powModNat c.base
                    (c.order / e.prime)
                    c.modulus ≠
                  1 % c.modulus

Characterisation of every condition replayed by the order checker.

theorem

Hex.Nat.order_eq_of_checkOrder {c : Hex.Nat.OrderCert}
  (h : Hex.Nat.checkOrder c = true) :
  Hex.Nat.orderOf c.base c.modulus = c.order
Hex.Nat.order_eq_of_checkOrder
  {c : Hex.Nat.OrderCert}
  (h : Hex.Nat.checkOrder c = true) :
  Hex.Nat.orderOf c.base c.modulus =
    c.order

Accepted order data identifies the local orderOf.

For a certified prime p, Hex.Nat.isPrimitiveRoot specializes this criterion to order p − 1; Hex.Nat.primitiveRoot? performs a fuel-bounded ascending search and returns the checked order certificate with the generator.

theorem

Hex.Nat.isPrimitiveRoot_iff {p : ℕ} {pc : Hex.Nat.CheckedPrimeCert p}
  {F : Hex.Nat.CheckedFactorization (p - 1)} {g : ℕ} :
  Hex.Nat.isPrimitiveRoot pc F g = true ↔ Hex.Nat.orderOf g p = p - 1
Hex.Nat.isPrimitiveRoot_iff {p : ℕ}
  {pc : Hex.Nat.CheckedPrimeCert p}
  {F :
    Hex.Nat.CheckedFactorization (p - 1)}
  {g : ℕ} :
  Hex.Nat.isPrimitiveRoot pc F g = true ↔
    Hex.Nat.orderOf g p = p - 1

The checker criterion is exact.

theorem

Hex.Nat.primitiveRoot?_spec {p : ℕ} {pc : Hex.Nat.CheckedPrimeCert p}
  {F : Hex.Nat.CheckedFactorization (p - 1)} {fuel g : ℕ}
  {c : Hex.Nat.CheckedOrderCert}
  (h : Hex.Nat.primitiveRoot? pc F fuel = some (g, c)) :
  c.raw.base = g ∧ c.raw.modulus = p ∧ c.raw.order = p - 1
Hex.Nat.primitiveRoot?_spec {p : ℕ}
  {pc : Hex.Nat.CheckedPrimeCert p}
  {F :
    Hex.Nat.CheckedFactorization (p - 1)}
  {fuel g : ℕ}
  {c : Hex.Nat.CheckedOrderCert}
  (h :
    Hex.Nat.primitiveRoot? pc F fuel =
      some (g, c)) :
  c.raw.base = g ∧
    c.raw.modulus = p ∧
      c.raw.order = p - 1

A successful primitive-root search returns an order certificate for the requested prime and full group order.

The Carmichael exponent is computed by taking the least common multiple of the Carmichael value of each certified prime power. Its correctness is stated both as a power law and as the divisibility bound on every multiplicative order.

def

Hex.Nat.carmichael {n : ℕ} (F : Hex.Nat.CheckedFactorization n) : ℕ
Hex.Nat.carmichael {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) : ℕ

Carmichael function from a checked complete factorization.

theorem

Hex.Nat.pow_carmichael {n : ℕ} (F : Hex.Nat.CheckedFactorization n)
  (a : ℕ) (ha : a.Coprime n) : a ^ Hex.Nat.carmichael F % n = 1 % n
Hex.Nat.pow_carmichael {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n)
  (a : ℕ) (ha : a.Coprime n) :
  a ^ Hex.Nat.carmichael F % n = 1 % n

Carmichael's exponent sends every unit to one.

theorem

Hex.Nat.orderOf_dvd_carmichael {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) (a : ℕ) (hn : 1 < n)
  (ha : a.Coprime n) : Hex.Nat.orderOf a n ∣ Hex.Nat.carmichael F
Hex.Nat.orderOf_dvd_carmichael {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n)
  (a : ℕ) (hn : 1 < n)
  (ha : a.Coprime n) :
  Hex.Nat.orderOf a n ∣
    Hex.Nat.carmichael F

Every multiplicative order divides the Carmichael exponent.

35.5.7. The Mathlib correspondence🔗

HexIntFactorMathlib is correspondence-only: it neither searches for factors nor replays certificates. It identifies values already computed and checked by HexIntFactor with Mathlib's canonical definitions.

theorem

Hex.Nat.CheckedFactorization.factorization_eq {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) (p : ℕ) :
  n.factorization p =
    (List.find? (fun e => e.prime == p) F.raw.factors).elim 0 fun x =>
      x.exponent
Hex.Nat.CheckedFactorization.factorization_eq
  {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n)
  (p : ℕ) :
  n.factorization p =
    (List.find? (fun e => e.prime == p)
          F.raw.factors).elim
      0 fun x => x.exponent

Pointwise factorization correspondence for checked data.

theorem

Hex.Nat.CheckedFactorization.primeFactorsList_eq {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) :
  n.primeFactorsList =
    List.flatMap (fun e => List.replicate e.exponent e.prime)
      F.raw.factors
Hex.Nat.CheckedFactorization.primeFactorsList_eq
  {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) :
  n.primeFactorsList =
    List.flatMap
      (fun e =>
        List.replicate e.exponent e.prime)
      F.raw.factors

Canonical factor-list correspondence for checked data.

theorem

Hex.Nat.divisors_eq {n : ℕ} (F : Hex.Nat.CheckedFactorization n) :
  (Hex.Nat.divisors F).toList.toFinset = n.divisors
Hex.Nat.divisors_eq {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) :
  (Hex.Nat.divisors F).toList.toFinset =
    n.divisors

The checked divisor enumeration is Mathlib's divisor finset.

theorem

Hex.Nat.totient_eq {n : ℕ} (F : Hex.Nat.CheckedFactorization n) :
  Hex.Nat.totient F = n.totient
Hex.Nat.totient_eq {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) :
  Hex.Nat.totient F = n.totient

The checked totient agrees with Mathlib's Euler totient.

theorem

Hex.Nat.isSquarefree_iff_squarefree {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) :
  Hex.Nat.isSquarefree F = true ↔ Squarefree n
Hex.Nat.isSquarefree_iff_squarefree
  {n : ℕ}
  (F : Hex.Nat.CheckedFactorization n) :
  Hex.Nat.isSquarefree F = true ↔
    Squarefree n

The checked squarefree decision agrees with Mathlib's squarefree predicate.

For modular orders, the bridge first identifies the Mathlib-free natural order with the order of the corresponding unit in ZMod n, then specializes that equality to accepted order certificates.

theorem

Hex.Nat.orderOf_unitOfCoprime {a n : ℕ} (hn : 1 < n)
  (ha : a.Coprime n) :
  orderOf (ZMod.unitOfCoprime a ha) = Hex.Nat.orderOf a n
Hex.Nat.orderOf_unitOfCoprime {a n : ℕ}
  (hn : 1 < n) (ha : a.Coprime n) :
  orderOf (ZMod.unitOfCoprime a ha) =
    Hex.Nat.orderOf a n

The Mathlib order of a residue-class unit agrees with the Mathlib-free natural order.

theorem

Hex.Nat.orderOf_eq {c : Hex.Nat.OrderCert}
  (h : Hex.Nat.checkOrder c = true) :
  orderOf (ZMod.unitOfCoprime c.base ⋯) = c.order
Hex.Nat.orderOf_eq {c : Hex.Nat.OrderCert}
  (h : Hex.Nat.checkOrder c = true) :
  orderOf (ZMod.unitOfCoprime c.base ⋯) =
    c.order

A checked natural order is the order of the corresponding Mathlib unit.

35.5.8. Cross-references🔗

HexPrimality supplies the primality certificates, order computation, and shared rho and p − 1 primitives.
HexArith supplies bounded powers, modular arithmetic, primality foundations, and exact gcd infrastructure.
HexConway can consume complete prime support for multiplicative-group orders when its committed table grows beyond hand-maintained factorizations.