not_proxyPhysicalizationBridge_of_charge_ne_zero

formal source

 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
 142    exact not_proxyPhysicalizationBridge_of_charge_ne_zero
 143      (zetaDefectSensor ρ.re ⟨hlo, hhi⟩ 1)
 144      (zetaDefectSensor_charge_ne_zero ρ.re ⟨hlo, hhi⟩)
 145      (hzipb ρ hzero hlo hhi)
 146  · intro hno ρ hzero hlo hhi
 147    exact (hno ρ hzero hlo hhi).elim