eulerQuantitativeFactorization
plain-language theorem explainer
This definition assembles a QuantitativeLocalFactorization for a hypothetical zero ρ of zetaReciprocal with Re(ρ) > 1/2 by combining the local meromorphic witness with a radius shrunk to obey the carrier derivative bound. Researchers working on conditional Riemann hypothesis proofs via the cost-covering axiom would cite it when instantiating the Euler product as a concrete RegularCarrier. The body selects the witness from zetaReciprocal_local_factorization, sets M to carrierDerivBound at Re(ρ), computes r as the min of the witness radius and 1/
Claim. Let ρ ∈ ℂ with ρ ≠ 1 and Re(ρ) = σ > 1/2, and let m ∈ ℤ be the meromorphic order of the reciprocal zeta function at ρ. The definition yields a QuantitativeLocalFactorization whose center is ρ, whose order is m, and whose log-derivative bound equals the carrier derivative bound at σ, obtained by shrinking the local meromorphic witness radius to satisfy the perturbation regime M r ≤ 1.
background
The module instantiates the abstract RS carrier/sensor framework from AnnularCost and CostCoveringBridge using the Euler product of ζ(s). Core objects include carrierDerivBound σ := 2 ∑_p (log p) p^{-2σ}/(1-p^{-σ}), which bounds |C'/C| for the holomorphic nonvanishing function C(s) = det₂²(I-A(s)) on Re(s) > 1/2, together with the Hilbert-Schmidt norm and log-series convergence results that guarantee the EulerCarrier and RegularCarrier interfaces. The local theoretical setting is the three-layer chain: abstract cost axioms, carrier/sensor bridge to conditional RH, and concrete Euler product data. Upstream results supply zetaReciprocal_local_factorization for the meromorphic witness and carrierDerivBound_pos to guarantee positivity of the bound M.
proof idea
The definition extracts the local meromorphic witness w via zetaReciprocal_local_factorization. It sets M := carrierDerivBound ρ.re (positive by carrierDerivBound_pos) and r := min(w.radius, 1/M). The QuantitativeLocalFactorization is then assembled by shrinking w to radius r, assigning logDerivBound := M, and verifying the perturbation regime by the direct chain M r ≤ M · (1/M) = 1.
why it matters
This supplies the concrete QuantitativeLocalFactorization required by honest_argument_principle_phase_family to produce a DefectPhaseFamily of charge exactly m, and by the sibling theorems eulerQuantitativeFactorization_center, _logDerivBound and _order. It completes the Euler instantiation layer, confirming that the zeta reciprocal satisfies RegularCarrier for any hypothetical zero with Re(ρ) > 1/2 and thereby activates the cost-covering axiom for conditional RH. The construction touches the open question of zero existence by furnishing the quantitative data structure needed for phase-charge analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.