binding_dominates

formal source

  45theorem E_binding_pos : 0 < E_binding := by
  46  unfold E_binding r_binding; exact mass_on_rung_pos 14
  47
  48theorem binding_dominates : E_binding > 40 * m_valence := by
  49  unfold E_binding m_valence m_u_contrib m_d_contrib r_binding mass_on_rung
  50  have hA : 0 < Masses.Anchor.E_coh := anchor_E_coh_pos
  51  have h14_eq : phi ^ (14 : ℤ) = phi ^ (4 : ℤ) * phi ^ (10 : ℤ) := by
  52    rw [← zpow_add₀ phi_ne_zero]; norm_num
  53  rw [h14_eq]
  54  have h4_pos : 0 < phi ^ (4 : ℤ) := zpow_pos phi_pos _
  55  have h10_gt : phi ^ (10 : ℤ) > (120 : ℝ) := by
  56    have h5_eq : phi ^ (10 : ℤ) = phi ^ (5 : ℤ) * phi ^ (5 : ℤ) := by
  57      rw [← zpow_add₀ phi_ne_zero]; norm_num
  58    rw [h5_eq]
  59    have h5_gt : phi ^ (5 : ℤ) > (11 : ℝ) := by
  60      rw [zpow_ofNat]
  61      have : phi ^ 5 = 5 * phi + 3 := by
  62        have h3 : phi ^ 3 = 2 * phi + 1 := by
  63          calc phi ^ 3 = phi * phi ^ 2 := by ring
  64            _ = phi * (phi + 1) := by rw [phi_sq_eq]
  65            _ = phi ^ 2 + phi := by ring
  66            _ = (phi + 1) + phi := by rw [phi_sq_eq]
  67            _ = 2 * phi + 1 := by ring
  68        calc phi ^ 5 = phi ^ 2 * phi ^ 3 := by ring
  69          _ = (phi + 1) * (2 * phi + 1) := by rw [phi_sq_eq, h3]
  70          _ = 2 * phi ^ 2 + 3 * phi + 1 := by ring
  71          _ = 2 * (phi + 1) + 3 * phi + 1 := by rw [phi_sq_eq]
  72          _ = 5 * phi + 3 := by ring
  73      rw [this]; linarith [phi_gt_onePointSixOne]
  74    nlinarith [h5_gt]
  75  have h_base := mul_pos hA h4_pos
  76  nlinarith [mul_lt_mul_of_pos_left h10_gt h_base]
  77
  78def m_p : ℝ := m_valence + E_binding