zeroInducedBridge_of_rh

formal source

 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`.**
 168
 169The bridge proposition is exactly equivalent to Mathlib's `RiemannHypothesis`.
 170Forward: `rh_from_ZeroInducedProxyPhysicalizationBridge` (via RS thesis + functional equation).
 171Backward: `zeroInducedBridge_of_rh` (RH eliminates all strip zeros, making the bridge vacuous).
 172
 173This closes the reduction: the directed-ledger infrastructure correctly isolates
 174the gap, and the gap is precisely RH — no more, no less. -/
 175theorem zeroInducedBridge_iff_rh :
 176    ZeroInducedProxyPhysicalizationBridge ↔ RiemannHypothesis :=
 177  ⟨rh_from_ZeroInducedProxyPhysicalizationBridge, zeroInducedBridge_of_rh⟩
 178
 179/-! ## Axiom audit -/
 180
 181#print axioms proxyPhysicalizationBridge_iff_physicallyExists