theorem proved term proof

`euler_budget_upgrade_target`

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

formal statement (Lean)

 767theorem euler_budget_upgrade_target (σ₀ : ℝ) (hσ : 1/2 < σ₀) :
 768    EulerBudgetUpgradeTarget σ₀ := by

Term-mode proof.

 769  refine ⟨eulerBudgetedCarrier σ₀ hσ, rfl, rfl⟩
 770
 771/-- Package the concrete Euler budgeted carrier. -/

Lean names referenced from this declaration's body.

carrier in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
carrier in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use
eulerBudgetedCarrier in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use
EulerBudgetUpgradeTarget in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use