regular_perturbation_small
The bound asserts that the regular perturbation component epsilon extracted from sampled phase increments on an 8n-grid satisfies |log phi * epsilon| <= 1. Downstream constructions of ring perturbation control for canonical defect families invoke it to license the phiCost perturbation lemma. The proof is a direct projection of the smallness field already present in the supplied perturbation witness structure.
claimLet $d$ be a defect phase family and $w$ a perturbation witness for it. For every positive integer $n$ and every index $j$ on the $8n$-point sampling grid, $|$log$phi$ $cdot$ $epsilon_n^j| le 1$, where $epsilon_n^j$ is the regular-factor perturbation in the decomposition of the $j$-th sampled increment at level $n$.
background
The module bridges Mathlib meromorphic-order machinery to the RS annular-cost framework. A meromorphic function with order $n$ at a point admits a local factorization into a pole part carrying phase charge $-n$ and a holomorphic nonvanishing regular factor carrying charge zero; the total charge is therefore $-n$. For the RS application, the inverse zeta function supplies charge equal to the multiplicity at each zero, matching the defect sensor charge. A defect phase family packages a fixed-radius witness circle together with level-dependent continuous phase data whose uniform charge equals the prescribed sensor charge. The perturbation witness decomposes every sampled increment on the $8n$-grid into a pure winding term plus a regular epsilon, and records the smallness condition together with linear and quadratic summability bounds.
proof idea
One-line wrapper that applies the smallness field of the DefectPhasePerturbationWitness.
why it matters in Recognition Science
This supplies the uniform smallness needed to close the quantitative bound on excess cost above the topological floor for the canonical defect sampled family. It is invoked inside both canonicalDefectSampledFamily_ringPerturbationControl and phaseFamily_ringPerturbationControl to construct the RingPerturbationControl witness required by the annular-cost machinery. The construction targets the Axiom 2 attack by keeping regular perturbations inside the unit-scale regime for the phiCost lemma, consistent with the eight-tick octave sampling grid and the log-phi scaling native to the Recognition framework.
scope and limits
- Does not prove existence of a DefectPhasePerturbationWitness for a given defect phase family.
- Does not bound the summed linear or quadratic error terms over refinement depth.
- Does not derive the smallness from the underlying meromorphic factorization.
- Does not address the total boundedness clause of the downstream RingPerturbationControl.
Lean usage
have hsmall := regular_perturbation_small hw (n.val + 1) (Nat.succ_pos n.val) jformal statement (Lean)
196theorem regular_perturbation_small
197 {dpf : DefectPhaseFamily} (hw : DefectPhasePerturbationWitness dpf)
198 (n : ℕ) (hn : 0 < n) (j : Fin (8 * n)) :
199 |Real.log Constants.phi * hw.epsilon n hn j| ≤ 1 :=
proof body
Term-mode proof.
200 hw.small n hn j
201
202/-- Uniform bound for the linear perturbation budget. -/