WitnessedDefectSensor
plain-language theorem explainer
A structure equips a complex point ρ with real part strictly between 1/2 and 1 together with an integer charge certified by the meromorphic order of the reciprocal zeta function at ρ. Analysts constructing conditional Riemann-hypothesis proofs from Euler-product carriers cite this object to feed concrete sensors into abstract cost bridges. The declaration is a plain record type whose coercion to the weaker sensor and the auxiliary non-pole lemma are both one-line projections.
Claim. A witnessed defect sensor consists of a complex number ρ satisfying 1/2 < Re(ρ) < 1, an integer charge n, and a witness that the meromorphic order of ζ^{-1} at ρ equals -n.
background
The EulerInstantiation module supplies the concrete third layer of the RS cost framework: the Euler product for ζ(s) is turned into a Hilbert-Schmidt operator A(s) whose determinant C(s) is holomorphic and non-vanishing for Re(s) > 1/2. The weaker DefectSensor records only charge and real part; the present structure augments it with the full center ρ and the analytic certificate drawn from meromorphicOrderAt applied to zetaReciprocal. Upstream imports provide the meromorphic-order predicate and the EulerCarrierComplex interface that guarantees the order is an integer.
proof idea
The declaration is a structure definition packaging four fields. The coercion toDefectSensor is a one-line record projection. The lemma rho_ne_one proceeds by contradiction: assume ρ = 1, extract Re(ρ) = 1, then apply linarith to the strict upper bound of the strip interval.
why it matters
This structure supplies the concrete input required by the charge-zero discharge theorems in AnalyticTrace, including direct_rh_from_honestPhaseCostBridge and direct_rh_from_EBBA_via_analytic. It closes the passage from the abstract ZeroFreeCriterion to Euler-product data, allowing the cost-covering axiom to imply the Riemann hypothesis conditionally on the existence of such witnessed sensors. It touches the open question whether every zero inside the strip carries non-zero charge under the RS cost model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.