eulerSampledBudgetedCarrier
This definition packages the holomorphic nonvanishing Euler product carrier C(s) as a BudgetedCarrier by wrapping its zero-winding certificate and logarithmic derivative bounds into the sampled trace construction. Analysts working on conditional Riemann hypothesis statements via cost-covering axioms cite it when instantiating the abstract carrier interface with the concrete zeta function. The construction is a direct one-line application of the sampled budgeted carrier template to the Euler-specific certificate and bounds.
claimFor real number $σ_0 > 1/2$, the Euler sampled budgeted carrier is the structure extending the regular carrier $C(s)$ (the squared determinant of $I - A(s)$ from the prime-sum operator) with a zero-charge annular trace, nonnegative budget constant, and uniform excess-cost bound above the topological floor, obtained via the sampled trace construction.
background
The module instantiates the abstract RS cost structure with the Euler product of ζ(s). Layer 1 supplies the annular cost framework; layer 2 adds the carrier-plus-axiom interface that yields conditional RH; layer 3 (this file) supplies the concrete objects: PrimeSum, HilbertSchmidtNorm, carrierLogSeries, and carrierDerivBound. BudgetedCarrier is the structure extending RegularCarrier with an explicit zero-charge annular trace and an excess-budget witness that makes mesh-independent budget claims possible. The upstream eulerZeroWindingCert derives the zero-winding property directly from holomorphy and nonvanishing of C(s) on Re(s) > 1/2 rather than assuming it synthetically.
proof idea
One-line wrapper that applies the sampledBudgetedCarrier constructor from SampledTrace to the Euler zero-winding certificate, the carrier derivative bound, its positivity witness, the gap parameter σ₀ − 1/2, and a linarith justification that the gap is positive.
why it matters in Recognition Science
It supplies the concrete budgeted carrier required to form the CostCoveringPackage in the Euler instantiation chain, feeding directly into the scale-zero theorem and the sampled package definition. This completes the layer-3 step that lets the cost-covering axiom apply to the zeta function. The construction touches the open question of whether the zero budget persists under analytic continuation beyond the half-plane of absolute convergence.
scope and limits
- Does not establish any convergence or nonvanishing statement for Re(s) ≤ 1/2.
- Does not yield an unconditional proof of the Riemann hypothesis.
- Does not compute an explicit numerical value for the budget constant beyond nonnegativity.
- Does not apply to carriers other than the Euler product instantiation.
Lean usage
eulerSampledBudgetedCarrier (3/2) (by norm_num)formal statement (Lean)
959noncomputable def eulerSampledBudgetedCarrier (σ₀ : ℝ) (hσ : 1/2 < σ₀) :
960 BudgetedCarrier :=
proof body
Definition body.
961 SampledTrace.sampledBudgetedCarrier
962 (EulerCarrierComplex.eulerZeroWindingCert σ₀ hσ)
963 (carrierDerivBound σ₀)
964 (carrierDerivBound_pos hσ)
965 (σ₀ - 1/2)
966 (by linarith)
967
968/-- The sampled Euler carrier has budget scale 0. -/