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

RealizedDefectAnnularExcessBounded

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)

 125def RealizedDefectAnnularExcessBounded (fam : DefectSampledFamily) : Prop :=

proof body

Definition body.

 126  ∃ K : ℝ, ∀ N : ℕ, annularExcess (fam.mesh N) ≤ K
 127
 128/-! ### §3a. Ring-level regular-part error control -/
 129
 130/-- A ring-level regular-part error package for a realized sampled family.
 131
 132For each depth `N` and ring `n`, the sampled ring cost is bounded by the
 133topological floor for its charge sector plus an error term coming from the
 134regular factor in the local meromorphic factorization. The total error across
 135all rings is uniformly bounded in `N`.
 136
 137This is the exact quantitative input needed to prove bounded annular excess. -/

used by (11)

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

depends on (22)

Lean names referenced from this declaration's body.