`TransmutationStep`

definition

show as: view math explainer →

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

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

  91
  92/-- A transmutation step: configuration changes from ratio x to ratio y.
  93    Valid iff it reduces J-cost (towards stability). -/
  94structure TransmutationStep where
  95  initial : NuclearConfig
  96  final : NuclearConfig
  97  /-- Each step reduces J-cost. -/
  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) :

papers checked against this theorem

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