eulerCostCoveringPackage
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.