meromorphicOrderAt_zetaReciprocal
plain-language theorem explainer
The theorem states that the meromorphic order of the reciprocal of the Riemann zeta function at any complex point equals the negative of the zeta function's order there. Number theorists connecting the Euler product to Recognition Science's defect and cost models would cite this when handling sign changes between zeros and poles. The proof is a direct one-line application of the general meromorphic order inversion lemma after rewriting the reciprocal explicitly.
Claim. For every complex number $s$, the meromorphic order of $ζ^{-1}$ at $s$ is equal to the negative of the meromorphic order of the Riemann zeta function $ζ$ at $s$.
background
This declaration appears in the module that instantiates the abstract RS cost structure using the Euler product of the Riemann zeta function. The function zetaReciprocal is the pointwise reciprocal of riemannZeta. The meromorphic order at a point $s$ is the integer $m$ such that the function behaves like $(z-s)^m$ times a holomorphic non-zero function near $s$. The module builds on the AnnularCost layer for abstract carriers and the CostCoveringBridge for deriving conditional statements about the Riemann hypothesis from carrier axioms.
proof idea
The proof rewrites zetaReciprocal explicitly as the inverse of riemannZeta and applies the library result meromorphicOrderAt_inv that the order of an inverse equals the negation of the original order.
why it matters
This theorem is applied in zetaReciprocal_order_at_zero to convert a positive order $m$ at a zero of zeta into a negative order $-m$ at the corresponding pole of the reciprocal. The doc-comment links this sign change to the charge of a defect sensor in the sampled function. It advances the Euler instantiation chain by supplying the required meromorphic property for the carrier to satisfy the RegularCarrier interface, supporting the path to a conditional Riemann hypothesis via the cost-covering axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.