nuclear_cost_zero_iff_stable

formal source

  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 =>
  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