proxyPhysicalizationBridge_of_charge_zero

formal source

 108    (charge_zero_iff_physicallyExists sensor).symm
 109
 110/-- The bridge holds unconditionally for charge-zero sensors. -/
 111theorem proxyPhysicalizationBridge_of_charge_zero (sensor : DefectSensor)
 112    (h : sensor.charge = 0) : ProxyPhysicalizationBridge sensor :=
 113  (proxyPhysicalizationBridge_iff_charge_zero sensor).mpr h
 114
 115/-- The bridge fails for any sensor with nonzero charge: the cost scalar
 116collapses and T1 defect diverges, so `PhysicallyExists` is false. -/
 117theorem not_proxyPhysicalizationBridge_of_charge_ne_zero (sensor : DefectSensor)
 118    (hm : sensor.charge ≠ 0) : ¬ ProxyPhysicalizationBridge sensor := by
 119  intro hbridge
 120  exact nonzero_charge_not_physical sensor hm
 121    (physicallyExists_of_ProxyPhysicalizationBridge sensor hbridge)
 122
 123/-- `ZeroInducedProxyPhysicalizationBridge` is logically equivalent to
 124`RSPhysicalThesis`: the bridge at zeta-zero sensors reduces to the RS
 125claim that zeta zeros are physical recognition events. -/
 126theorem zeroInducedBridge_iff_rsPhysicalThesis :
 127    ZeroInducedProxyPhysicalizationBridge ↔ RSPhysicalThesis := by
 128  constructor
 129  · intro hzipb ρ hzero hlo hhi
 130    exact (proxyPhysicalizationBridge_iff_physicallyExists _).mp (hzipb ρ hzero hlo hhi)
 131  · intro hrs ρ hzero hlo hhi
 132    exact (proxyPhysicalizationBridge_iff_physicallyExists _).mpr (hrs ρ hzero hlo hhi)
 133
 134/-- `ZeroInducedProxyPhysicalizationBridge` is equivalent to the absence of
 135strip zeros of ζ: for charge-1 sensors, the bridge evaluates to `False`,
 136so quantifying over strip zeros asserts their non-existence. -/
 137theorem zeroInducedBridge_iff_no_strip_zeros :
 138    ZeroInducedProxyPhysicalizationBridge ↔
 139      (∀ ρ : ℂ, riemannZeta ρ = 0 → 1/2 < ρ.re → ρ.re < 1 → False) := by
 140  constructor
 141  · intro hzipb ρ hzero hlo hhi