zetaDerivedPhaseFamily
plain-language theorem explainer
The definition constructs a defect phase family by packaging a defect sensor with phase data extracted from a quantitative local factorization of a meromorphic function near a pole or zero. Researchers working on analytic proofs of the Riemann hypothesis would cite it to obtain families whose charge matches the multiplicity of zeta zeros. The construction is a direct record definition that sets the sensor and radius fields from the inputs and delegates phase computation while verifying uniform charge via the order matching hypothesis.
Claim. Let $S$ be a defect sensor with charge $m$ and let $Q$ be a quantitative local factorization with order $-m$. The associated defect phase family has sensor $S$, witness radius equal to the radius of $Q$, phase data at each level $n$ extracted from $Q$, and charge uniformly equal to $m$ at every level.
background
A defect sensor records an integer charge (the multiplicity of a zero of the zeta function), the real part of its location, and the condition that the zero lies in the right half of the critical strip. A quantitative local factorization extends a local meromorphic witness by adding a positive bound $M$ on the logarithmic derivative of the regular factor $g$ together with the regime condition $M$ times radius at most 1; this bound controls phase perturbations on sampled circles. The defect phase family structure requires a sensor, a positive witness radius, a map sending each positive integer level to continuous phase data, and a uniformity proof that every such datum carries charge exactly equal to the sensor charge. In the setting of the meromorphic circle order module this bridges Mathlib meromorphic-order machinery to the recognition science annular cost framework: for the reciprocal of zeta at a zero of multiplicity $m$ the phase charge equals $m$, matching the defect sensor. From the module documentation: a meromorphic function $f$ with meromorphic order $n$ at $ρ$ admits the local factorization $f(z)=(z-ρ)^n g(z)$ with $g$ analytic and nonvanishing at $ρ$; on a small circle the phase charge of $f$ is $-n$.
proof idea
The definition is a direct record construction. It assigns the input sensor to the sensor field, copies the radius and radius positivity from the quantitative local factorization, sets the phase-at-level map to the zeta-derived phase data function, and establishes the charge-uniformity property by invoking the charge theorem for that data and rewriting with the order hypothesis to cancel the negation.
why it matters
This definition supplies the concrete phase family required by the honest argument principle phase family theorem to realize the argument principle for zeta reciprocal using genuine factorization data. It is the input to the zeta-derived phase family excess zero theorem, which establishes that annular excess vanishes identically, and to the genuine zeta-derived phase perturbation witness for controlling perturbations. Within the recognition science framework it supplies the non-scaffolding phase data that connects meromorphic order to defect charge, enabling the honest phase budget bridge and supporting the path to unified RH statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.