jcost_energy

formal source

 107/-! ## §III. J-Cost Energy Storage -/
 108
 109/-- J-cost energy stored in a recognition event with ratio x. -/
 110def jcost_energy (x : ℝ) (hx : 0 < x) : ℝ := E_coh_storage * Jcost x
 111
 112/-- **THEOREM EN-004.7**: J-cost energy is non-negative. -/
 113theorem jcost_energy_nonneg (x : ℝ) (hx : 0 < x) : 0 ≤ jcost_energy x hx := by
 114  unfold jcost_energy
 115  apply mul_nonneg E_coh_storage_pos.le
 116  exact Jcost_nonneg hx
 117
 118/-- **THEOREM EN-004.8**: J-cost energy is zero iff x = 1 (ground state). -/
 119theorem jcost_energy_zero_iff_ground (x : ℝ) (hx : 0 < x) :
 120    jcost_energy x hx = 0 ↔ x = 1 := by
 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. -/
 139theorem jcost_energy_min_at_ground (x : ℝ) (hx : 0 < x) :
 140    jcost_energy 1 one_pos ≤ jcost_energy x hx := by