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

zetaDerivedPhaseFamily_sensor

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)

 360@[simp] theorem zetaDerivedPhaseFamily_sensor
 361    (sensor : DefectSensor) (qlf : QuantitativeLocalFactorization)
 362    (horder : qlf.order = -sensor.charge) :
 363    (zetaDerivedPhaseFamily sensor qlf horder).sensor = sensor := rfl

proof body

Term-mode proof.

 364
 365/-- The current `zetaDerivedPhaseFamily` carries a zero-perturbation witness:
 366its sampled increments are exactly the pure winding increments. -/

depends on (4)

Lean names referenced from this declaration's body.