nuclear_chemical_ratio

formal source

  97  exact one_lt_zpow₀ one_lt_phi (by norm_num)
  98
  99/-- The nuclear-to-chemical energy ratio is φ^45. -/
 100def nuclear_chemical_ratio : ℝ := phi ^ (45 : ℕ)
 101
 102/-- **THEOREM EN-004.5**: Nuclear/chemical energy ratio > 1 (φ^45 > 1). -/
 103theorem nuclear_chemical_ratio_gt_one : 1 < nuclear_chemical_ratio := by
 104  unfold nuclear_chemical_ratio
 105  exact one_lt_pow₀ one_lt_phi (by norm_num)
 106
 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