pith. machine review for the scientific record. sign in
theorem proved term proof

rh_from_ZeroInducedProxyPhysicalizationBridge

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  73theorem rh_from_ZeroInducedProxyPhysicalizationBridge
  74    (bridge : ZeroInducedProxyPhysicalizationBridge) :
  75    RiemannHypothesis :=

proof body

Term-mode proof.

  76  rh_from_rs_thesis (rsPhysicalThesis_of_ZeroInducedProxyPhysicalizationBridge bridge)
  77
  78/-! ## Equivalence Theorems
  79
  80The bounded-proxy hypothesis in `ProxyPhysicalizationBridge` is
  81unconditionally proved (`EulerLedgerOntologyInterface.scalarDefectBounded`).
  82Therefore the implication collapses to its conclusion, and the bridge
  83is equivalent to `PhysicallyExists`, to `charge = 0`, and (for the
  84zeta-zero specialization) to `RSPhysicalThesis` and to `RiemannHypothesis`.
  85
  86These equivalences are the definitive reduction: the bridge proposition is
  87neither weaker nor stronger than RH — it IS RH, expressed through the
  88T1-bounded realizability architecture. -/
  89
  90/-- The proxy physicalization bridge is equivalent to physical existence.
  91The bounded-proxy hypothesis is unconditionally true, so the implication
  92reduces to its conclusion. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (15)

Lean names referenced from this declaration's body.