`zeroInducedBridge_iff_rh`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.ProxyPhysicalizationBridge
domain: NumberTheory
line: 175 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.ProxyPhysicalizationBridge on GitHub at line 175.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 172
 173This closes the reduction: the directed-ledger infrastructure correctly isolates
 174the gap, and the gap is precisely RH — no more, no less. -/
 175theorem zeroInducedBridge_iff_rh :
 176    ZeroInducedProxyPhysicalizationBridge ↔ RiemannHypothesis :=
 177  ⟨rh_from_ZeroInducedProxyPhysicalizationBridge, zeroInducedBridge_of_rh⟩
 178
 179/-! ## Axiom audit -/
 180
 181#print axioms proxyPhysicalizationBridge_iff_physicallyExists
 182#print axioms proxyPhysicalizationBridge_iff_charge_zero
 183#print axioms zeroInducedBridge_iff_rsPhysicalThesis
 184#print axioms zeroInducedBridge_iff_no_strip_zeros
 185#print axioms zeroInducedBridge_iff_rh
 186
 187end NumberTheory
 188end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.