zetaReciprocal_order_at_zero
plain-language theorem explainer
If the Riemann zeta function has a zero of positive integer order m at a complex point ρ, then its reciprocal has a pole of order m at the same point. Number theorists linking analytic orders to defect charges in Recognition Science cost models would cite this when equating sensor charge with meromorphic multiplicity. The proof is a one-line wrapper that rewrites the reciprocal order from the zeta order and simplifies.
Claim. If the meromorphic order of the Riemann zeta function at ρ ∈ ℂ equals the positive integer m, then the meromorphic order of the reciprocal 1/ζ at ρ equals −m.
background
The module instantiates the abstract RS carrier and sensor framework from AnnularCost and CostCoveringBridge by means of the Euler product for ζ(s). Core objects include PrimeSum σ = ∑_p p^{−σ}, the Hilbert–Schmidt norm squared of the associated operator A(s), and the resulting holomorphic nonvanishing carrier C(s) = det₂²(I − A(s)) on Re(s) > 1/2. The DefectSensor interface records charge together with real part; the present theorem supplies the concrete meromorphic-order witness that converts that charge into an analytic multiplicity for ζ⁻¹.
proof idea
The proof is a one-line wrapper that applies the sibling lemma meromorphicOrderAt_zetaReciprocal to replace the target order by the negation of the given zeta order, then finishes with simp.
why it matters
The declaration closes the link between defect-sensor charge and meromorphic order inside the Euler instantiation chain, allowing the cost-covering axiom to be applied once RegularCarrier is satisfied. It directly supports the conditional Riemann hypothesis route described in the module architecture and supplies the missing multiplicity statement for any zero of ζ. No open scaffolding remains for this specific step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.