`transmutation_efficiency`

definition

show as: view math explainer →

module: IndisputableMonolith.Engineering.FissionTransmutationStructure
domain: Engineering
line: 195 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Engineering.FissionTransmutationStructure on GitHub at line 195.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 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))]
 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.

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.