theorem
proved
cost_reduction_bounded
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Engineering.FissionTransmutationStructure on GitHub at line 106.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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. -/
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). -/