strict_transmutation_progress

formal source

 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
 199/-- **THEOREM EN-006.13**: Transmutation efficiency is in [0, 1]. -/
 200theorem efficiency_bounded (initial final : NuclearConfig)
 201    (h : nuclearCost final ≤ nuclearCost initial) :
 202    0 ≤ transmutation_efficiency initial final ∧
 203    transmutation_efficiency initial final ≤ 1 := by
 204  unfold transmutation_efficiency
 205  split_ifs with h0
 206  · constructor <;> norm_num
 207  · constructor
 208    · apply div_nonneg
 209      · linarith [nuclear_cost_nonneg final]
 210      · exact nuclear_cost_nonneg initial
 211    · rw [div_le_one (lt_of_le_of_ne (nuclear_cost_nonneg initial) (Ne.symm h0))]