zetaDerivedPhasePerturbationWitness
plain-language theorem explainer
This definition equips the zeta-derived phase family with a zero-perturbation witness, confirming that its sampled increments coincide exactly with the pure winding increments from the defect charge. Researchers applying annular cost bounds to the Riemann hypothesis would cite it to establish the base case before introducing regular-factor errors. The construction sets the perturbation function to zero and verifies the witness fields by direct unfolding followed by field simplification and ring arithmetic.
Claim. Let $σ$ be a defect sensor recording the multiplicity of a zero of $ζ$ and let $Q$ be a quantitative local factorization of $ζ^{-1}$ whose order equals the negative of the charge of $σ$. The associated zeta-derived phase family admits a defect phase perturbation witness whose regular perturbation term $ε$ is identically zero.
background
A DefectSensor at a point $ρ$ records the multiplicity $m$ of a zero of $ζ$ (hence the order of the pole of $ζ^{-1}$) together with the real part of $ρ$. QuantitativeLocalFactorization extends a local meromorphic witness by a uniform bound $M$ on $|g'/g|$ of the regular factor $g$ over a disk, together with the regime condition $M·r ≤ 1$ that keeps perturbations small on sampled circles. DefectPhasePerturbationWitness packages the data needed for RingPerturbationControl: an epsilon function, the splitting of each sampled increment into pure winding plus epsilon, the smallness condition $|log φ · ε| ≤ 1$, and summability of the induced linear and quadratic error terms. The module bridges Mathlib meromorphic order to the RS annular-cost setting by showing that the phase charge of $ζ^{-1}$ equals the defect charge, so that the pure winding term matches defectPhasePureIncrement exactly when the regular factor contributes zero perturbation.
proof idea
The definition constructs the witness by setting epsilon to the constant-zero function. The increment_eq field is discharged by unfolding zetaDerivedPhaseFamily, zetaDerivedPhaseData, ContinuousPhaseData.sampleIncrements and defectPhasePureIncrement, then applying field_simp on the nonzero denominator 8n followed by ring. The small, linear_term_bounded and quadratic_term_bounded fields hold by immediate simplification once epsilon vanishes.
why it matters
This supplies the zero-perturbation base case for the zeta-derived phase family, which is invoked directly by zetaDerivedPhaseFamily_excess_zero to prove that annular excess vanishes on every mesh depth. It sits inside the eight-tick octave structure (T7) and the phase-charge matching required for the RH application in the meromorphic circle order module. The construction closes the pure-winding case before the general regular-factor perturbation lemmas are applied downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.