ringRegularErrorBound_of_ringPerturbationControl
The definition assembles a RingRegularErrorBound structure for a DefectSampledFamily once a RingPerturbationControl package is supplied. Researchers bounding annular excess for the canonical phase-sampled family attached to a zeta defect cite it to convert perturbation data into the required error package. It proceeds by direct structure construction that invokes the ring cost inequality after verifying the small-increment hypothesis on each ring.
claimGiven a defect-sampled family $fam$ and a perturbation control $hctrl$ for $fam$, define the regular error bound package whose error function on each ring is the realized perturbation error, whose ring cost satisfies ringCost((fam.mesh N).rings n) ≤ topologicalFloor(n.val + 1, charge) + error N n, and whose total summed error remains uniformly bounded in depth N.
background
In the Defect Sampled Trace module a DefectSampledFamily is a realized structure consisting of a defect sensor, a depth-indexed family of annular meshes, and the requirement that every mesh carries exactly the sensor charge. RingPerturbationControl supplies two quantitative conditions: each sampled increment on ring n deviates from the pure winding increment by at most unit scale in the phi-cost metric, and the summed realized ring errors admit a uniform upper bound independent of depth. RingRegularErrorBound packages the resulting per-ring error function together with the inequality ringCost ≤ topologicalFloor + error and the uniform bound on the sum of those errors. The module addresses the refined Axiom 2 by restricting attention to the canonical sampled family arising from the phase of ζ^{-1} near a hypothetical defect, rather than quantifying over arbitrary meshes.
proof idea
The definition constructs the target structure by setting the error field to realizedRingPerturbationError fam and the total_error_bounded field to the bound supplied by hctrl. For the ring_estimate field it first equates winding number to charge via the uniform_charge lemma, then extracts the smallness hypothesis from hctrl.small for every increment, and finally applies ringCost_le_topologicalFloor_add_linear_quadratic_error to obtain the desired inequality; the charge is rewritten and the expression is simplified using add_assoc.
why it matters in Recognition Science
This definition supplies the algebraic bridge from a perturbation-control witness to the regular-error package required for bounded annular excess. It is invoked directly by canonicalDefectSampledFamily_ringRegularErrorBound to equip the canonical family and by phaseFamily_excess_bounded_of_perturbationWitness to conclude RealizedDefectAnnularExcessBounded from a phase perturbation witness. In the Recognition framework it closes the ring-to-annulus step that supports the refined Axiom 2 for the zeta defect trace, after Axiom 1 has been eliminated.
scope and limits
- Does not prove existence of RingPerturbationControl for an arbitrary family.
- Does not supply an explicit numerical value for the uniform error bound K.
- Does not extend the bound to meshes lacking the uniform charge specification.
- Does not address the zero-charge case.
formal statement (Lean)
181noncomputable def ringRegularErrorBound_of_ringPerturbationControl
182 (fam : DefectSampledFamily) (hctrl : RingPerturbationControl fam) :
183 RingRegularErrorBound fam := by
proof body
Definition body.
184 refine
185 { error := realizedRingPerturbationError fam
186 ring_estimate := ?_
187 total_error_bounded := hctrl.total_bounded }
188 intro N n
189 have hcharge : ((fam.mesh N).rings n).winding = (fam.mesh N).charge := by
190 rw [((fam.mesh N).uniform_charge n)]
191 have hsmall_ring :
192 ∀ j : Fin (8 * n.val.succ),
193 |Real.log Constants.phi *
194 (((fam.mesh N).rings n).increments j -
195 (-(2 * Real.pi * ((((fam.mesh N).rings n).winding : ℤ) : ℝ)) /
196 (8 * n.val.succ : ℝ)))| ≤ 1 := by
197 intro j
198 have hj := hctrl.small N n j
199 simpa [hcharge, Nat.succ_eq_add_one] using hj
200 have hring :=
201 ringCost_le_topologicalFloor_add_linear_quadratic_error
202 (Nat.succ_pos n.val) ((fam.mesh N).rings n) hsmall_ring
203 rw [hcharge] at hring
204 simpa [realizedRingPerturbationError, add_assoc] using hring
205
206/-- Summing the ring-level estimate yields a bound for annular excess.
207
208This is the unconditional algebraic step:
209
210`ringCost ≤ topologicalFloor + regularError`
211
212on each ring implies
213
214`annularExcess ≤ ∑ regularError`
215
216on the full annulus. -/