sum_epsilon_abs_bound
The theorem bounds the summed absolute phase perturbations from the regular analytic factor over 8(n+1) angular samples at refinement level n+1. Researchers controlling error terms in zeta-derived phase families within Recognition Science cite it when establishing summable linear-plus-quadratic perturbations. The proof applies the per-sample bound epsilon_abs_bound to obtain a uniform constant B, sums over the finite index set, and simplifies the resulting expression by field arithmetic.
claimLet $M$ be the logarithmic-derivative bound and $R$ the radius of a QuantitativeLocalFactorization. For each $n$, the sum of absolute sample increments of the regular factor phase at level $n+1$ satisfies $$sum_{j=0}^{8(n+1)-1} |ε_j| ≤ M R · 2π / (n+2),$$ where each $ε_j$ is the phase increment at angular spacing $2π/(8(n+1))$.
background
The MeromorphicCircleOrder module translates Mathlib meromorphic-order data into the Recognition Science annular-cost setting. A QuantitativeLocalFactorization extends LocalMeromorphicWitness by a uniform bound $M$ on $|g'/g|$ for the regular factor $g$ in the local factorization $f(z)=(z-ρ)^k g(z)$, together with a perturbation-regime condition $M R ≤ 1$. This supplies the analytic control on phase increments $ε_j$ sampled on circles around a zero or pole. The module records that for $ζ^{-1}$ the meromorphic order $-m$ produces phase charge $m$, matching the DefectSensor.charge convention. The immediate upstream lemma epsilon_abs_bound supplies the individual estimate $|ε_j| ≤ M · (R/(n+2)) · (2π/(8(n+1)))$.
proof idea
The proof defines an auxiliary real $B = M · (R/(n+2)) · (2π/(8(n+1)))$. It invokes epsilon_abs_bound via simpa to show every sample increment is at most $B$. The sum is then bounded by $8(n+1)·B$ using Finset.sum_le_sum. Algebraic reduction with positivity lemmas, field_simp and ring converts the product back to the target $M R 2π/(n+2)$.
why it matters in Recognition Science
The result is used by genuineZetaDerivedPhasePerturbationWitness to certify that the perturbation terms of the genuine zeta-derived phase family remain small in the log-φ scale. It supplies the uniform summability needed for the linear and quadratic error controls inside RingPerturbationControl. In the broader framework it closes the analytic step that lets meromorphic order at a zero translate directly into the phase-charge input for defect-phase families, consistent with the eight-tick octave and J-cost minimization.
scope and limits
- Does not supply explicit numerical values for the logDerivBound or radius.
- Does not treat non-uniform or higher-derivative bounds on the regular factor.
- Does not bound the pure winding contribution from the pole term.
- Applies only inside the perturbation regime $M R ≤ 1$.
formal statement (Lean)
555private theorem sum_epsilon_abs_bound
556 (qlf : QuantitativeLocalFactorization) {N : ℕ} (n : Fin N) :
557 ∑ j : Fin (8 * (n.val + 1)),
558 |(genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
559 (n.val + 1) j| ≤
560 qlf.logDerivBound * qlf.radius * (2 * π) / (↑(n.val) + 2) := by
proof body
Tactic-mode proof.
561 let B : ℝ :=
562 qlf.logDerivBound * (qlf.radius / (↑(n.val + 1) + 1)) *
563 (2 * π / (8 * ↑(n.val + 1)))
564 have hB : ∀ j : Fin (8 * (n.val + 1)),
565 |(genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
566 (n.val + 1) j| ≤ B := by
567 intro j
568 simpa [B] using epsilon_abs_bound qlf (n.val + 1) (Nat.succ_pos n.val) j
569 calc
570 ∑ j : Fin (8 * (n.val + 1)),
571 |(genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
572 (n.val + 1) j|
573 ≤ ∑ _j : Fin (8 * (n.val + 1)), B := by
574 apply Finset.sum_le_sum
575 intro j _
576 exact hB j
577 _ = (8 * (n.val + 1) : ℝ) * B := by
578 rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
579 norm_num [Nat.cast_add, Nat.cast_mul]
580 _ = qlf.logDerivBound * qlf.radius * (2 * π) / (↑(n.val) + 2) := by
581 have h8n : (8 * ((n.val : ℝ) + 1)) ≠ 0 := by positivity
582 have hn2 : (n.val : ℝ) + 2 ≠ 0 := by positivity
583 simp [B, Nat.cast_add]
584 field_simp [h8n, hn2]
585 ring
586
587/-- Bound on the inner j-sum of epsilon² at level n+1. -/