zetaReciprocal
plain-language theorem explainer
zetaReciprocal supplies the reciprocal of the Riemann zeta function at complex s as the concrete meromorphic object in the Euler product instantiation of the RS carrier framework. Researchers applying the argument principle to hypothetical zeros cite it when realizing defect charge via sampled phase. The implementation is a direct one-line wrapper inverting riemannZeta.
Claim. For $s ∈ ℂ$, define the reciprocal zeta function by $ζ^{-1}(s) := 1/ζ(s)$. This is the meromorphic object whose sampled phase realizes the defect charge around a hypothetical zero.
background
The EulerInstantiation module bridges the abstract RS carrier and sensor framework (from AnnularCost and CostCoveringBridge) to the concrete Euler product of the Riemann zeta function. It shows that the prime sum yields a Hilbert-Schmidt operator A(s) whose determinant C(s) is holomorphic and nonvanishing for Re(s) > 1/2, satisfying the EulerCarrier and RegularCarrier interfaces and enabling the cost-covering axiom for conditional RH.
proof idea
This is a one-line wrapper that applies the reciprocal operation to riemannZeta at the input complex argument.
why it matters
zetaReciprocal provides the central meromorphic object for eulerQuantitativeFactorization and its variants (center, log-deriv bound, order) as well as analyticAt_riemannZeta. It feeds the analytic route to RH in the module and connects to the defect functional (equal to J for positive x) from LawOfExistence. In the Recognition Science framework it instantiates the carrier for the cost-covering step toward conditional RH, aligning with T5 J-uniqueness and the defect sensor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.