zetaDerivedPhaseFamily
plain-language theorem explainer
Constructs a DefectPhaseFamily whose phase data on concentric circles is taken directly from the meromorphic factorization of zeta reciprocal at a zero. Analysts applying the argument principle to obtain charge equal to multiplicity cite this construction. The definition is a record that wires radius and phase function from the supplied QuantitativeLocalFactorization and proves uniform charge by one-line rewrite on the order hypothesis.
Claim. Given defect sensor $S$ with charge $m$ and quantitative local factorization $Q$ satisfying order$(Q)=-m$, there exists a defect phase family with sensor $S$, witness radius from $Q$, phase data at level $n$ taken from the factorization on the circle of radius $r_0/(n+1)$, and charge uniformly equal to $m$.
background
DefectPhaseFamily is the structure carrying a DefectSensor, a positive witness radius, a function returning ContinuousPhaseData at each refinement level, and a uniformity proof that every level carries the sensor charge. QuantitativeLocalFactorization extends a local meromorphic witness by a bound $M$ on $|g'/g|$ of the regular factor together with the regime $M imes$ radius $\le 1$. The module doc states that a meromorphic function with order $n$ at $ ho$ factors as $(z- ho)^n g(z)$ with $g$ analytic and nonvanishing, so the phase charge on small circles equals $-n$; for $\zeta^{-1}$ this yields charge $m$ matching the sensor.
proof idea
Record construction. It copies the sensor, sets witnessRadius and witnessRadius_pos from the quantitative local factorization, delegates phaseAtLevel to zetaDerivedPhaseData, and proves charge_uniform by applying zetaDerivedPhaseData_charge then rewriting with the order hypothesis and double negation.
why it matters
Supplies the genuine phase family required by honest_argument_principle_phase_family to link the argument principle to the defect sensor. It is invoked by zetaDerivedPhaseFamily_excess_zero to obtain zero annular excess and by genuineZetaDerivedPhasePerturbationWitness to control perturbations. The construction realizes the meromorphic-circle-order bridge that feeds the analytic route to the Riemann hypothesis in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.