zeroInducedBridge_iff_no_strip_zeros

formal source

 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⟩
 157    have h1 : ρ.re = (-2 * ((n : ℂ) + 1)).re := congrArg Complex.re hn
 158    have h2 : (-2 * ((n : ℂ) + 1)).re = -2 * ((n : ℝ) + 1) := by
 159      rw [Complex.mul_re, Complex.add_re, Complex.natCast_re, Complex.one_re,
 160          Complex.add_im, Complex.natCast_im, Complex.one_im]
 161      simp [Complex.neg_re, Complex.neg_im]
 162    linarith [Nat.cast_nonneg (α := ℝ) n]
 163  have hne1 : ρ ≠ 1 := by
 164    intro h; rw [h, Complex.one_re] at hhi; linarith
 165  linarith [hrh ρ hzero hntrivial hne1]
 166
 167/-- **`ZeroInducedProxyPhysicalizationBridge ↔ RiemannHypothesis`.**