euler_regular_carrier_covers_strip
plain-language theorem explainer
For any real σ₀ strictly larger than 1/2 the regular carrier built from the Euler product at σ₀ has radius exactly σ₀ minus 1/2, so its disk reaches the critical line. Researchers closing the cost-covering bridge to a conditional Riemann hypothesis cite the result when confirming carrier-sensor compatibility inside the Euler instantiation. The argument reduces at once to the definition of the regular carrier by simplification.
Claim. Let σ₀ ∈ ℝ satisfy σ₀ > 1/2. The radius of the regular carrier obtained from the Euler product centered at σ₀ equals σ₀ − 1/2.
background
This theorem belongs to the Euler Product Instantiation module, which supplies a concrete model for the abstract carrier and sensor framework of AnnularCost and CostCoveringBridge. Core objects include the prime sum ∑_p p^{-σ}, the squared Hilbert-Schmidt norm ∑_p p^{-2σ}, the carrier logarithmic series, and the derivative bound, all shown to converge for σ > 1/2 and to produce a holomorphic nonvanishing C(s) on Re(s) > 1/2 whose logarithmic derivative stays bounded. The module therefore realizes the three-layer chain: abstract cost axioms, carrier-plus-axiom implying conditional RH, and the Euler product that satisfies the EulerCarrier interface.
proof idea
The proof is a one-line wrapper that applies simp to the definition of eulerRegularCarrier.
why it matters
The result supplies the explicit radius needed by sensor_carrier_compatible and by mkEulerInstantiationCert. It therefore completes the passage from the Euler product to a regular carrier whose disk touches the critical line, allowing the cost-covering axiom to apply and yield a conditional form of the Riemann hypothesis. The declaration sits at the interface between classical analytic number theory and the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.