eulerSampledPackage
plain-language theorem explainer
The definition packages the sampled Euler carrier into a CostCoveringPackage for real σ₀ exceeding 1/2. Analysts studying conditional Riemann Hypothesis via cost-covering axioms would reference this construction. It is a direct wrapper that assigns the carrier field from the budgeted Euler carrier.
Claim. For real σ₀ with σ₀ > 1/2, the sampled Euler package is the CostCoveringPackage whose carrier equals the budgeted Euler carrier at σ₀.
background
The EulerInstantiation module embeds the classical Euler product for the zeta function into the Recognition Science cost framework. Core objects include 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 carrier derivative bound. These converge for σ > 1/2, yielding a holomorphic nonvanishing C(s) whose logarithmic derivative is bounded on Re(s) > 1/2.
proof idea
One-line wrapper that applies the budgeted Euler carrier construction.
why it matters
This definition supplies the concrete CostCoveringPackage used by the analytic trace module to build the sampled covering package. It completes the instantiation step in the Euler product chain from primes through Hilbert-Schmidt convergence to the EulerCarrier interface, allowing the floor coverage equivalence to charge zero. The construction supports the conditional Riemann Hypothesis pathway via the cost-covering axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.