theorem
proved
efficiency_bounded
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Engineering.FissionTransmutationStructure on GitHub at line 200.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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))]
212 linarith [nuclear_cost_nonneg final]
213
214/-- **THEOREM EN-006.14**: Perfect transmutation (to stable state) has 100% efficiency. -/
215theorem perfect_transmutation_efficiency (cfg : NuclearConfig) (h_unstable : cfg.ratio ≠ 1) :
216 transmutation_efficiency cfg stable_config = 1 := by
217 unfold transmutation_efficiency
218 have h0 : nuclearCost cfg ≠ 0 := by
219 intro h
220 exact h_unstable ((nuclear_cost_zero_iff_stable cfg).mp h)
221 simp [h0, stable_config_zero_cost]
222
223/-! ## §VII. Summary -/
224
225/-- The RS fission transmutation theorem.
226 Derives key properties of transmutation from J-cost structure. -/
227theorem fission_transmutation_from_ledger :
228 (∀ cfg : NuclearConfig, cfg.ratio ≠ 1 → 0 < nuclearCost cfg) ∧
229 (∃ cfg : NuclearConfig, nuclearCost cfg = 0) ∧
230 (∀ cfg : NuclearConfig, ∃ path : TransmutationPath,