theorem Hex.ECPP.replayBits_rep {p n a b q : ℕ} [Fact (_root_.Nat.Prime p)] (hp : p ∣ n) (hn : 0 < n) (Q : Point) (V : (shortCurve p a b).toAffine.Point) (hQ : Point.Rep p a b Q V) (k : ℕ) {R S : Point} {ws rest : List ℕ} (U : (shortCurve p a b).toAffine.Point) : Point.Rep p a b R U → replayBits n a b q Q k R ws = some (S, rest) → Point.Rep p a b S (2 ^ k • U + (q % 2 ^ k) • V)

The structurally recursive raw replay computes the canonical binary prefix of the scalar in the actual elliptic-curve group.

theorem Hex.ECPP.replay_zero {p n a b q : ℕ} [Fact (_root_.Nat.Prime p)] (hp : p ∣ n) (hn : 0 < n) (Q : Point) (V : (shortCurve p a b).toAffine.Point) (hQ : Point.Rep p a b Q V) {ws rest : List ℕ} (h : replay n a b q Q ws = some (Point.infinity, rest)) : q • V = 0

If the complete replay returns infinity, its field point is annihilated by the child subject.

theorem Hex.ECPP.natPrime_of_step {n a b x y discrInv q : ℕ} {inverses : List ℕ} (hq : _root_.Nat.Prime q) (h : checkStep n a b x y discrInv inverses q = true) : _root_.Nat.Prime n

A checked ECPP step is prime once its structurally smaller child subject is prime. No primality of the candidate is assumed.

theorem Hex.ECPP.natPrime_of_check {cert : Cert} (h : check cert = true) : _root_.Nat.Prime cert.subject

An accepted elliptic curve primality certificate proves its recorded integer prime in Mathlib. The sole premise is the checker equation: the smaller primes, curve nonsingularity, point order and Hasse-bound size condition are all verified by the certificate and soundness proof.

theorem Hex.ECPP.natPrime_of_checkAt {n : ℕ} {cert : Cert} (h : checkAt n cert = true) : _root_.Nat.Prime n

If checkAt n cert = true, then n is prime. The checker verifies both the certificate and that its recorded integer is n; no additional assumption about search, curve orders or auxiliary primes is required.