sum_epsilon_sq_bound
plain-language theorem explainer
A bound is derived on the sum of squared regular-factor phase increments over the 8(k) sample points at each refinement depth k. Workers controlling quadratic errors in zeta-derived defect phase families cite this when closing summability estimates for annular costs. The argument invokes the per-increment absolute bound to cap every term by an auxiliary B, sums the resulting B squared terms, and reduces the expression by direct algebraic simplification.
Claim. Let $M$ and $R$ be the logarithmic-derivative bound and radius of a QuantitativeLocalFactorization. For each natural number $k = n+1$, the sum of squared phase increments $ε_j$ of the regular factor on the sampled circle satisfies $∑_{j ∈ Fin(8k)} ε_j² ≤ M² R² (2π)² / (8k (k+1)²).
background
The MeromorphicCircleOrder module translates meromorphic orders into phase charges for the Recognition Science annular-cost framework. A local factorization around a pole or zero separates the winding contribution from the regular holomorphic factor g, whose logarithmic derivative is bounded by M over the disk. This yields small phase perturbations ε_j on angular samples spaced by 2π/(8k). QuantitativeLocalFactorization packages the witness with the explicit bound M together with the regime condition M R ≤ 1. The upstream result epsilon_abs_bound supplies the individual estimate |ε_j| ≤ M R (2π) / (8k (k+1)) at level k. The module doc notes that for the inverse zeta function the phase charge of the regular factor is zero, so all net charge arises from the pole term.
proof idea
An auxiliary quantity B is defined as the right-hand side of the per-increment bound. Non-negativity of B follows from positivity of M and R. Each squared increment is then bounded by B squared via the absolute-value form of the epsilon_abs_bound lemma and the inequality x² ≤ y² for |x| ≤ |y|. The sum is estimated by replacing each term with B² and using the cardinality of the finite set of indices, after which the algebraic identity 8k B² equals the target expression is verified by field simplification and ring normalization.
why it matters
The bound closes the quadratic-error control inside DefectPhasePerturbationWitness for genuine zeta-derived families and is applied in the carrier-excess theorem for shared-circle pairs. It thereby supplies the missing summability step that lets the perturbation lemmas feed into RingPerturbationControl. Within the broader framework the result ensures that regular-factor contributions remain compatible with the eight-tick octave sampling and the phi-ladder scaling of costs. It leaves open the question of whether sharper constants can be obtained by exploiting further analytic properties of the zeta function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.