eulerCostCoveringPackage
The definition packages any real abscissa σ₀ strictly above 1/2 into a CostCoveringPackage whose carrier slot is filled by the budgeted Euler carrier at that point. Researchers tracing the Euler-product route to a conditional Riemann hypothesis inside the Recognition Science cost framework would cite this step. It is realized as a one-line wrapper delegating directly to eulerBudgetedCarrier.
claimFor any real number σ₀ satisfying σ₀ > 1/2, the construction yields a CostCoveringPackage whose carrier field equals the budgeted Euler carrier evaluated at σ₀.
background
The module instantiates the abstract RS carrier/sensor framework by means of the Euler product for ζ(s). Layer 1 supplies the abstract AnnularCost and CostCoveringBridge structures; Layer 3 supplies the concrete objects PrimeSum σ = ∑_p p^{-σ}, HilbertSchmidtNorm σ = ∑_p p^{-2σ}, carrierLogSeries, and carrierDerivBound. The key intermediate claim is that C(s) = det₂²(I − A(s)) is holomorphic and non-vanishing for Re(s) > 1/2, with bounded logarithmic derivative.
proof idea
One-line wrapper that applies eulerBudgetedCarrier σ₀ hσ to populate the carrier field of the CostCoveringPackage record.
why it matters in Recognition Science
The definition closes the concrete-to-abstract link required before the cost-covering axiom can be invoked, completing the chain primes → Hilbert–Schmidt convergence → det₂ product convergence → EulerCarrier interface → CostCoveringPackage. It therefore sits immediately upstream of any conditional RH statement obtained via the argument-principle sampling axiom. The module leaves open the formalization of contour integration needed to discharge that axiom.
scope and limits
- Does not prove the Riemann hypothesis unconditionally.
- Does not supply contour-integration machinery for the argument principle.
- Does not treat zeros on the critical line Re(s) = 1/2.
- Does not produce explicit numerical bounds on the carrier derivative.
formal statement (Lean)
772noncomputable def eulerCostCoveringPackage (σ₀ : ℝ) (hσ : 1/2 < σ₀) : CostCoveringPackage where
773 carrier := eulerBudgetedCarrier σ₀ hσ
proof body
Definition body.
774
775/-! ### §7b. Complex-analysis axioms for RH -/
776
777/-- **Axiom 1 (Argument Principle Sampling).**
778
779Standard complex analysis: if ζ has a zero of order `m` at ρ with Re(ρ) > 1/2,
780then sampling the phase of ζ(s)⁻¹ on `N` concentric rings around ρ produces an
781annular mesh whose per-ring winding is exactly `m`.
782
783This is NOT equivalent to RH. It is a consequence of the argument principle
784for meromorphic functions and requires contour integration, which is not yet
785available in Mathlib. -/