Each certificate prime belongs to the theta certificate list

Proved

TaoFivePrimes.tao_totient_cert_ptab_mem

by andreaskapfer · Sep 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

certificatenumber-theoryprime-numberstao-five-primes

The Chebyshev-theta certificates used in this development are indexed by the Finset plist, the list of the 66 primes below 320. The certificate prime table ptab records the same primes in increasing order.

The theorem states that every entry of the table is a member of the certificate list:

\mathrm{ptab}(i) \;\in\; \mathrm{plist} \qquad (0 \le i < 66).

Combined with the identification $\mathrm{ptab}(i) = p_{i+1}$ , this lets arguments about the first 66 primes pass freely between the explicit numeric table and the certificate list plist, so that the prime-by-prime logarithm certificates can be attached to the entries of ptab.

Preamble

import Definitions.Def_TaoFivePrimes_theta_cert_tables
import Definitions.Def_TaoFivePrimes_totient_cert_tables

Formal statement

namespace TaoFivePrimes

theorem tao_totient_cert_ptab_mem (i : ℕ) (hi : i < 66) :
    ptab i ∈ plist := by sorry

end TaoFivePrimes

Source

Input data for the finite Rosser--Schoenfeld (1962) totient verification formalized in this project; the list `plist` is the prime list of the Chebyshev-theta logarithm certificates.

View graph