rh_from_ZeroInducedProxyPhysicalizationBridge

formal source

  70
  71/-- Hence the full Riemann Hypothesis follows once the proxy physicalization
  72bridge is proved for the zeta-zero sensors. -/
  73theorem rh_from_ZeroInducedProxyPhysicalizationBridge
  74    (bridge : ZeroInducedProxyPhysicalizationBridge) :
  75    RiemannHypothesis :=
  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. -/
  93theorem proxyPhysicalizationBridge_iff_physicallyExists (sensor : DefectSensor) :
  94    ProxyPhysicalizationBridge sensor ↔ PhysicallyExists sensor := by
  95  constructor
  96  · exact physicallyExists_of_ProxyPhysicalizationBridge sensor
  97  · intro hphys
  98    let pkg := concreteEulerLedgerOntologyInterface sensor
  99    letI : PhysicallyRealizableLedger sensor := pkg.realizableProxy
 100    exact fun _ => hphys
 101
 102/-- The proxy physicalization bridge is equivalent to charge zero.
 103Combines the bridge-to-existence equivalence with the ontological