Registry · Proposition III.P43 tau-effective formalized

III.P43 — CRT-Goldbach Duality

CRT-Goldbach local solvability: for any even n≥4 and prime p≥3, ∃r with both r and n-r nonzero mod p. CRT guarantees independent local solutions.

Book III Part 10 Ch. 81

Dependency Graph

Depends on (2)

Depended on by (1)

Lean Formalization

Module: TauLib.BookIII.Spectral.GoldbachDeep

Symbol: crt_goldbach_duality_3