Registry · Theorem III.T71 tau-effective formalized

III.T71 — Obstruction Bounded

Obstruction bounded: at each prime p_k, obstruction count ≤ 1 for even n ≤ 100.

Book III Part 10 Ch. 81

Dependency Graph

Depends on (1)

III.D104

Lean Formalization

Module: TauLib.BookIII.Spectral.GoldbachDeep

Symbol: obstruction_bounded_5