euler_budget_upgrade_target
plain-language theorem explainer
For σ₀ > 1/2 the Euler budget upgrade target holds by direct construction of a budgeted carrier from the Euler product. Number theorists working on cost-covering proofs of the Riemann hypothesis would cite this result to close the concrete instantiation step. The proof is a one-line term refinement that supplies the pre-built eulerBudgetedCarrier witness and matches the two field equalities by reflexivity.
Claim. For every real number $σ₀ > 1/2$ there exists a budgeted carrier such that its logarithmic derivative bound equals the carrier derivative bound evaluated at $σ₀$ and its radius equals $σ₀ - 1/2$.
background
The module instantiates the abstract RS carrier framework with the Euler product of the zeta function. Layer 1 supplies the annular cost structure, Layer 2 the carrier-plus-axiom bridge to conditional RH, and this file supplies the concrete Euler product that satisfies both EulerCarrier and RegularCarrier interfaces. EulerBudgetUpgradeTarget is the proposition that a zero-charge annular trace exists whose excess above the topological floor is bounded by the explicit carrier scale at radius $σ₀ - 1/2$. The supporting definition eulerBudgetedCarrier constructs the witness whose logDerivBound field is set to carrierDerivBound $σ₀$ and whose radius field is set to $σ₀ - 1/2$.
proof idea
The proof is a term-mode one-line wrapper. It applies the already-constructed eulerBudgetedCarrier $σ₀$ $hσ$ to obtain the required BudgetedCarrier witness, then uses reflexivity to discharge the two field equalities logDerivBound = carrierDerivBound $σ₀$ and radius = $σ₀ - 1/2$.
why it matters
This declaration shows that the Euler budget upgrade target is constructively inhabited, completing the concrete half of the instantiation chain primes → Hilbert–Schmidt operator → det₂ convergence → regular carrier. It feeds directly into the cost-covering bridge that yields conditional RH for Re(s) > 1/2. The result sits inside the T5–T8 forcing chain by supplying the J-cost and defect bounds required for the eight-tick octave and D = 3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.