eulerBudgetedCarrier
plain-language theorem explainer
This definition supplies an explicit BudgetedCarrier witness for the Euler product of zeta at real part sigma_0 greater than 1/2. Researchers pursuing the Recognition Science cost-covering route to a conditional Riemann hypothesis would cite it to obtain a concrete carrier with zero excess budget. The construction is a structure literal that sets the trace to the zero-charge Euler trace and invokes uniformChargeMesh_excess_zero to force annular excess to vanish identically.
Claim. Let $σ_0 > 1/2$. The Euler budgeted carrier is the BudgetedCarrier whose logarithmic-derivative bound equals the carrier derivative bound at $σ_0$, whose radius equals $σ_0 - 1/2$, whose trace is the Euler zero-charge trace, and whose excess bound is identically zero because the annular excess of every uniform zero-charge mesh vanishes.
background
The module instantiates the abstract RS carrier framework with the Euler product of ζ(s). Layer 1 (AnnularCost) defines the abstract BudgetedCarrier structure together with annularExcess, the excess cost above the topological floor for an annular mesh. Layer 3 (this file) supplies the concrete witness by taking the zero-charge Euler trace whose annular excess is identically zero. Upstream, annularExcess is defined as annularCost minus annularTopologicalFloor, and uniformChargeMesh_excess_zero shows that uniform zero increments saturate the floor at zero.
proof idea
The definition is a structure literal. It assigns logDerivBound to carrierDerivBound σ₀, radius to σ₀ - 1/2, trace to eulerZeroTrace, and budgetConstant to 0. The excess_bound field is discharged by reducing annularExcess(eulerZeroTrace.mesh N) to zero via uniformChargeMesh_excess_zero and then simplifying.
why it matters
This definition closes the concrete instantiation step that feeds eulerCostCoveringPackage and riemann_hypothesis_euler_conditional, thereby completing the chain from Euler product to conditional RH. It realizes the Layer 3 step in the module architecture where the Euler product satisfies the abstract carrier interface required by the cost-covering axiom. The parent theorem riemann_hypothesis_euler_conditional packages this carrier to obtain the full conditional statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.