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

euler_carrier_zero_winding

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)

 114theorem euler_carrier_zero_winding (σ₀ : ℝ) (hσ : 1/2 < σ₀)
 115    (r : ℝ) (hr : 0 < r) (hrR : r < σ₀ - 1/2) :
 116    contourWinding (mkComplexCarrierCert σ₀ hσ) r = 0 :=

proof body

Term-mode proof.

 117  carrier_zero_winding _ r hr hrR
 118
 119/-! ### §4. Interface to sampled traces -/
 120
 121/-- A zero-winding certificate: the function has zero winding around every
 122interior circle. This is the interface consumed by the sampled-trace layer. -/

depends on (12)

Lean names referenced from this declaration's body.