zetaDerivedPhaseFamily_sensor
plain-language theorem explainer
The theorem states that the sensor component of a zeta-derived phase family equals the input defect sensor whenever the quantitative local factorization order matches the negative sensor charge. Analysts applying meromorphic orders to zeta zeros in annular cost models would cite it to verify that the constructed family preserves the defect charge. The proof is a direct reflexivity step once the family definition is unfolded.
Claim. Let $S$ be a defect sensor with charge $m$ and let $Q$ be a quantitative local factorization whose order equals $-m$. The sensor field of the defect phase family built from $S$ and $Q$ equals $S$.
background
The MeromorphicCircleOrder module bridges Mathlib meromorphic-order machinery to the Recognition Science annular cost framework. A DefectSensor records the multiplicity $m$ of a zero of zeta (hence the pole order of zeta inverse) together with its real part inside the critical strip. QuantitativeLocalFactorization extends a local meromorphic witness by a uniform bound on the logarithmic derivative of the regular factor, supplying the analytic control needed for phase perturbations on sampled circles.
proof idea
The proof is a one-line wrapper that applies reflexivity. The definition of zetaDerivedPhaseFamily sets the sensor field directly to the supplied parameter, so the equality holds by construction under the order-matching hypothesis.
why it matters
This equality anchors the zeta-derived phase family to its input defect sensor, ensuring that downstream perturbation bounds and cost coverings operate on the correct charge. It supports the transition from local meromorphic factorization to sampled phase increments required by RingPerturbationControl. Within the Recognition Science setting it reinforces the identification of meromorphic order at zeta zeros with the phase charge used in the annular cost model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.