Registry · Theorem III.T69 tau-effective formalized

III.T69 — Goldbach at Primorial M₄

Goldbach at M₄=210: all even n ≤ 210 verified. Primorial-level Goldbach extends M₃ result.

Book III Part 10 Ch. 81

Dependency Graph

Depends on (1)

III.D102

Lean Formalization

Module: TauLib.BookIII.Spectral.GoldbachDeep

Symbol: goldbach_primorial_m4