m_u_contrib

formal source

  31private lemma mass_on_rung_pos (r : ℤ) : 0 < mass_on_rung r :=
  32  mul_pos anchor_E_coh_pos (zpow_pos phi_pos _)
  33
  34def m_u_contrib : ℝ := mass_on_rung 4
  35def m_d_contrib : ℝ := mass_on_rung 4
  36def m_valence : ℝ := 2 * m_u_contrib + m_d_contrib
  37
  38theorem m_valence_pos : 0 < m_valence := by
  39  unfold m_valence m_u_contrib m_d_contrib
  40  linarith [mass_on_rung_pos 4]
  41
  42def r_binding : ℤ := 14
  43def E_binding : ℝ := mass_on_rung r_binding
  44
  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]