cost_monotone_descent_terminates

formal source

 165
 166/-- **THEOREM EN-006.11**: Cost-decreasing transmutation is optimal.
 167    Any sequence of steps that strictly decreases cost will reach stability. -/
 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
 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. -/
 181theorem strict_transmutation_progress
 182    (cfg : NuclearConfig) (h_unstable : cfg.ratio ≠ 1) :
 183    ∃ step : TransmutationStep,
 184      step.initial = cfg ∧
 185      nuclearCost step.final < nuclearCost step.initial := by
 186  have hcost_pos := transmutation_cost_pos cfg h_unstable
 187  have hscz : nuclearCost stable_config = 0 := stable_config_zero_cost
 188  refine ⟨⟨cfg, stable_config, ?_⟩, rfl, ?_⟩
 189  · linarith [hscz.le, hcost_pos]
 190  · linarith [hscz.le, hcost_pos]
 191
 192/-! ## §VI. RS Transmutation Efficiency -/
 193
 194/-- The transmutation efficiency: ratio of cost reduction to initial cost. -/
 195def transmutation_efficiency (initial final : NuclearConfig) : ℝ :=
 196  if nuclearCost initial = 0 then 1
 197  else (nuclearCost initial - nuclearCost final) / nuclearCost initial
 198