eulerCarrierInstance

formal source

 688/-- **Main instantiation theorem:** The concrete Euler carrier
 689    satisfies the abstract EulerCarrier interface from
 690    CostCoveringBridge.lean. -/
 691noncomputable def eulerCarrierInstance : EulerCarrier where
 692  halfPlane := 1
 693  halfPlane_gt := by norm_num
 694  logDerivBound := carrierDerivBound
 695  logDerivBound_finite σ hσ := by
 696    trivial
 697  nonvanishing := True
 698
 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. -/