`nuclearCost`

definition

show as: view math explainer →

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

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

  53  ratio_pos : 0 < ratio
  54
  55/-- The J-cost (instability measure) of a nuclear configuration. -/
  56def nuclearCost (cfg : NuclearConfig) : ℝ := Jcost cfg.ratio
  57
  58/-- **THEOREM EN-006.1**: Nuclear cost is non-negative. -/
  59theorem nuclear_cost_nonneg (cfg : NuclearConfig) : 0 ≤ nuclearCost cfg :=
  60  Jcost_nonneg cfg.ratio_pos
  61
  62/-- **THEOREM EN-006.2**: Nuclear cost is zero iff the nucleus is in the ground state
  63    (doubly-magic, x = 1). -/
  64theorem nuclear_cost_zero_iff_stable (cfg : NuclearConfig) :
  65    nuclearCost cfg = 0 ↔ cfg.ratio = 1 := by
  66  unfold nuclearCost
  67  constructor
  68  · intro h
  69    rw [Jcost_eq_sq cfg.ratio_pos.ne'] at h
  70    have hden : 0 < 2 * cfg.ratio := by linarith [cfg.ratio_pos]
  71    have hnum : (cfg.ratio - 1) ^ 2 = 0 := by
  72      have := div_eq_zero_iff.mp h
  73      exact this.resolve_right (ne_of_gt hden)
  74    have hne' : cfg.ratio - 1 = 0 := by
  75      by_contra h'
  76      have hpos : 0 < (cfg.ratio - 1) ^ 2 := by
  77        rw [← sq_abs]; exact pow_pos (abs_pos.mpr h') 2
  78      linarith
  79    linarith
  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 =>

papers checked against this theorem

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