eulerSampledBudgetedCarrier_scale_zero
plain-language theorem explainer
The sampled Euler carrier at real part σ₀ > 1/2 has vanishing carrier budget scale. Researchers instantiating the Recognition Science cost-covering bridge with the Euler product of ζ(s) cite this to confirm the concrete carrier meets the zero-scale requirement for defect estimates. The proof is a direct term-mode simplification that unfolds the sampled carrier definition and the budget scale formula.
Claim. Let σ₀ ∈ ℝ with σ₀ > 1/2. The scalar carrier budget of the Euler product carrier packaged as a BudgetedCarrier via the sampled-trace infrastructure with the zero-winding certificate equals zero.
background
The Euler Product Instantiation module realizes the abstract RS carrier/sensor framework from AnnularCost and CostCoveringBridge using the Euler product of ζ(s). Core objects include PrimeSum σ := ∑_p p^{-σ}, HilbertSchmidtNorm σ := ∑_p p^{-2σ}, carrierLogSeries, and carrierDerivBound σ := 2∑_p (log p) p^{-2σ}/(1-p^{-σ}). The module states that primes yield Hilbert-Schmidt convergence, det₂(I-A(s)) convergence, holomorphic nonvanishing C(s) on Re(s) > 1/2, and bounded logarithmic derivative, which together satisfy the EulerCarrier interface.
proof idea
The proof is a term-mode simplification. It unfolds the definition of the sampled Euler carrier, which applies SampledTrace.sampledBudgetedCarrier to the Euler zero-winding certificate, the carrier derivative bound, and its positivity, then substitutes the definition of carrierBudgetScale as budgetConstant times (logDerivBound)^2 times radius^2. The expression reduces directly to zero.
why it matters
This result verifies the final numerical property in the Euler instantiation chain that feeds CostCoveringPackage construction and the topological step of the conditional RH bridge. It ensures the defect topological floor is controlled by zero excess scale, consistent with the Recognition Science cost structure and the requirement that C(s) be holomorphic and nonvanishing for σ₀ > 1/2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.