euler_budget_upgrade_extends_regular
plain-language theorem explainer
Any Euler budget upgrade target at a real number σ₀ yields a regular carrier whose logarithmic derivative bound equals the explicit carrierDerivBound at σ₀ and whose radius equals σ₀ minus one half. Researchers instantiating the Euler product inside the Recognition Science cost-covering chain cite this when moving from budgeted to regular carriers. The proof is a direct term extraction that unpacks the budgeted carrier and applies its conversion to the regular carrier type.
Claim. Let σ₀ ∈ ℝ. If there exists a budgeted carrier such that its logDerivBound equals carrierDerivBound(σ₀) and its radius equals σ₀ − 1/2, then there exists a regular carrier satisfying the same two equalities.
background
The Euler Product Instantiation module realizes the abstract RS carrier framework from AnnularCost and CostCoveringBridge by instantiating the Euler product of ζ(s) as a concrete carrier. EulerBudgetUpgradeTarget is the existence of a BudgetedCarrier whose logDerivBound matches the explicit sum carrierDerivBound(σ₀) = 2∑_p (log p)·p^{−2σ₀}/(1−p^{−σ₀}) and whose radius is σ₀ − 1/2; this encodes a zero-charge annular trace with uniformly bounded excess. RegularCarrier supplies the interface whose data are fed to the cost-covering axiom that yields conditional RH. The module records the prior results that the Hilbert–Schmidt norm of A(s) converges for σ > 1/2 and that C(s) is holomorphic and nonvanishing on Re(s) > 1/2.
proof idea
The proof is a one-line term wrapper. It introduces the hypothesis, performs rcases to extract the budgeted carrier together with the two equalities, then applies the toRegularCarrier conversion to witness the required regular carrier.
why it matters
The declaration closes the final step of the Euler instantiation chain: primes → Hilbert–Schmidt → det₂ → C(s) holomorphic → EulerCarrier → RegularCarrier. It thereby supplies the concrete carrier data needed for the cost-covering bridge that produces conditional RH. The result sits inside the Recognition Science framework after the Recognition Composition Law and the eight-tick octave, providing the explicit radius and derivative bound that the phi-ladder mass formula later consumes. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.