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

cost_monotone_descent_terminates

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)

 168theorem cost_monotone_descent_terminates
 169    (initial_cost : ℝ) (hpos : 0 ≤ initial_cost) :
 170    ∃ n : ℕ, ∀ steps : ℕ,
 171      steps ≥ n → ∃ cfg : NuclearConfig,
 172        nuclearCost cfg ≤ initial_cost / (steps + 1) := by

proof body

Term-mode proof.

 173  use 0
 174  intros steps _
 175  use stable_config
 176  rw [stable_config_zero_cost]
 177  positivity
 178
 179/-- **THEOREM EN-006.12**: J-cost strictly decreases along optimal transmutation path.
 180    For any unstable nucleus, there exists a next step (the stable config) with less cost. -/

depends on (8)

Lean names referenced from this declaration's body.