inductive 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.

• small (n : Nat) : PrimeCert

  n is an entry of the stored table.

• pock (n : Nat) (factors : List (Nat × Nat × PrimeCert)) : PrimeCert

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

• pock3 (n r s w : Nat) (factors : List (Nat × Nat × PrimeCert)) : 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).

partial def Hex.Nat.instReprPrimeCert.repr : PrimeCert → Nat → Std.Format

@[instance_reducible]

instance Hex.Nat.instReprPrimeCert : Repr PrimeCert

Equations

• Hex.Nat.instReprPrimeCert = { reprPrec := Hex.Nat.instReprPrimeCert.repr }

def Hex.Nat.PrimeCert.subject : PrimeCert → Nat

The number a certificate is about.

Equations

• (Hex.Nat.PrimeCert.small n).subject = n
• (Hex.Nat.PrimeCert.pock n factors).subject = n
• (Hex.Nat.PrimeCert.pock3 n r s w factors).subject = n

def Hex.Nat.boundedPowMul (bound q : Nat) : Nat → Nat → Option Nat

acc * q ^ e, checking each nonzero multiplication by division before constructing it. A zero accumulator or base returns zero immediately; otherwise the computation aborts as soon as the next product would exceed bound, so an attacker-chosen enormous power is never constructed.

Equations

• Hex.Nat.boundedPowMul bound q x✝ 0 = some x✝
• Hex.Nat.boundedPowMul bound q x✝ e.succ = if x✝ = 0 then some 0 else if q = 0 then some 0 else if x✝ ≤ bound / q then Hex.Nat.boundedPowMul bound q (x✝ * q) e else none

def Hex.Nat.certProduct (bound : Nat) : List (Nat × Nat × PrimeCert) → Option Nat

The factored part F = ∏ qᵢ ^ (eᵢ + 1) of a factor list, aborting as soon as the running product exceeds bound.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Nat.certProduct bound [] = some 1

def Hex.Nat.subjectsAfter (lower : Nat) : List (Nat × Nat × PrimeCert) → Bool

Continue the canonical factor-subject check above a strict lower bound.

Equations

• Hex.Nat.subjectsAfter lower [] = true
• Hex.Nat.subjectsAfter lower ((fst, e, c) :: rest) = (decide (lower < c.subject) && Hex.Nat.subjectsAfter c.subject rest)

def Hex.Nat.subjectsOk (factors : List (Nat × Nat × PrimeCert)) : Bool

Structural check on the factor list: every claimed prime is at least 2, and the claimed primes are in strictly ascending order. The canonical order implies pairwise distinctness with one lower-bound subject comparison per entry.

Equations

• Hex.Nat.subjectsOk factors = Hex.Nat.subjectsAfter 1 factors

def Hex.Nat.checkWitness (n q a : Nat) : Bool

The per-entry witness conditions: Fermat at the base, and the gcd condition at the reduced exponent. The gcd argument is written modularly: the checker only holds the residue x, and (x + n - 1) % n is x - 1 modulo n at every residue, where the literal x - 1 would truncate at x = 0.

Equations

• Hex.Nat.checkWitness n q a = (HexArith.powModNat a (n - 1) n == 1 % n && ((HexArith.powModNat a ((n - 1) / q) n + n - 1) % n).gcd n == 1)

def Hex.Nat.checkPockArith (n : Nat) (factors : List (Nat × Nat × PrimeCert)) : Bool

The arithmetic side of the square-root Pocklington node: n odd and at least 2, canonical strictly ascending factor subjects, F ∣ n - 1 with n < F * F, and every per-entry witness condition. Child certificates are checked separately by checkPrime.

Equations

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

def Hex.Nat.checkPock3Arith (n r s w : Nat) (factors : List (Nat × Nat × PrimeCert)) : Bool

The arithmetic side of the cube-root node: everything the square-root arm verifies except the n < F * F bound, which the Brillhart-Lehmer-Selfridge conditions replace: F even, the cofactor R = (n - 1) / F odd (the weaker form of the classical gcd(F, R) = 1 that the proof uses once F is even), the decomposition R = 2Fs + r with 1 ≤ r < 2F, the cube-root size bound, and the discriminant condition on r² - 8s, with the stored witness w verifying non-squareness by two multiplications. (When r² ≤ 8s the truncated subtraction makes the witness clause w * w < 0 unsatisfiable, so the disjunct is simply never taken; the middle disjunct covers that region.)

Equations

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

def Hex.Nat.checkPrime : 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.

Equations

• Hex.Nat.checkPrime (Hex.Nat.PrimeCert.small n) = Hex.Nat.isTablePrime n
• Hex.Nat.checkPrime (Hex.Nat.PrimeCert.pock n factors) = (Hex.Nat.checkPockArith n factors && Hex.Nat.checkChildren factors)
• Hex.Nat.checkPrime (Hex.Nat.PrimeCert.pock3 n r s w factors) = (Hex.Nat.checkPock3Arith n r s w factors && Hex.Nat.checkChildren factors)

def Hex.Nat.checkChildren : List (Nat × Nat × PrimeCert) → Bool

Accept every child certificate of a factor list.

Equations

• Hex.Nat.checkChildren [] = true
• Hex.Nat.checkChildren ((fst, e, c) :: rest) = (Hex.Nat.checkPrime c && Hex.Nat.checkChildren rest)

theorem Hex.Nat.boundedPowMul_eq {bound q : Nat} (e acc r : Nat) : boundedPowMul bound q acc e = some r → r = acc * q ^ e

On success, the bounded accumulator computes the ordinary product.

theorem Hex.Nat.boundedPowMul_le {bound q acc e r : Nat} (hacc : acc ≤ bound) (h : boundedPowMul bound q acc e = some r) : r ≤ bound

A successful bounded multiplication preserves the accumulator bound. The incoming bound is needed only for the zero-exponent case; every positive step establishes it before constructing the next accumulator.

theorem Hex.Nat.certProduct_le {bound : Nat} (hbound : 1 ≤ bound) (l : List (Nat × Nat × PrimeCert)) (F : Nat) : certProduct bound l = some F → F ≤ bound

A successful certificate product is bounded when its initial accumulator 1 is bounded.

theorem Hex.Nat.prime_of_pocklington {n : Nat} {factors : List (Nat × Nat × PrimeCert)} (hcheck : checkPockArith n factors = true) (hprimes : ∀ (x : Nat × Nat × PrimeCert), x ∈ factors → Prime x.snd.snd.subject) : Prime n

Pocklington replay with separately proved child primes. This permits a certificate generator to share child proofs across many parent certificates. Only each child's subject is used; checkPockArith validates the parent arithmetic, factor ordering and witnesses. The PrimeCert payload is ignored apart from its subject: a .small q here is not checked against the table. The separate hprimes hypothesis must prove that q is prime.

theorem Hex.Nat.prime_of_checkPrime {c : PrimeCert} (h : checkPrime c = true) : Prime c.subject

Checker soundness: an accepted certificate proves its subject prime. The whole conclusion; no certificate-existence, checker-completeness, or search-completeness claim accompanies it.

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

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

structure Hex.Nat.CheckedPrimeCert (n : Nat) : Type

An accepted certificate tied to the number requested by its caller. The subject equality is load-bearing: checkPrime proves primality of c.subject, not of an unrelated input that happened to request c.

• raw : PrimeCert

  The certificate itself.

• subject_eq : self.raw.subject = n

  The certificate is about the requested number.

• valid : checkPrime self.raw = true

  The checker accepts.

theorem Hex.Nat.CheckedPrimeCert.prime {n : Nat} (c : CheckedPrimeCert n) : Prime n

The primality of the requested subject.