eulerRegularCarrier

formal source

 699/-- For any hypothetical zero ρ with Re(ρ) > 1/2, the carrier
 700    is regular on a disk centered at ρ, so RegularCarrier is
 701    instantiated. -/
 702noncomputable def eulerRegularCarrier (σ₀ : ℝ) (hσ : 1/2 < σ₀) :
 703    RegularCarrier where
 704  logDerivBound := carrierDerivBound σ₀
 705  logDerivBound_pos := carrierDerivBound_pos hσ
 706  radius := σ₀ - 1/2
 707  radius_pos := by linarith
 708
 709/-- The instantiation is compatible: the RegularCarrier derived
 710    from the Euler product at σ₀ has the carrier centered at σ₀
 711    with radius reaching the critical line. -/
 712theorem euler_regular_carrier_covers_strip (σ₀ : ℝ) (hσ : 1/2 < σ₀) :
 713    (eulerRegularCarrier σ₀ hσ).radius = σ₀ - 1/2 := by
 714  simp [eulerRegularCarrier]
 715
 716/-! ### §7. The realizable `BudgetedCarrier` target -/
 717
 718/-- The direct Euler upgrade target now asks for a zero-charge annular trace
 719whose excess above the topological floor remains uniformly bounded by the
 720explicit carrier scale. Unlike the former interface, this does not quantify
 721over arbitrary synthetic meshes and is therefore a realizable target. -/
 722def EulerBudgetUpgradeTarget (σ₀ : ℝ) : Prop :=
 723  ∃ carrier : BudgetedCarrier,
 724    carrier.logDerivBound = carrierDerivBound σ₀ ∧
 725    carrier.radius = σ₀ - 1 / 2
 726
 727/-- Any successful Euler budget upgrade automatically extends the already proved
 728regular-carrier data at `σ₀`. -/
 729theorem euler_budget_upgrade_extends_regular (σ₀ : ℝ) :
 730    EulerBudgetUpgradeTarget σ₀ →
 731      ∃ carrier : RegularCarrier,
 732        carrier.logDerivBound = carrierDerivBound σ₀ ∧