pith. machine review for the scientific record. sign in
def definition def or abbrev

zeroWindingData

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)

  56def zeroWindingData (c : ℂ) (r : ℝ) (hr : 0 < r) : WindingData where
  57  center := c

proof body

Definition body.

  58  radius := r
  59  radius_pos := hr
  60  charge := 0
  61
  62/-! ### §2. Zero winding from carrier certificate -/
  63
  64/-- Given a `ZeroWindingCert`, produce zero `WindingData` at any interior radius.
  65This is the bridge from the complex carrier certificate to the discrete sampling
  66layer: the carrier has zero winding, so any sampling of it will produce zero
  67net phase increment. -/

depends on (22)

Lean names referenced from this declaration's body.