def definition def or abbrev

`ZeroInducedProxyPhysicalizationBridge`

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

formal statement (Lean)

  57def ZeroInducedProxyPhysicalizationBridge : Prop :=

proof body

Definition body.

  58  ∀ (ρ : ℂ), riemannZeta ρ = 0 →
  59    ∀ (hlo : 1/2 < ρ.re) (hhi : ρ.re < 1),
  60      ProxyPhysicalizationBridge (zetaDefectSensor ρ.re ⟨hlo, hhi⟩ 1)
  61
  62/-- The zero-induced proxy physicalization bridge implies the RS Physical
  63Thesis. -/

used by (7)

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

not_proxyPhysicalizationBridge_of_charge_ne_zero in IndisputableMonolith.NumberTheory.ProxyPhysicalizationBridge decl_use
rh_from_ZeroInducedProxyPhysicalizationBridge in IndisputableMonolith.NumberTheory.ProxyPhysicalizationBridge decl_use
rsPhysicalThesis_of_ZeroInducedProxyPhysicalizationBridge in IndisputableMonolith.NumberTheory.ProxyPhysicalizationBridge decl_use
zeroInducedBridge_iff_no_strip_zeros in IndisputableMonolith.NumberTheory.ProxyPhysicalizationBridge decl_use
zeroInducedBridge_iff_rh in IndisputableMonolith.NumberTheory.ProxyPhysicalizationBridge decl_use
zeroInducedBridge_iff_rsPhysicalThesis in IndisputableMonolith.NumberTheory.ProxyPhysicalizationBridge decl_use
zeroInducedBridge_of_rh in IndisputableMonolith.NumberTheory.ProxyPhysicalizationBridge decl_use

depends on (4)

Lean names referenced from this declaration's body.

Physical in IndisputableMonolith.Bridge.DataCore decl_use
bridge in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
zetaDefectSensor in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use
ProxyPhysicalizationBridge in IndisputableMonolith.NumberTheory.ProxyPhysicalizationBridge decl_use