phiInv_lt_one

formal source

  34  unfold phiInv
  35  exact div_pos one_pos phi_pos
  36
  37theorem phiInv_lt_one : phiInv < 1 := by
  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