regular_perturbation_quadratic_term_bounded
plain-language theorem explainer
The declaration supplies a uniform real bound K on the summed quadratic phiCost contributions from regular-factor perturbations epsilon across refinement levels in any defect phase family. Recognition Science researchers controlling excess annular cost for the Axiom 2 attack would cite it when assembling RingPerturbationControl witnesses. The proof is a direct one-line projection of the quadratic_term_bounded field already stored inside the DefectPhasePerturbationWitness hypothesis.
Claim. Let dpf be a DefectPhaseFamily and hw a DefectPhasePerturbationWitness for dpf. Then there exists a real constant K such that for every natural number N,
background
A DefectPhaseFamily consists of a DefectSensor together with a radius and a level-indexed family of ContinuousPhaseData whose charge equals the sensor charge at every n. The companion DefectPhasePerturbationWitness records, for each level n and each of the 8n samples, a regular perturbation epsilon such that the observed increment equals the pure winding increment plus epsilon, with the smallness condition |log phi * epsilon| <= 1 already enforced. The witness further packages explicit linear and quadratic bounds on the resulting phiCost increments. The module uses these structures to translate Mathlib meromorphic-order factorizations of zeta inverse into the annular-cost language of Recognition Science, where the regular factor g supplies the epsilon terms on 8-tick circles. Upstream constants include K defined as phi to the power 1/2 and the eight-tick phase map.
proof idea
The proof is the one-line term application of the quadratic_term_bounded field carried by the DefectPhasePerturbationWitness hypothesis hw.
why it matters
The bound is invoked by phaseFamily_ringPerturbationControl to produce the RingPerturbationControl package required by the annular-cost machinery, and by canonicalDefectSampledFamily_ringPerturbationControl to close the quantitative Axiom 2 target. It therefore supplies one of the two summability conditions needed to guarantee that the total perturbation cost above the topological floor remains finite independently of sampling depth N. The result sits inside the perturbation lemmas that connect local meromorphic factorization to the phi-ladder cost estimates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.