canonicalDefectSampledFamily_ringRegularErrorBound
The declaration yields the ring-regular error bound for the canonical defect sampled family attached to any nonzero-charge defect sensor. Analysts bounding the cost of realized zeta-defect meshes would cite it to obtain uniform control on regular-part errors across all sampling depths. It is a direct one-line wrapper that invokes the conversion from ring perturbation control.
claimLet $s$ be a defect sensor with charge $m ≠ 0$. Let $F$ be the canonical sampled family attached to $s$. Then $F$ satisfies the ring-regular error bound: there exist error terms $e(N,n)$ such that for every depth $N$ and ring index $n$, the ring cost of the $n$-th ring at depth $N$ is at most the topological floor for charge $m$ plus $e(N,n)$, and the sum of errors over rings is bounded by a constant independent of $N$.
background
The Defect Sampled Trace module builds realized annular meshes from the phase-sampling construction for a hypothetical zeta defect. A DefectSensor records the multiplicity $m$ of a zero of $ζ$ (equivalently the order of the pole of $ζ^{-1}$) together with its real part; the sensor is required to lie in the right half of the critical strip. The canonicalDefectSampledFamily is the sampled family obtained by converting the chosen defect phase family for that sensor into a full refinement family of meshes.
proof idea
The definition is a one-line wrapper that applies ringRegularErrorBound_of_ringPerturbationControl to the RingPerturbationControl package returned by canonicalDefectSampledFamily_ringPerturbationControl for the given sensor and charge hypothesis.
why it matters in Recognition Science
This declaration supplies the RingRegularErrorBound instance required by the downstream theorem canonicalDefectSampledFamily_excess_bounded, which establishes RealizedDefectAnnularExcessBounded for the canonical family. It therefore closes the quantitative step that converts local factorization bounds into the uniform error control needed to attack Axiom 2: any uniform upper bound on the cost of the realized sampled family would contradict annular coercivity when charge is nonzero.
scope and limits
- Does not establish the underlying ring perturbation control.
- Applies only when the sensor charge is nonzero.
- Does not supply explicit numerical values for the error constant K.
- Does not address the full annular cost, only the regular-part error component.
formal statement (Lean)
432noncomputable def canonicalDefectSampledFamily_ringRegularErrorBound (sensor : DefectSensor)
433 (hm : sensor.charge ≠ 0) :
434 RingRegularErrorBound (canonicalDefectSampledFamily sensor hm) := by
proof body
Definition body.
435 exact ringRegularErrorBound_of_ringPerturbationControl _
436 (canonicalDefectSampledFamily_ringPerturbationControl sensor hm)
437