`transmutation_cost_pos`

proved

show as: view math explainer →

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

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

  80  · intro h; rw [h]; exact Jcost_unit0
  81
  82/-- **THEOREM EN-006.3**: Fission products (x ≠ 1) have positive transmutation cost. -/
  83theorem transmutation_cost_pos (cfg : NuclearConfig) (h : cfg.ratio ≠ 1) :
  84    0 < nuclearCost cfg := by
  85  have hge := nuclear_cost_nonneg cfg
  86  have hne : nuclearCost cfg ≠ 0 := fun hz =>
  87    h ((nuclear_cost_zero_iff_stable cfg).mp hz)
  88  exact lt_of_le_of_ne hge (Ne.symm hne)
  89
  90/-! ## §II. Transmutation Steps -/
  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

papers checked against this theorem

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