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

SpiralArray

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)

  36def SpiralArray (n_coils : ℕ) (r0 : ℝ) (kappa : ℤ) : List Coil :=

proof body

Definition body.

  37  List.range n_coils |>.map fun i =>
  38    let theta := (i : ℝ) * 2 * Real.pi / n_coils
  39    let r := Geometry.SpiralLemmas.logSpiral r0 theta { kappa := kappa }
  40    let phase := i % 8
  41    { id := i, angle := theta, radius := r, phase_offset := phase }
  42
  43/-- The Tip Speed of the virtual field.
  44    v = distance / time = (2π r) / (period).
  45    Period = n_coils * pulse_width. -/

depends on (19)

Lean names referenced from this declaration's body.