zetaReciprocal_local_factorization
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.
claimLet ρ ∈ ℂ 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 in Recognition Science
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.
scope and limits
- Does not compute the explicit value of the meromorphic order m at any ρ.
- Does not prove existence or location of zeros of zetaReciprocal.
- Does not extend the factorization outside a local disk around ρ.
- Does not address global properties of the reciprocal zeta function beyond the given point.
formal statement (Lean)
612theorem zetaReciprocal_local_factorization (ρ : ℂ)
613 (hρ_ne : ρ ≠ 1)
614 (m : ℤ)
615 (hord : meromorphicOrderAt zetaReciprocal ρ = ↑m) :
616 ∃ w : LocalMeromorphicWitness, w.center = ρ ∧ w.order = m := by
proof body
Term-mode proof.
617 exact local_meromorphic_factorization zetaReciprocal ρ m
618 (zetaReciprocal_meromorphicAt ρ hρ_ne) hord
619
620/-- Construct a `QuantitativeLocalFactorization` from the Euler carrier data
621at a hypothetical zero ρ. The log-derivative bound `M` is taken from
622`carrierDerivBound(Re(ρ))`, which dominates the per-prime log-derivative
623terms by `eulerPrimeLogDerivTermComplex_summable`. -/