pith. machine review for the scientific record. sign in
theorem proved tactic proof

nuclear_cost_zero_iff_stable

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  64theorem nuclear_cost_zero_iff_stable (cfg : NuclearConfig) :
  65    nuclearCost cfg = 0 ↔ cfg.ratio = 1 := by

proof body

Tactic-mode proof.

  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. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.