realizedRingPerturbationError
The definition computes the explicit linear-plus-quadratic perturbation error on one ring of a realized defect-sampled annular family. Researchers attacking the refined Axiom 2 for the zeta defect cite it when converting sampled increments into bounded excess above the topological floor. It is obtained by extracting the pure winding increment u from the mesh charge and then weighting the summed absolute and squared deviations by the linear and quadratic coefficients of phiCost evaluated at |u|.
claimLet $u = -2π q / (8(n+1))$ where $q$ is the charge of the mesh at refinement depth $N$. For a DefectSampledFamily $fam$, the realized ring perturbation error at ring $n$ is $L(|u|) ∑ |Δ_j - u| + Q(|u|) ∑ (Δ_j - u)^2$, where $L$ and $Q$ are the linear and quadratic coefficients of the phiCost function, and the $Δ_j$ are the increments of the $n$-th ring.
background
A DefectSampledFamily packages a defect sensor together with a family of annular meshes indexed by refinement depth $N$, each mesh carrying exactly the sensor charge. The construction samples the phase of $ζ^{-1}$ near a hypothetical defect rather than ranging over arbitrary meshes. The module supplies the concrete objects needed once Axiom 1 is eliminated, so that the remaining task is to bound the cost of the canonical sampled family and thereby contradict annular coercivity for nonzero charge.
proof idea
Direct definition. It first forms the pure winding increment $u$ from the charge and the number of increments $8(n.val+1)$, then evaluates the linear coefficient of phiCost at |u| against the sum of absolute deviations and the quadratic coefficient against the sum of squared deviations.
why it matters in Recognition Science
The definition supplies the concrete error term that RingPerturbationControl packages and that ringRegularErrorBound_of_ringPerturbationControl converts into a RingRegularErrorBound. It is invoked inside canonicalDefectSampledFamily_ringPerturbationControl, the quantitative target for the Axiom 2 attack. In the Recognition framework it operationalizes the perturbative reduction of ringCost around the topological floor using the phi-cost derived from the functional equation, advancing the bridge from local factorization of $ζ^{-1}$ to uniform annular bounds.
scope and limits
- Does not prove the error sums are bounded; that is the content of RingPerturbationControl.
- Does not apply to arbitrary AnnularMesh families, only to those realized from a DefectSampledFamily.
- Does not compute the full annular cost, only the perturbation component on a single ring.
- Does not depend on global constants beyond the phiCost coefficients.
Lean usage
realizedRingPerturbationError fam N nformal statement (Lean)
151noncomputable def realizedRingPerturbationError (fam : DefectSampledFamily)
152 (N : ℕ) (n : Fin N) : ℝ :=
proof body
Definition body.
153 let u : ℝ := -(2 * Real.pi * ((fam.mesh N).charge : ℝ)) / (8 * (n.val + 1) : ℝ)
154 phiCostLinearCoeff |u| *
155 ∑ j : Fin (8 * (n.val + 1)),
156 |((fam.mesh N).rings n).increments j - u| +
157 phiCostQuadraticCoeff |u| *
158 ∑ j : Fin (8 * (n.val + 1)),
159 (((fam.mesh N).rings n).increments j - u) ^ 2
160
161/-- Quantitative perturbation control for a realized sampled family.
162
163The `small` field says each sampled increment stays within the unit-scale
164perturbative regime of `phiCost` once expressed as
165
166`Δ_j = (pure winding increment) + ε_j`.
167
168The `total_bounded` field says the resulting linear-plus-quadratic error sums
169are uniformly bounded across refinement depth `N`. This is exactly the remaining
170analytic input needed after the perturbative `phiCost` reduction. -/