zetaReciprocal_meromorphicAt
plain-language theorem explainer
The reciprocal of the Riemann zeta function is meromorphic at every complex point except s=1. Researchers building the Euler product instantiation of the RS cost structure cite this when confirming that the carrier satisfies the meromorphic requirements for the conditional Riemann hypothesis. The proof is a one-line wrapper that invokes the known analyticity of zeta away from its pole and applies the inversion rule for meromorphic functions.
Claim. The function $1/ζ(s)$ is meromorphic at every $s ∈ ℂ$ with $s ≠ 1$.
background
The module EulerInstantiation shows how the Euler product for ζ(s) supplies a concrete carrier for the abstract RS cost framework defined in AnnularCost and CostCoveringBridge. zetaReciprocal is the pointwise reciprocal of the Riemann zeta function, used to form the regularized determinant C(s) = det₂²(I − A(s)) that must be holomorphic and nonvanishing on Re(s) > 1/2. The local setting requires that this reciprocal remain meromorphic wherever the original zeta is analytic, so that logarithmic derivatives and local factorizations stay well-defined for the cost-covering axiom.
proof idea
One-line wrapper that applies analyticAt_riemannZeta (supplied by hs) to obtain meromorphicity of zeta, then composes with the standard inversion rule meromorphicAt.inv to conclude the result for the reciprocal.
why it matters
This theorem is the immediate predecessor of zetaReciprocal_local_factorization, which extracts the regular analytic factor at any hypothetical zero ρ in the strip. It completes the concrete-to-abstract step in the module's instantiation chain (primes → Hilbert–Schmidt operator → det₂ → EulerCarrier), allowing the cost-covering axiom to apply and yielding the conditional RH. The result therefore sits inside the T5–T8 forcing chain of Recognition Science by furnishing the meromorphic extension needed for the phi-ladder mass formula and the eight-tick octave analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.