theorem
proved
tactic proof
zeroInducedBridge_of_rh
show as:
view Lean formalization →
formal statement (Lean)
151theorem zeroInducedBridge_of_rh (hrh : RiemannHypothesis) :
152 ZeroInducedProxyPhysicalizationBridge := by
proof body
Tactic-mode proof.
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. -/