Registry · Definition I.D19f established formalized

I.D19f — 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.

Book I Part 4 Ch. 16

Dependency Graph

Depends on (1)

Depended on by (1)

Lean Formalization

Module: TauLib.BookI.Coordinates.PrimeEnumeration

Symbol: Tau.Coordinates.nthPrime