Registry · Theorem III.T67 established formalized

III.T67 — Sieve-Tower Compatibility

Sieve is tower-stable: M_k|M_{k+1}, each p_i divides M_k. Brun sieve matches Euler phi: B(M_k,k)=φ(M_k).

Book III Part 10 Ch. 81

Dependency Graph

Depends on (3)

III.D99 III.D101 III.D19

Lean Formalization

Module: TauLib.BookIII.Spectral.SieveInfrastructure

Symbol: sieve_tower_compat_3