genuineZetaDerivedPhasePerturbationWitness
plain-language theorem explainer
The definition equips the genuine zeta-derived phase family with a full perturbation witness consisting of regular increments, exact split from pure winding terms, smallness in the log phi scale, and an explicit linear cost bound. Analysts verifying summability for sampled phase data in the annular cost framework cite it when building ring perturbation control for meromorphic functions. The construction proceeds by direct substitution of sample increments from the quantitative factorization followed by algebraic verification and sinh scaling.
Claim. Let $S$ be a defect sensor with integer charge $m$ and let $Q$ be a quantitative local factorization of order $-m$. The genuine zeta-derived phase family $F$ associated to $S$ and $Q$ admits a perturbation witness in which the regular increments satisfy $|log phi · epsilon_{n,j}| ≤ 1$, the sampled increments equal the pure defect increment plus epsilon, and there exists $K$ such that the summed linear coefficients times absolute increments are bounded by $K ∑ 1/(n(n+1))$ for all refinement depths $N$.
background
The Meromorphic Circle Order module connects Mathlib meromorphic order at a point to the Recognition Science annular cost model. A meromorphic function with order $n$ at ρ factors locally as (z−ρ)^n g(z) with g holomorphic and nonzero at ρ; the power term contributes phase charge −n while the regular factor contributes zero charge. For the inverse zeta function at a zero of multiplicity m the order is −m, so the phase charge is m and matches the defect sensor charge.
proof idea
The witness is built by setting epsilon to the sample increments of the genuine regular factor phase at each level. Increment equality follows by unfolding the family definitions and ring simplification on the pure increment. Smallness is taken from the perturbation regime of the quantitative factorization together with log phi < 1. The linear term bound is obtained by exhibiting an explicit K proportional to log phi · sinh(A) with A = log phi · (π |m|/4), proving nonnegativity of all factors, and applying the scaled inequality sinh(t x) ≤ t sinh x for t ≤ 1 together with the 1/(n(n+1)) decay of the pure increment.
why it matters
This definition supplies the key analytic input for canonical defect sampled family ring perturbation control in the module. It thereby enables the Recognition Science application to the Riemann hypothesis via phase charge matching at zeta zeros. The construction relies on the eight-tick octave sampling and phi-ladder cost structure, with the linear bound ensuring the error series converges uniformly in refinement depth. It closes the local factorization step required for global summability estimates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.