Volume V Synthesis — Dual-Track Obstruction Reductions (Work in Progress)
Headline Lean Theorems (Codex-Verified)
theorem ObstructionTrackA : RH_classical ↔ ∃ (J : Polarization), Compatible J ωtheorem ObstructionTrackB : RH_classical ↔ CondensedPurityTransfer SpecZCondtheorem RH_HilbertPolya_iff_RH_Frob : RH_HilbertPolya ↔ RH_Frob (inside ℰ_cond)Abstract
Synthesis of the HoTT-Riemann programme to date. Thirteen concurrent agent teams across five months produced 239 valid / 0 invalid Lean theorems. The current state: theorem ObstructionTrackA reduces RH to wedge-polarization convergence; theorem ObstructionTrackB reduces RH to CondensedPurityTransfer SpecZCond inside the condensed topos. The dual obstructions are honest logical equivalences characterising the same barrier from operator-theoretic and cohomological angles. The post-pipeline Yoneda–Nyman addendum sharpens Track A further. Work in progress — RH remains open, precisely quantified, and the programme continues.
The synthesis paper has no Lean library of its own; the figures below are the project totals it summarises across the 13 team papers.
Full Paper
Read the full paper as a PDF:
Open PDF