genuineZetaDerivedPhaseFamily
plain-language theorem explainer
genuineZetaDerivedPhaseFamily assembles a DefectPhaseFamily from a defect sensor and quantitative local factorization whose order matches the negated sensor charge. Researchers applying annular cost bounds to zeta zeros cite it to obtain phase data carrying non-zero regular-factor perturbations. The definition is a direct record that delegates phase computation to genuineZetaDerivedPhaseData and enforces charge uniformity by a single negation rewrite.
Claim. Let $S$ be a defect sensor with integer charge $m$ and let $Q$ be a quantitative local factorization whose order equals $-m$. The genuine zeta-derived phase family is the defect phase family whose sensor field is $S$, whose witness radius is the radius of $Q$, whose phase at level $n$ is supplied by the genuine zeta-derived phase data at that level, and whose charge is uniformly $m$ at every level.
background
DefectPhaseFamily packages a defect sensor, a positive witness radius, a map from positive integers to continuous phase data, and a uniformity axiom requiring that every level carries exactly the sensor charge. QuantitativeLocalFactorization extends a local meromorphic witness by a positive bound on the logarithmic derivative of the regular factor together with the regime condition that this bound times the radius is at most one. DefectSensor records the integer charge (multiplicity of the corresponding zeta zero) and the real part of its location in the critical strip.
proof idea
The declaration is a definition that directly populates the DefectPhaseFamily record. It copies the supplied sensor, sets the witness radius to the factorization radius, and defines phaseAtLevel by calling genuineZetaDerivedPhaseData. The charge_uniform field is discharged by a one-line tactic block that invokes genuineZetaDerivedPhaseData_charge, rewrites with the order hypothesis, and applies negation.
why it matters
This definition supplies the genuine (non-synthetic) phase family consumed by mkSharedCirclePair in CarrierBudgetComparison and by genuineZetaDerivedPhasePerturbationWitness inside the same module. It supplies the concrete regular-factor perturbation data needed for the annular-cost perturbation lemmas that support the Riemann-hypothesis application of meromorphic order to zeta zeros. The construction sits inside the module that translates Mathlib meromorphic factorization into the Recognition Science defect-cost framework, linking the eight-tick phase sampling to the charge carried by zeta inverse.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.