EulerBudgetUpgradeTarget
plain-language theorem explainer
EulerBudgetUpgradeTarget σ₀ asserts existence of a BudgetedCarrier whose logarithmic derivative bound equals the Euler-derived carrierDerivBound at σ₀ and whose radius equals σ₀ minus one half. Number theorists instantiating the Recognition Science cost structure via the Euler product would cite this definition as the realizable upgrade target. The definition is a direct existential packaging of the zero-charge trace and uniform excess bound without mesh quantification.
Claim. For a real number σ₀, the Euler budget upgrade target holds if there exists a budgeted carrier such that its logarithmic derivative bound equals 2 ∑_p (log p) p^{-2σ₀}/(1 - p^{-σ₀}) and its radius equals σ₀ - 1/2.
background
The Euler Product Instantiation module shows that the Euler product of ζ(s) instantiates the abstract RS carrier/sensor framework from AnnularCost and CostCoveringBridge. BudgetedCarrier extends RegularCarrier with a zero-charge annular trace and an explicit excess-budget witness along that trace. carrierDerivBound σ₀ is the explicit scale 2 ∑_p (log p) p^{-2σ₀}/(1 - p^{-σ₀}) obtained from the prime sum. Upstream results establish Hilbert-Schmidt convergence for σ > 1/2 and nonvanishing of the determinant C(s) on Re(s) > 1/2.
proof idea
The definition is a direct existential statement over the BudgetedCarrier structure. It packages the two equality conditions on logDerivBound and radius as the target proposition.
why it matters
This definition supplies the concrete target in the Euler instantiation chain from primes through Hilbert-Schmidt norm to conditional RH via cost-covering. It is used by euler_budget_upgrade_target to inhabit the proposition for σ₀ > 1/2 and by euler_budget_upgrade_extends_regular to recover the regular-carrier data. It realizes the abstract carrier interface without quantifying over synthetic meshes, advancing the cost-covering step toward the T5-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.