E_PBM_bounds

formal source

 102  mul_pos phi_pos eV_to_J_pos
 103
 104/-- E_PBM bounded by φ bounds: E_PBM ∈ (1.61, 1.62) eV. -/
 105lemma E_PBM_bounds :
 106    1.61 * eV_to_J < E_PBM ∧ E_PBM < 1.62 * eV_to_J :=
 107  ⟨mul_lt_mul_of_pos_right phi_gt_onePointSixOne eV_to_J_pos,
 108   mul_lt_mul_of_pos_right phi_lt_onePointSixTwo eV_to_J_pos⟩
 109
 110/-- E_PBM equals rung 6 on the φ-energy ladder:
 111    E_base · φ⁶ = φ⁻⁵ eV · φ⁶ = φ eV = E_PBM. -/
 112theorem E_PBM_is_rung_6 : E_PBM = phi_energy_rung 6 := by
 113  unfold E_PBM phi_energy_rung E_base
 114  have key : phi ^ (-(5 : ℝ)) * phi ^ (6 : ℝ) = phi := by
 115    rw [← Real.rpow_add phi_pos,
 116        (by norm_num : (-(5 : ℝ) + (6 : ℝ) : ℝ) = (1 : ℝ)),
 117        Real.rpow_one]
 118  have h : phi ^ (-(5 : ℝ)) * eV_to_J * phi ^ (6 : ℝ) = phi * eV_to_J := by
 119    calc phi ^ (-(5 : ℝ)) * eV_to_J * phi ^ (6 : ℝ)
 120        = phi ^ (-(5 : ℝ)) * phi ^ (6 : ℝ) * eV_to_J := by ring
 121      _ = phi * eV_to_J := by rw [key]
 122  exact h.symm
 123
 124/-- Division bounds helper: transfers E_PBM bounds to any positive numerator. -/
 125private lemma div_bounds_of_E_PBM {K : ℝ} (hK : 0 < K) :
 126    K / (1.62 * eV_to_J) < K / E_PBM ∧
 127      K / E_PBM < K / (1.61 * eV_to_J) := by
 128  have ⟨h_lower, h_upper⟩ := E_PBM_bounds
 129  have h_upper_pos : 0 < 1.62 * eV_to_J :=
 130    mul_pos (by norm_num) eV_to_J_pos
 131  have h_lower_pos : 0 < 1.61 * eV_to_J :=
 132    mul_pos (by norm_num) eV_to_J_pos
 133  have h1 := one_div_lt_one_div_of_lt E_PBM_pos h_upper
 134  have h2 := one_div_lt_one_div_of_lt h_lower_pos h_lower
 135  constructor