eulerSampledCoveringPackage
plain-language theorem explainer
The definition supplies the sampled Euler CostCoveringPackage for any real σ₀ exceeding 1/2. Researchers pursuing the pure analytic route to the Riemann hypothesis cite it when deriving charge-zero equivalences from zero-winding certificates. It is realized as a direct one-line wrapper around the Euler sampled package.
Claim. For any real number $σ_0 > 1/2$, the Euler-sampled cost-covering package is the CostCoveringPackage constructed by the sampled Euler instantiation at $σ_0$.
background
The Analytic Trace module assembles an axiom-free RH bridge. It replaces earlier axioms with contour winding derived from holomorphy and nonvanishing, and with a proved floor-coverage equivalence. The defect functional equals J on positive reals. CostCoveringPackage is the structure exported by CostCoveringBridge that bundles covering budget and topological floor data. EulerInstantiation supplies the underlying eulerSampledPackage whose zero-winding certificate yields budget zero.
proof idea
This is a one-line wrapper that applies eulerSampledPackage σ₀ hσ from the EulerInstantiation module.
why it matters
The package feeds the three downstream theorems carrier_side_obstruction, charge_zero_of_covered, and floorCovered_iff_charge_zero. It supplies the zero-budget carrier required for the pure analytic route to RH, distinct from the ontology route through UnifiedRH.unified_rh. The construction uses the zero-winding certificate rather than a synthetic zero-charge trace, closing one former axiom in the analytic trace interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.