realizedDefectAnnularExcessBounded_of_ringRegularErrorBound
A uniform bound on the total regular-part error across rings in a realized sampled annular family implies that the annular excess stays bounded under mesh refinement. Number theorists closing the refined Axiom 2 in the Recognition framework cite this to convert ring-level estimates into global excess control for the canonical defect family. The proof extracts the uniform error constant K from the hypothesis and chains it via transitivity with the inequality that absorbs the nonnegative topological floor into the excess.
claimLet $fam$ be a realized sampled family of annular meshes attached to one defect sensor. Suppose $fam$ admits a ring-regular error bound: for each depth $N$ and ring index $n$, the ring cost is at most the topological floor for its charge sector plus an error term, and the sum of these error terms over all rings is bounded by some constant $K$ independent of $N$. Then the annular excess of $fam$ is bounded by $K$ independently of refinement depth.
background
DefectSampledFamily packages a sensor together with a sequence of realized AnnularMesh objects whose charges match the sensor; it arises from phase sampling of the inverse zeta function near a hypothetical defect rather than from arbitrary synthetic meshes. RingRegularErrorBound supplies, for each $N$ and each ring, an explicit error term such that ring cost is bounded by the topological floor plus that error, together with the statement that the total error summed over rings remains uniformly bounded in $N$. RealizedDefectAnnularExcessBounded asserts the existence of a single $K$ such that annular excess of the mesh at depth $N$ never exceeds $K$ for any $N$ (MODULE_DOC).
proof idea
The term-mode proof first obtains the uniform error bound $K$ and its witness $hK$ from the total_error_bounded field of the RingRegularErrorBound hypothesis. It then refines the goal to show annular excess at each $N$ is at most $K$, applying le_trans to the inequality annularExcess_le_sum_of_ringCost_le_topologicalFloor_plus_regularError (which absorbs the nonnegative topological floor) followed by the bound $hK N$.
why it matters in Recognition Science
This theorem supplies the final step that converts a ring-regular error package into bounded annular excess for any realized sampled family. It is invoked directly by canonicalDefectSampledFamily_excess_bounded (which handles the nonzero-charge case) and by phaseFamily_excess_bounded_of_perturbationWitness, thereby closing the quantitative bridge needed for the refined Axiom 2 in the Defect Sampled Trace module. The result sits inside the larger program that replaces the original all-mesh quantification with control on the canonical phase-sampled family.
scope and limits
- Does not construct or guarantee the existence of any RingRegularErrorBound.
- Does not produce an explicit numerical value for the excess bound $K$.
- Does not apply to families that are not realized from a DefectPhaseFamily.
- Does not address the case of zero charge (handled separately downstream).
Lean usage
theorem canonicalDefectSampledFamily_excess_bounded (sensor : DefectSensor) (hm : sensor.charge ≠ 0) : RealizedDefectAnnularExcessBounded (canonicalDefectSampledFamily sensor hm) := realizedDefectAnnularExcessBounded_of_ringRegularErrorBound _ (canonicalDefectSampledFamily_ringRegularErrorBound sensor hm)formal statement (Lean)
242theorem realizedDefectAnnularExcessBounded_of_ringRegularErrorBound
243 (fam : DefectSampledFamily) (hreg : RingRegularErrorBound fam) :
244 RealizedDefectAnnularExcessBounded fam := by
proof body
Term-mode proof.
245 obtain ⟨K, hK⟩ := hreg.total_error_bounded
246 refine ⟨K, ?_⟩
247 intro N
248 exact le_trans
249 (annularExcess_le_sum_of_ringCost_le_topologicalFloor_plus_regularError fam hreg N)
250 (hK N)
251
252/-- A uniform total-cost bound immediately gives a uniform excess bound, since
253the topological floor is nonnegative. -/