pith. machine review for the scientific record. sign in
theorem proved term proof

zeroInducedBridge_iff_no_strip_zeros

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 137theorem zeroInducedBridge_iff_no_strip_zeros :
 138    ZeroInducedProxyPhysicalizationBridge ↔
 139      (∀ ρ : ℂ, riemannZeta ρ = 0 → 1/2 < ρ.re → ρ.re < 1 → False) := by

proof body

Term-mode proof.

 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. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.