analyticAt_riemannZeta
plain-language theorem explainer
The Riemann zeta function is analytic at every complex number except the pole at s=1. Researchers building the Euler product instantiation of the Recognition Science carrier framework cite this to secure holomorphy of zeta away from s=1 before passing to the reciprocal and the determinant factor C(s). The proof is a short term construction that lifts pointwise differentiability on the complement of {1} to analyticity via the open-set criterion from complex analysis.
Claim. The Riemann zeta function satisfies analyticity at every complex number $s$ with $s ≠ 1$.
background
The EulerInstantiation module shows how the Euler product for the Riemann zeta function concretely realizes the abstract RS carrier and sensor framework defined in AnnularCost and CostCoveringBridge. This supplies the concrete layer that turns the cost-covering axiom into a conditional statement on the Riemann hypothesis. The local setting begins with the prime zeta sums and Hilbert-Schmidt norms of the associated operator A(s), then passes through the determinant factor C(s) = det₂²(I − A(s)) whose holomorphy and non-vanishing on Re(s) > 1/2 are required for the RegularCarrier interface.
proof idea
The term proof first builds a DifferentiableOn statement for riemannZeta on the complement of the singleton {1} by applying differentiableAt_riemannZeta at each point and converting the result to differentiableWithinAt. It then invokes the analyticAt method on that DifferentiableOn object, using the fact that the complement of a singleton is open in the complex plane, to obtain the required analyticity at the given s ≠ 1.
why it matters
This theorem is invoked directly by zetaReciprocal_meromorphicAt, which in turn supports the meromorphic character of the reciprocal needed for the Euler carrier instantiation. Within the Recognition Science chain it supplies the analyticity step that lets C(s) be holomorphic and non-vanishing on Re(s) > 1/2, thereby licensing the cost-covering axiom and the conditional RH. The result closes one link in the Layer 3 concrete-to-abstract passage described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.