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

zeroInducedBridge_iff_rsPhysicalThesis

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)

 126theorem zeroInducedBridge_iff_rsPhysicalThesis :
 127    ZeroInducedProxyPhysicalizationBridge ↔ RSPhysicalThesis := by

proof body

Term-mode proof.

 128  constructor
 129  · intro hzipb ρ hzero hlo hhi
 130    exact (proxyPhysicalizationBridge_iff_physicallyExists _).mp (hzipb ρ hzero hlo hhi)
 131  · intro hrs ρ hzero hlo hhi
 132    exact (proxyPhysicalizationBridge_iff_physicallyExists _).mpr (hrs ρ hzero hlo hhi)
 133
 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. -/

used by (1)

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

depends on (14)

Lean names referenced from this declaration's body.