`TransmutationPath`

definition

show as: view math explainer →

module: IndisputableMonolith.Engineering.FissionTransmutationStructure
domain: Engineering
line: 113 · 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 113.

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

 110/-! ## §III. Transmutation Pathways -/
 111
 112/-- A transmutation pathway: sequence of steps from fission product to stable end. -/
 113structure TransmutationPath where
 114  /-- Initial fission product configuration. -/
 115  start : NuclearConfig
 116  /-- Final (stable) end state. -/
 117  finish : NuclearConfig
 118  /-- Number of steps. -/
 119  n_steps : ℕ
 120  /-- Net cost reduction from start to finish. -/
 121  net_reduction : nuclearCost finish ≤ nuclearCost start
 122
 123/-- **THEOREM EN-006.6**: Any transmutation path reduces total cost. -/
 124theorem path_reduces_total_cost (path : TransmutationPath) :
 125    nuclearCost path.finish ≤ nuclearCost path.start :=
 126  path.net_reduction
 127
 128/-- A stable configuration: J-cost = 0 (doubly-magic nucleus). -/
 129def stable_config : NuclearConfig := ⟨1, one_pos⟩
 130
 131/-- **THEOREM EN-006.7**: The stable configuration has zero cost. -/
 132theorem stable_config_zero_cost : nuclearCost stable_config = 0 := by
 133  unfold nuclearCost stable_config
 134  exact Jcost_unit0
 135
 136/-- **THEOREM EN-006.8**: Stable configuration is optimal (minimal cost). -/
 137theorem stable_is_optimal (cfg : NuclearConfig) :
 138    nuclearCost stable_config ≤ nuclearCost cfg := by
 139  rw [stable_config_zero_cost]
 140  exact nuclear_cost_nonneg cfg
 141
 142/-! ## §IV. Doubly-Magic Attractors -/
 143

papers checked against this theorem

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