pith. machine review for the scientific record. sign in
structure definition def or abbrev high

ZetaPhaseFamilyData

show as:
view Lean formalization →

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.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 965structure ZetaPhaseFamilyData where
 966  sensor : DefectSensor
 967  witness : QuantitativeLocalFactorization
 968  witness_realPart : witness.center.re = sensor.realPart
 969  witness_order : witness.order = -sensor.charge
 970  phaseFamily : DefectPhaseFamily
 971  family_sensor : phaseFamily.sensor = sensor
 972  family_derived : phaseFamily = zetaDerivedPhaseFamily sensor witness witness_order
 973
 974/-- Any honest zeta phase-family package carries the canonical zero-perturbation
 975witness attached to its derived phase family. -/
 976noncomputable def ZetaPhaseFamilyData.perturbationWitness
 977    (zfd : ZetaPhaseFamilyData) :
 978    DefectPhasePerturbationWitness zfd.phaseFamily := by

proof body

Definition body.

 979  simpa [zfd.family_derived] using
 980    zetaDerivedPhasePerturbationWitness zfd.sensor zfd.witness zfd.witness_order
 981
 982end
 983
 984end NumberTheory
 985end IndisputableMonolith

used by (22)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (13)

Lean names referenced from this declaration's body.