realizedRingPerturbationError
plain-language theorem explainer
The definition assembles the explicit linear-plus-quadratic error for one ring inside a realized defect-sampled annular family, using the pure winding increment derived from charge and the phiCost coefficients on summed deviations. Researchers working on the refined Axiom 2 attack cite it to convert RingPerturbationControl into a concrete RingRegularErrorBound. The body is a direct algebraic expression that evaluates the error once the increments are written as pure winding plus regular perturbation.
Claim. For a defect-sampled family with mesh at depth $N$ and ring index $n$, let $u = -2π q / (8(n+1))$ where $q$ is the mesh charge. The realized ring perturbation error equals the linear coefficient of phiCost at $|u|$ times the sum of absolute deviations of the increments from $u$, plus the quadratic coefficient at $|u|$ times the sum of squared deviations, the sums running over the $8(n+1)$ increments of that ring.
background
DefectSampledFamily packages a sensor together with a family of realized AnnularMesh objects whose charges match the sensor; it arises from the phase-sampling construction for $ζ^{-1}$ near a hypothetical defect rather than from an arbitrary mesh. The module sits after the elimination of Axiom 1 and supplies the concrete family needed to attack Axiom 2 by showing that nonzero charge forces annular cost to infinity. Upstream, PhiForcingDerived supplies the J-cost structure whose linear and quadratic coefficients appear here; the pure winding increment $u$ is the topological floor term delivered by ringCost_le_topologicalFloor_add_linear_quadratic_error once increments are decomposed as pure winding plus perturbation.
proof idea
The definition is a direct algebraic expression. It first computes the pure winding increment $u$ from the mesh charge and the ring index, then multiplies the linear and quadratic coefficients of phiCost evaluated at $|u|$ by the respective summed absolute and squared deviations of the actual increments from $u$ over the eight-tick octave.
why it matters
This supplies the concrete error term consumed by ringRegularErrorBound_of_ringPerturbationControl to produce RingRegularErrorBound and by canonicalDefectSampledFamily_ringPerturbationControl to close the quantitative target for the Axiom 2 attack. It therefore sits inside the DefectSampledTrace layer that converts the phase-sampling construction into a uniform bound on excess above the topological floor. The construction touches the eight-tick octave and the Recognition Composition Law through the phiCost reduction that precedes it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.