Prime Enumeration and Sieve

Prime enumeration nthPrime(k) = p_k, prime counting pi(n), and prime index (inverse). The earned Sieve of Eratosthenes: computed entirely from rho-folds via is_prime_bool. Semantic orbit projection from pi-orbit to alpha-orbit values.

Prime Enumeration and Sieve

Summary

Prime enumeration nthPrime(k) = p_k, prime counting pi(n), and prime index (inverse). The earned Sieve of Eratosthenes: computed entirely from rho-folds via is_prime_bool. Semantic orbit projection from pi-orbit to alpha-orbit values.

Statement

%
\label{def:prime-enumeration}
The \textbf{prime enumeration function}
$\mathrm{nthPrime} : \tau\text{-Idx} \to \tau\text{-Idx}$
maps each index $\underline{k}$ to the $k$-th prime
(zero-indexed):
\[
    \mathrm{nthPrime}(\underline{0}) = \underline{2}, \quad
    \mathrm{nthPrime}(\underline{1}) = \underline{3}, \quad
    \mathrm{nthPrime}(\underline{2}) = \underline{5}, \quad
    \mathrm{nthPrime}(\underline{3}) = \underline{7}, \quad \ldots
\]
The \textbf{prime counting function}
$\pi_\tau : \tau\text{-Idx} \to \tau\text{-Idx}$
counts primes up to a given bound:
\[
    \pi_\tau(\underline{n})
    = \#\{\, \underline{p} \in \mathbb{P}_\tau
        : \underline{p} \leq \underline{n} \,\}.
\]
The \textbf{prime index function}
$\mathrm{primeIdx} : \mathbb{P}_\tau \to \tau\text{-Idx}$
is the inverse of $\mathrm{nthPrime}$:
for each prime $\underline{p}$,
$\mathrm{primeIdx}(\underline{p}) = \underline{k}$
where $\mathrm{nthPrime}(\underline{k}) = \underline{p}$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 69
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part04/ch16-primes-divisibility.tex lines 364-391

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Coordinates.PrimeEnumeration
• Name: Tau.Coordinates.nthPrime

Dependencies

• Canonical: I.D19b

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.