zetaReciprocal_differentiableAt
plain-language theorem explainer
The reciprocal of the Riemann zeta function is holomorphic at every complex s except the pole at 1 and the zeros of zeta. Analysts constructing holomorphic carriers for phase-lift witnesses in the Recognition Science Euler product instantiation would cite this result. The proof is a one-line wrapper that applies the known differentiability of zeta away from its pole together with the algebraic inverse rule for nonvanishing holomorphic functions.
Claim. Let $s$ be a complex number with $s ≠ 1$ and $ζ(s) ≠ 0$. Then the reciprocal function $1/ζ(s)$ is differentiable at $s$.
background
The Euler Product Instantiation module concretely realizes the abstract RS carrier/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, the carrier log series, and the carrier derivative bound. The local theoretical setting is the chain primes → Hilbert-Schmidt convergence → det₂(I−A(s)) holomorphic and nonvanishing on Re(s) > 1/2 → logarithmic derivative bounded → EulerCarrier and RegularCarrier satisfied → cost-covering axiom → conditional RH.
proof idea
This is a one-line wrapper proof. It invokes the known differentiability of the Riemann zeta function away from s = 1, then applies the inverse rule for holomorphic functions at points where the value is nonzero, using the definition of zetaReciprocal as the pointwise reciprocal.
why it matters
This result supplies the holomorphic reciprocal zeta function required for the EulerCarrier interface inside the Recognition Science cost structure. It supports the module architecture that leads to euler_instantiation and the conditional RH. Within the forcing chain it contributes the analytic prerequisite for the complex carrier derivative bounds that follow in the same section.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.