riemann_hypothesis_euler_conditional
plain-language theorem explainer
Number theorists working on the analytic continuation of the zeta function would cite this result for its explicit embedding of the Euler product into the Recognition Science cost-covering axioms. It asserts that a CostCoveringPackage together with topological floor coverage for every DefectSensor forces a contradiction for any potential zero with real part strictly between 1/2 and 1. The argument is a direct term-mode wrapper that packages the parameters into a sensor and hands them to the prior euler_rh_conditional lemma.
Claim. Let $pkg$ be a CostCoveringPackage. Assume that for every DefectSensor the topological floor is covered by $pkg$. Then for every real number $σ_0$ satisfying $1/2 < σ_0 < 1$ and every nonzero integer $m$, the sensor constructed from $m$ and $σ_0$ yields a contradiction.
background
The module EulerInstantiation shows how the Euler product of ζ(s) realizes the abstract RS carrier/sensor framework. Core objects are the prime sum ∑_p p^{-σ}, the Hilbert-Schmidt norm squared ∑_p p^{-2σ}, the carrier log series ∑_p [2 log(1-p^{-σ}) + 2p^{-σ}], and the derivative bound 2∑_p (log p) p^{-2σ}/(1-p^{-σ}). Supporting results establish that the Hilbert-Schmidt norm is finite for σ > 1/2, that C(s) = det₂² is holomorphic and nonvanishing on Re(s) > 1/2, and that its logarithmic derivative remains bounded.
proof idea
The proof is a one-line term-mode wrapper. It builds the DefectSensor tuple from the supplied σ₀, m and the two interval hypotheses, then applies euler_rh_conditional directly to pkg, the coverage assumption, this sensor, and the nonzero condition on m.
why it matters
This theorem completes the three-layer instantiation chain in the module documentation: primes to A(s) Hilbert-Schmidt operator to det₂ convergence to holomorphic nonvanishing C(s) to cost-covering applicability to conditional RH. It realizes the EulerCarrier and RegularCarrier interfaces inside the Recognition Science cost structure. The result leaves open whether the topological floor coverage hypothesis can be discharged without additional scaffolding from the phi-ladder or J-cost primitives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.