Registry · Definition III.D99 established formalized

III.D99 — Eratosthenes Sieve

Sieve of Eratosthenes: computable primality predicate via trial division. Foundation for all three conjecture tracks.

Book III Part 10 Ch. 81

Dependency Graph

Depends on (1)

I.T09

Depended on by (8)

III.D100 III.D101 III.D102 III.D103 III.D105 III.P42 III.T66 III.T67

Lean Formalization

Module: TauLib.BookIII.Spectral.SieveInfrastructure

Symbol: eratosthenes_sieve