theorem
proved
stable_end_state_exists
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Engineering.FissionTransmutationStructure on GitHub at line 157.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
V -
NuclearConfig -
nuclearCost -
nuclear_cost_nonneg -
stable_config -
stable_config_zero_cost -
TransmutationPath -
of -
cost -
cost -
is -
of -
is -
of -
V -
is -
of -
is -
Cost -
that -
V
used by
formal source
154
155/-- **THEOREM EN-006.10**: For any fission product, there exists a transmutation path
156 to a stable end state (the global minimum). -/
157theorem stable_end_state_exists (cfg : NuclearConfig) :
158 ∃ path : TransmutationPath,
159 path.start = cfg ∧
160 nuclearCost path.finish = 0 := by
161 use ⟨cfg, stable_config, 1, by rw [stable_config_zero_cost]; exact nuclear_cost_nonneg cfg⟩
162 exact ⟨rfl, stable_config_zero_cost⟩
163
164/-! ## §V. Cost-Descent Optimality -/
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