ZetaPhaseFamilyData
plain-language theorem explainer
ZetaPhaseFamilyData packages a defect sensor at a hypothetical zero, a quantitative local factorization witness whose real part and order match the sensor, and the defect phase family obtained by applying the zeta-derived constructor. Analysts working on the analytic route to the Riemann hypothesis cite it to supply honest phase data for charge-zero bridges in AnalyticTrace. The perturbationWitness definition is a one-line wrapper that applies zetaDerivedPhasePerturbationWitness after unfolding the family_derived equality.
Claim. A datum for a zeta-derived phase family consists of a defect sensor $S$ recording multiplicity $m$ and real part $σ$ of a hypothetical zero, a quantitative local factorization $W$ of the reciprocal zeta function at that point satisfying $W$ center real part equals $σ$ and $W$ order equals $-m$, and a defect phase family $F$ such that $F$ sensor equals $S$ and $F$ equals the phase family derived from $S$, $W$, and the order.
background
The module bridges Mathlib meromorphic-order machinery to the Recognition Science annular cost framework. For a meromorphic function with order $n$ at $ρ$, the local factorization $f(z)=(z-ρ)^n g(z)$ yields phase charge $-n$ from the pole part and charge $0$ from the regular factor $g$; for $ζ^{-1}$ at a zero of multiplicity $m$ this produces charge $m$, matching the defect sensor. A DefectSensor records the charge (multiplicity of the zero) and real part of the location in the critical strip. QuantitativeLocalFactorization extends a local meromorphic witness with a positive bound $M$ on the logarithmic derivative of the regular factor over the disk, together with the regime condition $M·radius≤1$ that controls phase perturbations $ε_j$ on sampled circles. DefectPhaseFamily packages a sensor, positive witness radius, and level-dependent continuous phase data whose charge is uniform and equals the sensor charge.
proof idea
The structure is a definition whose fields directly record the sensor, witness, matching conditions, and derived family. The perturbationWitness definition is a one-line wrapper: after substituting the family_derived equality it applies zetaDerivedPhasePerturbationWitness to the sensor, witness, and order.
why it matters
This declaration supplies the honest zeta phase-family data required by the charge-zero bridges in AnalyticTrace (HonestPhaseChargeZeroBridge, HonestPhaseCostBridge, VectorCChargeZeroBridge) and by the direct RH from zero-free criterion theorem. It connects the meromorphic order factorization to the phase charge that matches defect charge, supporting the eight-tick octave sampling and annular cost model in the Recognition framework. It leaves open the explicit construction of such data for actual zeros of zeta.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.