massAtAnchor

formal source

 101@[simp] theorem M0_pos : 0 < M0 := by
 102  dsimp [M0]; norm_num
 103
 104noncomputable def massAtAnchor (f : Fermion) : ℝ :=
 105  M0 * Real.exp (((rung f : ℝ) - 8 + gap (ZOf f)) * Real.log (Constants.phi))
 106
 107theorem anchor_ratio (f g : Fermion) (hZ : ZOf f = ZOf g) :
 108  massAtAnchor f / massAtAnchor g =
 109    Real.exp (((rung f : ℝ) - rung g) * Real.log (Constants.phi)) := by
 110  unfold massAtAnchor
 111  set Af := ((rung f : ℝ) - 8 + gap (ZOf f)) * Real.log (Constants.phi)
 112  set Ag := ((rung g : ℝ) - 8 + gap (ZOf g)) * Real.log (Constants.phi)
 113  -- Since M0=1, factor cancels directly
 114  calc
 115    (M0 * Real.exp Af) / (M0 * Real.exp Ag)
 116        = (Real.exp Af) / (Real.exp Ag) := by simpa [M0]
 117    _ = Real.exp (Af - Ag) := by
 118              simpa [Real.exp_sub] using (Real.exp_sub Af Ag).symm
 119    _ = Real.exp ((((rung f : ℝ) - 8 + gap (ZOf f)) - ((rung g : ℝ) - 8 + gap (ZOf g)))
 120                   * Real.log (Constants.phi)) := by
 121              have : Af - Ag
 122                    = (((rung f : ℝ) - 8 + gap (ZOf f)) - ((rung g : ℝ) - 8 + gap (ZOf g)))
 123                       * Real.log (Constants.phi) := by
 124                        simp [Af, Ag, sub_eq_add_neg, add_comm, add_left_comm, add_assoc,
 125                              mul_add, add_mul]
 126              have h' :
 127                ((rung f : ℝ) - 8 + gap (ZOf f)) - ((rung g : ℝ) - 8 + gap (ZOf g))
 128                = (rung f : ℝ) - rung g + (gap (ZOf f) - gap (ZOf g)) := by ring
 129              simpa [this, h']
 130    _ = Real.exp (((rung f : ℝ) - rung g) * Real.log (Constants.phi)) := by
 131              simpa [hZ, sub_self, add_zero, add_comm, add_left_comm, add_assoc, mul_add,
 132                     add_right_comm, mul_comm, mul_left_comm, mul_assoc]
 133
 134structure ResidueCert where