eulerQuantitativeFactorization_center
plain-language theorem explainer
The declaration shows that the center of the quantitative Euler factorization of the reciprocal zeta function at ρ coincides with ρ itself, under the assumptions that ρ is not 1, has specified meromorphic order m, and lies to the right of the critical line. Number theorists exploring conditional proofs of the Riemann hypothesis via Recognition Science cost structures would reference this to anchor the factorization point. The proof reduces directly to the specification of the local factorization witness for zetaReciprocal.
Claim. Let $ρ ∈ ℂ$ with $ρ ≠ 1$, $m ∈ ℤ$, and $1/2 < Re(ρ)$. If the meromorphic order of the reciprocal zeta function at $ρ$ equals $m$, then the center of the Euler quantitative factorization at $ρ$ equals $ρ$.
background
This module instantiates the abstract RS carrier/sensor framework from AnnularCost and CostCoveringBridge using the concrete Euler product for ζ(s). Core objects include PrimeSum σ := ∑_p p^{-σ}, HilbertSchmidtNorm σ := ∑_p p^{-2σ}, carrierLogSeries, and carrierDerivBound; these yield the Hilbert–Schmidt operator A(s) whose det₂(I − A(s)) defines C(s) holomorphic and nonvanishing for Re(s) > 1/2. The architecture proceeds from primes to convergent det₂ product to EulerCarrier + RegularCarrier satisfaction, enabling the cost-covering axiom that produces conditional RH.
proof idea
The proof is a one-line term-mode wrapper. It simplifies the definition of eulerQuantitativeFactorization together with the shrinkRadius property of LocalMeromorphicWitness, then invokes the first component of the choose_spec from the local factorization theorem for zetaReciprocal.
why it matters
This result anchors the quantitative factorization inside the Euler instantiation chain and feeds directly into honest_argument_principle_phase_family, which extracts a DefectPhaseFamily of charge exactly m from the meromorphic_phase_charge on concentric circles. It thereby closes the passage from Euler carrier satisfaction to the argument-principle data required for the cost-covering bridge. Within the Recognition Science framework it supplies the concrete localization step that lets the abstract RegularCarrier interface apply to zetaReciprocal on Re(s) > 1/2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.