sum_epsilon_sq_bound
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assert that the bound is attained for any concrete meromorphic function.
- Does not apply when the perturbation regime condition fails.
- Does not control higher-order terms beyond the quadratic contribution.
- Does not address global meromorphic functions outside a single disk.
formal statement (Lean)
588theorem sum_epsilon_sq_bound
589 (qlf : QuantitativeLocalFactorization) {N : ℕ} (n : Fin N) :
590 ∑ j : Fin (8 * (n.val + 1)),
591 ((genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
592 (n.val + 1) j) ^ 2 ≤
593 qlf.logDerivBound ^ 2 * qlf.radius ^ 2 * (2 * π) ^ 2 /
594 (8 * (↑(n.val) + 1) * (↑(n.val) + 2) ^ 2) := by
proof body
Tactic-mode proof.
595 let B : ℝ :=
596 qlf.logDerivBound * (qlf.radius / (↑(n.val + 1) + 1)) *
597 (2 * π / (8 * ↑(n.val + 1)))
598 have hB_nonneg : 0 ≤ B := by
599 have hlog_nonneg : 0 ≤ qlf.logDerivBound := le_of_lt qlf.logDerivBound_pos
600 have hr_nonneg : 0 ≤ qlf.radius := le_of_lt qlf.radius_pos
601 have hdiv1 : 0 ≤ qlf.radius / (↑(n.val + 1) + 1) := by
602 exact div_nonneg hr_nonneg (by positivity)
603 have hdiv2 : 0 ≤ 2 * π / (8 * ↑(n.val + 1)) := by
604 exact div_nonneg (by positivity) (by positivity)
605 dsimp [B]
606 exact mul_nonneg (mul_nonneg hlog_nonneg hdiv1) hdiv2
607 have hBsq : ∀ j : Fin (8 * (n.val + 1)),
608 ((genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
609 (n.val + 1) j) ^ 2 ≤ B ^ 2 := by
610 intro j
611 have hj := epsilon_abs_bound qlf (n.val + 1) (Nat.succ_pos n.val) j
612 have hj' :
613 |(genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
614 (n.val + 1) j| ≤ B := by
615 simpa [B] using hj
616 have hBabs : |B| = B := abs_of_nonneg hB_nonneg
617 exact (sq_le_sq).2 (by simpa [hBabs] using hj')
618 calc
619 ∑ j : Fin (8 * (n.val + 1)),
620 ((genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
621 (n.val + 1) j) ^ 2
622 ≤ ∑ _j : Fin (8 * (n.val + 1)), B ^ 2 := by
623 apply Finset.sum_le_sum
624 intro j _
625 exact hBsq j
626 _ = (8 * (n.val + 1) : ℝ) * B ^ 2 := by
627 rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
628 norm_num [Nat.cast_add, Nat.cast_mul]
629 _ = qlf.logDerivBound ^ 2 * qlf.radius ^ 2 * (2 * π) ^ 2 /
630 (8 * (↑(n.val) + 1) * (↑(n.val) + 2) ^ 2) := by
631 have h8n : (8 * ((n.val : ℝ) + 1)) ≠ 0 := by positivity
632 have hn2 : (n.val : ℝ) + 2 ≠ 0 := by positivity
633 simp [B, Nat.cast_add]
634 field_simp [h8n, hn2]
635 ring
636
637/-- `Real.sinh` is convex on `[0, ∞)`. -/