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

• pock3Sieve (n r s w m : Nat) (factors : List (Nat × Nat × PrimeCert)) : PrimeCert

  Cube-root Pocklington with divisors lF+1 excluded for 1 ≤ l < m.

@[instance_reducible]

instance Hex.Nat.instReprPrimeCert : Repr PrimeCert

Equations

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

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

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
• (Hex.Nat.PrimeCert.pock3Sieve n r s w m factors).subject = n

def Hex.Nat.boundedPowMul.native (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.native bound q x✝ 0 = some x✝
• Hex.Nat.boundedPowMul.native 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.native bound q (x✝ * q) e else none

noncomputable def Hex.Nat.boundedPowMul.go (bound q acc e : Nat) : Option Nat

Kernel reduction uses raw recursors to avoid auxiliary match and Decidable reductions at each bounded multiplication.

Equations

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

noncomputable def Hex.Nat.boundedPowMul (bound q acc e : Nat) : Option Nat

Powers of two use a checked shift: the right shift checks the final product bound before the left shift constructs that product. Other bases use bounded multiplication. Compiled evaluation retains the original loop.

Equations

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

@[csimp]

theorem Hex.Nat.boundedPowMul_eq_native : boundedPowMul = boundedPowMul.native

The compiler uses the verified runtime implementation.

@[simp]

theorem Hex.Nat.boundedPowMul_zero (bound q acc : Nat) : boundedPowMul bound q acc 0 = some acc

Exponent zero preserves the accumulator, even when it exceeds the bound.

theorem Hex.Nat.boundedPowMul_succ (bound q acc e : Nat) : boundedPowMul bound q acc (e + 1) = if acc = 0 then some 0 else if q = 0 then some 0 else if acc ≤ bound / q then boundedPowMul bound q (acc * q) e else none

One checked multiplication, as an equation for symbolic proofs.

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

noncomputable def Hex.Nat.pockProduct (bound : Nat) : List (Nat × Nat × PrimeCert) → Nat

Bounded product for positive factor subjects, with zero denoting failure. The caller checks positivity. Exponent-one entries multiply and check the result against the bound; larger exponents retain the bounded power routine. A multiplication has at most the sum of its operands’ bit lengths.

Equations

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

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

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

Equations

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

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

Primitive comparisons in a direct list fold for kernel replay.

Equations

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

@[csimp]

theorem Hex.Nat.subjectsAfter_eq_native : subjectsAfter = subjectsAfter.native

The compiler uses the verified runtime implementation.

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.native (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.native n q a = (HexArith.powModNat a (n - 1) n == 1 % n && ((HexArith.powModNat a ((n - 1) / q) n + n - 1) % n).gcd n == 1)

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

The witness conditions with primitive Nat comparisons for kernel reduction.

Equations

• Hex.Nat.checkWitness n q a = ((HexArith.powModNat a (n.sub 1) n).beq (Nat.mod 1 n) && (((((HexArith.powModNat a ((n.sub 1).div q) n).add n).sub 1).mod n).gcd n).beq 1)

@[csimp]

theorem Hex.Nat.checkWitness_eq_native : checkWitness = checkWitness.native

The compiler uses the verified runtime implementation.

def Hex.Nat.checkWitnesses.native (n : Nat) (fs : List (Nat × Nat × PrimeCert)) : Bool

The ordinary per-entry witness traversal used by compiled search.

Equations

• Hex.Nat.checkWitnesses.native n fs = fs.all fun (x : Nat × Nat × Hex.Nat.PrimeCert) => Hex.Nat.checkWitness n x.snd.snd.subject x.fst

noncomputable def Hex.Nat.checkWitnesses.go (n : Nat) (fs : List (Nat × Nat × PrimeCert)) (prev : Nat) (seen : Bool) : Bool

Replay adjacent equal witness bases with one Fermat check. seen records that the preceding base passed its Fermat check; the initial state is false.

Equations

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

noncomputable def Hex.Nat.checkWitnesses (n : Nat) (fs : List (Nat × Nat × PrimeCert)) : Bool

Check every witness, reusing the Fermat leg for adjacent equal bases.

Equations

• Hex.Nat.checkWitnesses n fs = Hex.Nat.checkWitnesses.go n fs 0 false

@[csimp]

theorem Hex.Nat.checkWitnesses_eq_native : checkWitnesses = checkWitnesses.native

The compiler uses the verified runtime implementation.

def Hex.Nat.checkPockArith.native (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.

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

Kernel comparisons use primitive Nat operations; compiled evaluation retains the original arithmetic check.

Equations

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

def Hex.Nat.checkPock3Arith.native (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.

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

Kernel replay uses the bounded positive product and primitive comparisons. Compiled checking retains the original arithmetic path.

Equations

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

def Hex.Nat.pocklingtonSieveCap : Nat

Maximum sieve bound in a checked certificate. This caps replay work for arbitrary untrusted literals, including rejected inputs.

Equations

• Hex.Nat.pocklingtonSieveCap = 64

def Hex.Nat.checkDivisors (n F : Nat) : Nat → Bool

Check the first k possible divisors lF+1.

Equations

• Hex.Nat.checkDivisors n F 0 = true
• Hex.Nat.checkDivisors n F k.succ = (Hex.Nat.checkDivisors n F k && n % ((k + 1) * F + 1) != 0)

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

The general cube-root arithmetic check; the legacy node retains its sieve-free path.

Equations

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

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

Kernel replay uses the bounded positive product and primitive comparisons. Compiled checking retains the original arithmetic path.

Equations

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

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.

@[csimp]

theorem Hex.Nat.checkPockArith_eq_native : checkPockArith = checkPockArith.native

The compiler uses the verified arithmetic implementation.

@[csimp]

theorem Hex.Nat.checkPock3Arith_eq_native : checkPock3Arith = checkPock3Arith.native

The compiler uses the verified runtime implementation.

@[csimp]

theorem Hex.Nat.checkPock3SieveArith_eq_native : checkPock3SieveArith = checkPock3SieveArith.native

The compiler uses the verified runtime implementation.

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

Accept or reject a primality certificate. Pocklington factor lists are accepted only in strictly ascending child-subject order. This is the ordinary compiled traversal; the public checkPrime supplies the kernel fold.

Equations

• Hex.Nat.checkPrime.native (Hex.Nat.PrimeCert.small n) = Hex.Nat.isTablePrime n
• Hex.Nat.checkPrime.native (Hex.Nat.PrimeCert.pock n factors) = (Hex.Nat.checkPockArith n factors && Hex.Nat.checkChildren factors)
• Hex.Nat.checkPrime.native (Hex.Nat.PrimeCert.pock3 n r s w factors) = (Hex.Nat.checkPock3Arith n r s w factors && Hex.Nat.checkChildren factors)
• Hex.Nat.checkPrime.native (Hex.Nat.PrimeCert.pock3Sieve n r s w m factors) = (Hex.Nat.checkPock3SieveArith n r s w m 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.native c && Hex.Nat.checkChildren rest)

noncomputable def Hex.Nat.checkPrime : PrimeCert → Bool

Direct structural fold for kernel replay. Compiled code retains the ordinary mutually recursive traversal.

Equations

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

@[csimp]

theorem Hex.Nat.checkPrime_eq_native : checkPrime = checkPrime.native

The compiler uses the verified recursive implementation.

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.