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

jcost_energy_zero_iff_ground

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)

 119theorem jcost_energy_zero_iff_ground (x : ℝ) (hx : 0 < x) :
 120    jcost_energy x hx = 0 ↔ x = 1 := by

proof body

Tactic-mode proof.

 121  unfold jcost_energy
 122  constructor
 123  · intro h
 124    have hEcoh : E_coh_storage ≠ 0 := E_coh_storage_pos.ne'
 125    have hJ : Jcost x = 0 := by
 126      rwa [mul_eq_zero, or_iff_right hEcoh] at h
 127    rw [Jcost_eq_sq hx.ne'] at hJ
 128    have hden : 0 < 2 * x := by linarith
 129    have hnum : (x - 1) ^ 2 = 0 := by
 130      have := div_eq_zero_iff.mp hJ
 131      exact this.resolve_right (ne_of_gt hden)
 132    by_contra hne
 133    have hpos : 0 < (x - 1) ^ 2 := by
 134      rw [← sq_abs]; exact pow_pos (abs_pos.mpr (sub_ne_zero.mpr hne)) 2
 135    linarith
 136  · intro h; rw [h]; simp [Jcost_unit0]
 137
 138/-- **THEOREM EN-004.9**: Ground state has minimum energy. -/

used by (1)

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

depends on (9)

Lean names referenced from this declaration's body.