Twin Primes and Siegel Zeros: a Fulcrum

Every theorem in this paper is verified by the Lean 4 kernel over mathlib, with axiom base exactly {propext, Classical.choice, Quot.sound}; nothing rests on informal argument. We introduce the fulcrum: a single hypothesis—one fixed quality constant C★, one zero per unbounded window—under which, together with an explicitly stated engine hypothesis, Siegel zeros produce infinitely many twin primes; the zero's reality is derived rather than assumed, and the fulcrum is proved minimal for the engine that consumes it. Around it we prove kernel-checked zero-free regions for ζ, a Deuring–Heilbronn repulsion contract, an exchange-rate neutrality theorem pricing transfer-based routes to twins, and the parity gap as a mathematical object. The corpus is 324,724 lines of Lean across 751 files, produced by the Salt method, which is described as a contribution in its own right. MSC 2020: Primary 11M26; Secondary 68V20, 11N35. Every result is a declaration in the public Lean 4 corpus at https://github.com/jyh/salt; Appendix A of the paper maps each stated result to its declaration and axiom audit.