zetaReciprocal_local_factorization
plain-language theorem explainer
This theorem guarantees a local meromorphic witness for the reciprocal zeta function at any complex point ρ ≠ 1 whose meromorphic order is the integer m. Researchers instantiating the Recognition Science carrier framework with the Euler product would cite it when building quantitative local factorizations near hypothetical zeros in the critical strip. The proof is a direct one-line application of the general local meromorphic factorization lemma to zetaReciprocal after confirming meromorphicity away from 1.
Claim. Let ρ ∈ ℂ with ρ ≠ 1, and let m ∈ ℤ be such that the meromorphic order of the reciprocal zeta function at ρ equals m. Then there exists a local meromorphic witness w with center ρ and order m.
background
The EulerInstantiation module shows how the Euler product for the Riemann zeta function supplies a concrete carrier for the abstract RS cost structure developed in AnnularCost and CostCoveringBridge. Core objects include the prime sum σ ↦ ∑_p p^{-σ}, the Hilbert-Schmidt norm squared ∑_p p^{-2σ}, the carrier log series, and the derivative bound carrierDerivBound(σ) = 2∑_p (log p) p^{-2σ}/(1-p^{-σ}). These establish that C(s) = det₂²(I - A(s)) is holomorphic and nonvanishing for Re(s) > 1/2 with bounded logarithmic derivative, satisfying the EulerCarrier and RegularCarrier interfaces.
proof idea
The proof is a one-line wrapper that applies the general lemma local_meromorphic_factorization to zetaReciprocal, passing the meromorphicAt hypothesis zetaReciprocal_meromorphicAt ρ hρ_ne together with the supplied integer order hord.
why it matters
This supplies the local witness required by eulerQuantitativeFactorization and its center and order extraction theorems. It completes the concrete-to-abstract step in the module's instantiation chain (primes → Hilbert-Schmidt operator → det₂ → bounded log derivative → carrier interface → cost-covering axiom), advancing the conditional Riemann hypothesis argument inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.