zeroInducedBridge_iff_rsPhysicalThesis

formal source

 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
 148
 149/-- Mathlib's `RiemannHypothesis` implies `ZeroInducedProxyPhysicalizationBridge`.
 150Any strip zero would violate `Re(ρ) = 1/2`, so the bridge holds vacuously. -/
 151theorem zeroInducedBridge_of_rh (hrh : RiemannHypothesis) :
 152    ZeroInducedProxyPhysicalizationBridge := by
 153  rw [zeroInducedBridge_iff_no_strip_zeros]
 154  intro ρ hzero hlo hhi
 155  have hntrivial : ¬∃ n : ℕ, ρ = -2 * (↑n + 1) := by
 156    rintro ⟨n, hn⟩