EulerBudgetUpgradeTarget

formal source

 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 σ₀ ∧
 733        carrier.radius = σ₀ - 1 / 2 := by
 734  intro h
 735  rcases h with ⟨carrier, hderiv, hradius⟩
 736  exact ⟨carrier.toRegularCarrier, hderiv, hradius⟩
 737
 738/-- The canonical zero-charge Euler trace: every refinement ring carries zero
 739winding. This is the concrete carrier trace whose excess is identically zero. -/
 740noncomputable def eulerZeroTrace : AnnularTrace where
 741  charge := 0
 742  mesh := fun N => uniformChargeMesh N 0
 743  charge_spec := by
 744    intro N
 745    simp [uniformChargeMesh]
 746
 747/-- The Euler carrier admits a concrete realizable `BudgetedCarrier` witness:
 748the zero-charge trace has zero annular excess, so the excess budget is
 749uniformly bounded with budget constant `0`. -/
 750noncomputable def eulerBudgetedCarrier (σ₀ : ℝ) (hσ : 1/2 < σ₀) : BudgetedCarrier where
 751  logDerivBound := carrierDerivBound σ₀
 752  logDerivBound_pos := carrierDerivBound_pos hσ