Registry · Theorem III.T09 tau-effective formalized

III.T09 — Primorial Cofinality

The primorial tower is cofinal: every ℤ/Nℤ maps to ℤ/Prim(k)ℤ for k large enough. Checking at primorial levels is SUFFICIENT. The cutoff k₀ is always computable.

Book III Part 3 Ch. 14

Dependency Graph

Depends on (1)

III.D19

Depended on by (11)

III.D30 III.D36 III.D37 III.D53 III.P11 III.P16 III.P17 III.R08 III.T10 III.T26 III.T31

Lean Formalization

Module: TauLib.BookIII.Spectral.PrimorialLadder

Symbol: primorial_cofinal_check