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

defectPhasePureIncrement

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)

 152noncomputable def defectPhasePureIncrement (dpf : DefectPhaseFamily) (n : ℕ) : ℝ :=

proof body

Definition body.

 153  -(2 * Real.pi * (dpf.sensor.charge : ℝ)) / (8 * n : ℝ)
 154
 155/-- Quantitative perturbation data for the regular factor in a defect phase
 156family.
 157
 158This structure captures exactly the data needed downstream to build the
 159`RingPerturbationControl` witness for the canonical sampled family:
 160
 1611. each sampled increment splits as the pure winding increment plus a regular
 162   perturbation `ε`;
 1632. every `ε` stays in the unit perturbative regime for the proved
 164   `phiCost` bound; and
 1653. the total linear and quadratic perturbation budgets are uniformly bounded in
 166   the refinement depth `N`. -/

used by (13)

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

depends on (17)

Lean names referenced from this declaration's body.