theorem
proved
perfect_transmutation_efficiency
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 215.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
NuclearConfig -
nuclearCost -
nuclear_cost_zero_iff_stable -
stable_config -
stable_config_zero_cost -
transmutation_efficiency -
of -
cost -
cost -
of -
from -
of -
of
used by
formal source
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,
231 path.start = cfg ∧ nuclearCost path.finish = 0) := by
232 exact ⟨transmutation_cost_pos, ⟨stable_config, stable_config_zero_cost⟩,
233 stable_end_state_exists⟩
234
235/-- Alias for registry lookup. -/
236theorem fission_transmutation_structure :
237 (∃ cfg : NuclearConfig, nuclearCost cfg = 0) :=
238 ⟨stable_config, stable_config_zero_cost⟩
239
240/-- Certificate: EN-006 Fission Product Transmutation — DERIVED -/
241def en006_certificate : String :=
242 "═══════════════════════════════════════════════════════════\n" ++
243 " EN-006: FISSION PRODUCT TRANSMUTATION — STATUS: DERIVED\n" ++
244 "═══════════════════════════════════════════════════════════\n" ++
245 "✓ nuclear_cost_nonneg: J(cfg) ≥ 0 for all configs\n" ++