canonicalDefectSampledFamily_charge

formal source

 104  chosenDefectPhaseFamily_sensor sensor hm
 105
 106/-- Every mesh in the canonical sampled family has the requested sensor charge. -/
 107theorem canonicalDefectSampledFamily_charge (sensor : DefectSensor)
 108    (hm : sensor.charge ≠ 0) (N : ℕ) :
 109    ((canonicalDefectSampledFamily sensor hm).mesh N).charge = sensor.charge := by
 110  simpa [canonicalDefectSampledFamily_sensor sensor hm] using
 111    ((canonicalDefectSampledFamily sensor hm).charge_spec N)
 112
 113/-! ### §3. Refined bounded-cost proposition -/
 114
 115/-- The annular cost of a realized sampled family is bounded independently of
 116mesh refinement. This is the realizable replacement for the previous
 117over-strong quantification over arbitrary `AnnularMesh` values. -/
 118def RealizedDefectAnnularCostBounded (fam : DefectSampledFamily) : Prop :=
 119  ∃ K : ℝ, ∀ N : ℕ, annularCost (fam.mesh N) ≤ K
 120
 121/-- The annular excess of a realized sampled family is bounded independently of
 122mesh refinement. This is the quantitatively plausible part of the defect-cost
 123story: after removing the topological floor, only the regular remainder should
 124need analytic control. -/
 125def RealizedDefectAnnularExcessBounded (fam : DefectSampledFamily) : Prop :=
 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. -/