regular_perturbation_linear_term_bounded
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.