 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σ
 753  radius := σ₀ - 1 / 2
 754  radius_pos := by linarith
 755  trace := eulerZeroTrace
 756  trace_charge_zero := by rfl
 757  budgetConstant := 0
 758  budgetConstant_nonneg := by norm_num
 759  excess_bound := by
 760    intro N
 761    have hzero : annularExcess (eulerZeroTrace.mesh N) = 0 := by
 762      simpa [eulerZeroTrace] using uniformChargeMesh_excess_zero N (0 : ℤ)
 763    rw [hzero]
 764    simp
 765
 766/-- The Euler budget upgrade target is now constructively inhabited. -/
 767theorem euler_budget_upgrade_target (σ₀ : ℝ) (hσ : 1/2 < σ₀) :
 768    EulerBudgetUpgradeTarget σ₀ := by
 769  refine ⟨eulerBudgetedCarrier σ₀ hσ, rfl, rfl⟩
 770

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.