3.5. Certificates🔗

The tactic is a convenience wrapper; the underlying objects are public. A certificate is plain data, and the checker is one structural Boolean function, so certificates can be built by hand, stored, or produced by an external tool and replayed later. Each Pocklington factor list must be in strictly ascending order of the child certificates' subjects:

inductive type

Hex.Nat.PrimeCert : Type
Hex.Nat.PrimeCert : Type

A primality certificate. One inductive rather than two mutually recursive declarations, because a structure referring forward to PrimeCert while PrimeCert refers back to it does not elaborate.

Each factor entry is a base a, an exponent e (stored off by one, so the exponent e + 1 is positive by construction), and the child certificate for a prime q, read off as the child's subject. Factor lists in both Pocklington constructors must be in strictly ascending child-subject order for the checker to accept them.

Constructors

Hex.Nat.PrimeCert.small (n : ℕ) : Hex.Nat.PrimeCert

n is an entry of the stored table.

Hex.Nat.PrimeCert.pock (n : ℕ)
  (factors : List (ℕ × ℕ × Hex.Nat.PrimeCert)) :
  Hex.Nat.PrimeCert

Pocklington: factors partially factors n - 1 past its square root.

Hex.Nat.PrimeCert.pock3 (n r s w : ℕ)
  (factors : List (ℕ × ℕ × Hex.Nat.PrimeCert)) :
  Hex.Nat.PrimeCert

The cube-root Brillhart-Lehmer-Selfridge variant, with the cofactor decomposition R = 2 F s + r and the integer-square-root witness w for the discriminant test (Nat.sqrt is well-founded recursion and does not kernel-reduce, so the checker verifies w instead of computing a root).

def

Hex.Nat.checkPrime : Hex.Nat.PrimeCert → Bool
Hex.Nat.checkPrime :
  Hex.Nat.PrimeCert → Bool

Accept or reject a primality certificate. Pocklington factor lists are accepted only in strictly ascending child-subject order. Structurally recursive and fully @[expose]d, so acceptance replays by kernel reduction alone.

def certM31 : Hex.Nat.PrimeCert :=
  .pock 2147483647
    [(1745337962, 0, .small 2), (1371693800, 1, .small 3),
     (1615909500, 0, .small 7), (447824900, 0, .small 11),
     (505209180, 0, .small 31), (1783259301, 0, .small 151),
     (904659249, 0, .small 331)]

theorem certM31_replays :
    Hex.Nat.checkPrime certM31 = true := by⊢ Hex.Nat.checkPrime certM31 = true
  decide +kernelAll goals completed! 🐙

Soundness turns a successful replay into primality of the certificate's subject; the tactic emits exactly this composition:

theorem

Hex.Nat.prime_of_checkPrimeAt {n : ℕ} {c : Hex.Nat.PrimeCert}
  (h : (c.subject == n && Hex.Nat.checkPrime c) = true) :
  Hex.Nat.Prime n
Hex.Nat.prime_of_checkPrimeAt {n : ℕ}
  {c : Hex.Nat.PrimeCert}
  (h :
    (c.subject == n &&
        Hex.Nat.checkPrime c) =
      true) :
  Hex.Nat.Prime n

Single-Bool-slot wrapper for the tactic reifier: the kernel verifies the subject match and the certificate replay in one reduction.

The certificate search itself is available as a runtime function returning a Hex.Nat.CheckedPrimeCert, a certificate bundled with the proof that it is about the requested number:

def

Hex.Nat.primeCert? (n : ℕ) (r : Hex.Rand) (fuel : ℕ) :
  Except Hex.Nat.PrimeCertFailure
    (Hex.Nat.CheckedPrimeCert n × Hex.Rand)
Hex.Nat.primeCert? (n : ℕ) (r : Hex.Rand)
  (fuel : ℕ) :
  Except Hex.Nat.PrimeCertFailure
    (Hex.Nat.CheckedPrimeCert n ×
      Hex.Rand)

Bounded certificate search. A success is a CheckedPrimeCert, so a certificate for one number can never answer a request about another; a .composite failure is a verdict (see primeCert?_composite); an .exhausted failure makes no claim and carries the advanced state.

The search factors n - 1 with trial division against the table followed by Brent's variant of Pollard rho; the rho primitive is public, reused by hex-int-factor, and validates every factor it returns:

def

Hex.Nat.rhoFactor? (n : ℕ) (r : Hex.Rand) (fuel : ℕ) :
  Except Hex.Nat.RhoFailure (ℕ × Hex.Rand)
Hex.Nat.rhoFactor? (n : ℕ) (r : Hex.Rand)
  (fuel : ℕ) :
  Except Hex.Nat.RhoFailure (ℕ × Hex.Rand)

A dynamically validated proper-factor candidate by batched Brent rho. fuel bounds restart attempts. Each restart draws a fresh polynomial and starting point through bounded unbiased sampling, accumulates up to 32 differences per gcd, and replays a whole-modulus batch difference by difference. Its cycle budget is scaled to n^(1/4) and capped at 2^22 (see rhoInnerFuel), so exhaustion arrives rather than hangs when the smallest factor is out of rho's reach. Every success is validated (1 < d < n and d ∣ n) before it is returned, so randomness and fuel affect only whether a factor is found.

theorem

Hex.Nat.rhoFactor?_spec {n d : ℕ} {r r' : Hex.Rand} {fuel : ℕ}
  (h : Hex.Nat.rhoFactor? n r fuel = Except.ok (d, r')) :
  1 < d ∧ d < n ∧ d ∣ n
Hex.Nat.rhoFactor?_spec {n d : ℕ}
  {r r' : Hex.Rand} {fuel : ℕ}
  (h :
    Hex.Nat.rhoFactor? n r fuel =
      Except.ok (d, r')) :
  1 < d ∧ d < n ∧ d ∣ n

The one theorem about the rho primitive: a success is a validated proper factor.