theorem Hex.Nat.not_square_of_sqrt_witness {w D : Nat} (h1 : w * w < D) (h2 : D < (w + 1) * (w + 1)) (t : Nat) : t * t ≠ D

A number strictly between consecutive squares is not a square: the witness form of the discriminant test, which the checker verifies with two multiplications instead of a (non-kernel-reducible) Nat.sqrt call.

theorem Hex.Nat.pocklington3 {n F r s : Nat} (hn3 : 3 ≤ n) (hF : F ∣ n - 1) (hFeven : F % 2 = 0) (hF0 : 0 < F) (hRodd : (n - 1) / F % 2 = 1) (hdec : (n - 1) / F = 2 * F * s + r) (hr1 : 1 ≤ r) (hr2 : r < 2 * F) (hbound : n < (F + 1) * (2 * F * F + (r - 1) * F + 1)) (hdisc : s = 0 ∨ r * r < 8 * s ∨ ∀ (t : Nat), t * t ≠ r * r - 8 * s) : (∀ (p : Nat), Prime p → p ∣ n → F ∣ p - 1) → Prime n

The cube-root Brillhart-Lehmer-Selfridge criterion at m = 1. The hypothesis hdivmod is what the per-entry witness conditions of the certificate checker produce (pock_divisor_step on the checker side); R odd is the weaker form of the classical gcd(F, R) = 1 that the proof actually uses once F is even.