pith. machine review for the scientific record. sign in
theorem proved term proof

euler_budget_upgrade_extends_regular

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 729theorem euler_budget_upgrade_extends_regular (σ₀ : ℝ) :
 730    EulerBudgetUpgradeTarget σ₀ →
 731      ∃ carrier : RegularCarrier,
 732        carrier.logDerivBound = carrierDerivBound σ₀ ∧
 733        carrier.radius = σ₀ - 1 / 2 := by

proof body

Term-mode proof.

 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. -/

depends on (15)

Lean names referenced from this declaration's body.