phi_plus_inv

formal source

  84  exact this
  85
  86/-- **The φ-sum identity**: φ + φ⁻¹ = √5. -/
  87theorem phi_plus_inv : phi + phi⁻¹ = Real.sqrt 5 := by
  88  rw [phi_inv_eq]
  89  simp only [phi]
  90  ring
  91
  92/-- **J(φ) exact formula**: J(φ) = (√5 − 2)/2. -/
  93theorem Jcost_phi_exact : Jcost phi = (Real.sqrt 5 - 2) / 2 := by
  94  unfold Jcost
  95  rw [phi_plus_inv]
  96  ring
  97
  98/-- **J(φ) = φ − 3/2**: the elementary closed form. -/
  99theorem Jcost_phi_eq_phi_minus_half : Jcost phi = phi - 3/2 := by
 100  rw [Jcost_phi_exact]
 101  simp only [phi]
 102  ring
 103
 104/-- **The mass gap constant**: the exact RS Yang-Mills mass gap. -/
 105def massGap : ℝ := (Real.sqrt 5 - 2) / 2
 106
 107/-- J(φ) equals the gap constant. -/
 108theorem Jcost_phi_eq_massGap : Jcost phi = massGap := Jcost_phi_exact
 109
 110/-! ## §2  Strict Positivity of the Mass Gap -/
 111
 112/-- **√5 > 2**: key bound for positivity. -/
 113private lemma sqrt5_gt_two : (2 : ℝ) < Real.sqrt 5 := by
 114  rw [show (2 : ℝ) = Real.sqrt 4 by
 115    rw [show (4 : ℝ) = 2 ^ 2 by norm_num]
 116    exact (Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2)).symm]
 117  exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)