theorem
proved
transmutation_reduces_cost
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 101.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
98 reduces_cost : nuclearCost final ≤ nuclearCost initial
99
100/-- **THEOREM EN-006.4**: Transmutation reduces or maintains cost. -/
101theorem transmutation_reduces_cost (step : TransmutationStep) :
102 nuclearCost step.final ≤ nuclearCost step.initial :=
103 step.reduces_cost
104
105/-- **THEOREM EN-006.5**: Transmutation cost reduction is bounded by initial cost. -/
106theorem cost_reduction_bounded (step : TransmutationStep) :
107 nuclearCost step.initial - nuclearCost step.final ≤ nuclearCost step.initial := by
108 linarith [nuclear_cost_nonneg step.final]
109
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. -/