RingPerturbationControl
RingPerturbationControl equips a DefectSampledFamily with two quantitative bounds on ring increments. The smallness field keeps each deviation from the pure winding increment inside the unit-scale regime after scaling by log phi, while total_bounded ensures the summed realized perturbation errors remain uniformly controlled over all refinement depths N. Analysts working on the zeta defect would cite this package as the precise analytic input required to obtain a ring-regular-error bound after the phiCost linearization step. The declaration is a
claimLet fam be a DefectSampledFamily. Then RingPerturbationControl fam is the structure whose small field requires that for all N, n, j the quantity |log φ ⋅ ((fam.mesh N).rings n).increments j − (−2π ⋅ charge / (8(n+1)))| is at most 1, and whose total_bounded field asserts the existence of a real K such that the sum over n of realizedRingPerturbationError fam N n is ≤ K for every N.
background
The DefectSampledTrace module packages realized annular meshes arising from phase sampling of ζ^{-1} near a hypothetical defect. A DefectSampledFamily consists of a DefectSensor, a mesh function that assigns an AnnularMesh at each depth N, and a charge_spec ensuring the mesh charge matches the sensor at every level. This construction replaces the stronger universal quantification over all AnnularMesh objects with the concrete family needed for the refined Axiom 2 statement. Upstream constants supply phi (the self-similar fixed point) and the integration gap A = 1; the module doc states that any uniform upper bound on the cost of this realized family contradicts annular coercivity when charge is nonzero.
proof idea
This is a structure definition with an empty proof body. It directly declares the two fields small and total_bounded. Downstream instantiations apply the lemma regular_perturbation_small from a DefectPhasePerturbationWitness to populate the small field and then verify the summed error bound by direct summation.
why it matters in Recognition Science
RingPerturbationControl is the interface that converts a phase-family perturbation witness into the RingRegularErrorBound required for annular-excess control. It is used by canonicalDefectSampledFamily_ringPerturbationControl (the quantitative target for the Axiom 2 attack) and by ringRegularErrorBound_of_ringPerturbationControl to produce the error package. In the Recognition framework it supplies the remaining analytic input after the perturbative phiCost reduction, advancing the bridge from the canonical sampled family to the claim that nonzero charge forces cost to infinity.
scope and limits
- Does not prove existence of an instance for any concrete family.
- Does not supply an explicit numerical value for the bound K.
- Does not extend the control to the full annular cost functional.
- Does not address the zero-charge case.
formal statement (Lean)
171structure RingPerturbationControl (fam : DefectSampledFamily) where
172 small : ∀ N : ℕ, ∀ n : Fin N, ∀ j : Fin (8 * (n.val + 1)),
173 |Real.log Constants.phi *
174 (((fam.mesh N).rings n).increments j -
175 (-(2 * Real.pi * ((fam.mesh N).charge : ℝ)) / (8 * (n.val + 1) : ℝ)))| ≤ 1
176 total_bounded : ∃ K : ℝ, ∀ N : ℕ,
177 ∑ n : Fin N, realizedRingPerturbationError fam N n ≤ K
178
179/-- A perturbation-control package yields the ring-regular-error package needed
180for bounded annular excess. -/