phiInv_lt_phi

formal source

  38  unfold phiInv
  39  exact (div_lt_one phi_pos).mpr one_lt_phi
  40
  41theorem phiInv_lt_phi : phiInv < phi := by
  42  have h := phi_pos
  43  have hone := one_lt_phi
  44  unfold phiInv
  45  calc 1 / phi < 1 := (div_lt_one h).mpr hone
  46    _ < phi := hone
  47
  48/-- 1/φ = φ - 1 (Fibonacci-phi identity).
  49    Proof: φ·(φ-1) = φ² - φ = (φ+1) - φ = 1, so φ-1 = 1/φ. -/
  50theorem phiInv_eq_phi_minus_one : phiInv = phi - 1 := by
  51  have hpos : phi ≠ 0 := ne_of_gt phi_pos
  52  have h2 : phi^2 = phi + 1 := phi_sq_eq
  53  have hkey : phi * (phi - 1) = 1 := by nlinarith [h2]
  54  -- 1/φ = (φ-1) iff φ·(φ-1) = 1
  55  unfold phiInv
  56  rw [eq_comm, eq_div_iff hpos]
  57  linarith [hkey]
  58
  59/-- 1/φ² = 2 - φ. Proof: φ²·(2-φ) = 2φ² - φ³ = 2(φ+1) - (2φ+1) = 1. -/
  60theorem phiInvSq_eq_two_minus_phi : 1 / phi^2 = 2 - phi := by
  61  have hpos : phi^2 ≠ 0 := ne_of_gt (pow_pos phi_pos 2)
  62  have h2 : phi^2 = phi + 1 := phi_sq_eq
  63  have h3 : phi^3 = 2 * phi + 1 := phi_cubed_eq
  64  have hkey : phi^2 * (2 - phi) = 1 := by nlinarith [h2, h3]
  65  rw [eq_comm, eq_div_iff hpos]
  66  linarith [hkey]
  67
  68/-- 1/φ³ = 2φ - 3 (= the Cabibbo-angle factor). -/
  69theorem phiInvCubed_eq_two_phi_minus_three : 1 / phi^3 = 2 * phi - 3 := by
  70  have hpos : phi^3 ≠ 0 := ne_of_gt (pow_pos phi_pos 3)
  71  have hsq : phi^2 = phi + 1 := phi_sq_eq