regular_perturbation_linear_term_bounded
Uniform bounds on linear perturbation budgets are guaranteed for any defect phase family equipped with a quantitative witness. Analysts building ring perturbation control for the canonical defect sampled family cite this to close the linear error term in the Axiom 2 attack. The argument is a direct one-line extraction of the linear_term_bounded field packaged inside the DefectPhasePerturbationWitness structure.
claimLet $dpf$ be a defect phase family and let $hw$ be a perturbation witness for $dpf$. Then there exists a real constant $K$ such that for every natural number $N$, $$sum_{n=0}^{N-1} phiCostLinearCoeff(|defectPhasePureIncrement(dpf,n+1)|) times sum_{j=0}^{8(n+1)-1} |hw.epsilon(n+1,j)| leq K.$$
background
The MeromorphicCircleOrder module bridges Mathlib meromorphic-order machinery to the Recognition Science annular-cost framework. A DefectPhaseFamily consists of a DefectSensor together with a constant-radius phase package whose charge matches the sensor at every level; the associated DefectPhasePerturbationWitness augments this data with an epsilon field that records the deviation of each sampled increment from the pure winding increment, a smallness condition |log phi * epsilon| <= 1, and the linear_term_bounded property. The coefficient phiCostLinearCoeff(A) is the linear term in the phi-cost expansion on [-A,A], defined as log phi * sinh(log phi * A) in the AnnularCost module. The module documentation states that these perturbation lemmas guarantee the epsilons remain small in the log-phi scale so that the phiCost bound applies and the linear-plus-quadratic error remains summable uniformly in refinement depth N.
proof idea
The proof is a one-line term-mode wrapper that directly returns the linear_term_bounded field of the supplied DefectPhasePerturbationWitness.
why it matters in Recognition Science
This theorem supplies the linear half of the total_bounded requirement inside RingPerturbationControl. It is invoked by canonicalDefectSampledFamily_ringPerturbationControl, the quantitative target for the Axiom 2 attack, and by phaseFamily_ringPerturbationControl. The result closes one piece of uniform summability of perturbation budgets across refinement depths, relying on the eight-tick octave sampling and the phi-ladder structure of the cost function. The module positions these lemmas as the analytic input needed to realize bounded excess above the topological floor.
scope and limits
- Does not establish existence of a DefectPhasePerturbationWitness.
- Does not bound the quadratic perturbation terms.
- Does not apply outside the assumptions of a valid DefectPhasePerturbationWitness.
- Does not supply an explicit numerical value for the bound K.
- Does not address convergence of the partial sums as N tends to infinity beyond the stated uniform bound.
formal statement (Lean)
203theorem regular_perturbation_linear_term_bounded
204 {dpf : DefectPhaseFamily} (hw : DefectPhasePerturbationWitness dpf) :
205 ∃ K : ℝ, ∀ N : ℕ,
206 ∑ n : Fin N,
207 phiCostLinearCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
208 ∑ j : Fin (8 * (n.val + 1)),
209 |hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j| ≤ K :=
proof body
Term-mode proof.
210 hw.linear_term_bounded
211
212/-- Uniform bound for the quadratic perturbation budget. -/