zetaDerivedPhaseFamily_sensor
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence or uniqueness of any quantitative local factorization.
- Does not bound the size of phase perturbations arising from the regular factor.
- Does not address global analytic continuation or functional equation properties of zeta.
- Does not invoke the eight-tick winding or phi-ladder mass formulas.
formal statement (Lean)
360@[simp] theorem zetaDerivedPhaseFamily_sensor
361 (sensor : DefectSensor) (qlf : QuantitativeLocalFactorization)
362 (horder : qlf.order = -sensor.charge) :
363 (zetaDerivedPhaseFamily sensor qlf horder).sensor = sensor := rfl
proof body
Term-mode proof.
364
365/-- The current `zetaDerivedPhaseFamily` carries a zero-perturbation witness:
366its sampled increments are exactly the pure winding increments. -/