phi_12_div_2

formal source

  98  norm_num
  99
 100/-- φ^12 / 2 ≈ 161. Uses algebraic identity: φ^12 = 144φ + 89 (from φ² = φ + 1). -/
 101theorem phi_12_div_2 : abs (phi ^ 12 / 2 - 161) < 1 := by
 102  -- Key identity: φ^12 = 144φ + 89 (Fibonacci recurrence)
 103  -- With φ ∈ (1.61, 1.62): φ^12 ∈ (320.84, 322.28), so φ^12/2 ∈ (160.42, 161.14)
 104  -- |φ^12/2 - 161| < max(0.58, 0.14) = 0.58 < 1
 105  have hlo : phi > 1.61 := phi_gt_onePointSixOne
 106  have hhi : phi < 1.62 := phi_lt_onePointSixTwo
 107  -- Derive φ^12 = 144φ + 89 using φ² = φ + 1
 108  have h_phi_sq : phi ^ 2 = phi + 1 := phi_sq_eq
 109  -- Build up powers using the recurrence
 110  have h_phi4 : phi ^ 4 = 3 * phi + 2 := by
 111    calc phi ^ 4 = (phi ^ 2) ^ 2 := by ring
 112      _ = (phi + 1) ^ 2 := by rw [h_phi_sq]
 113      _ = phi^2 + 2*phi + 1 := by ring
 114      _ = (phi + 1) + 2*phi + 1 := by rw [h_phi_sq]
 115      _ = 3 * phi + 2 := by ring
 116  have h_phi6 : phi ^ 6 = 8 * phi + 5 := by
 117    have h1 : phi ^ 6 = phi ^ 4 * phi ^ 2 := by ring
 118    rw [h1, h_phi4, h_phi_sq]
 119    ring_nf
 120    rw [h_phi_sq]
 121    ring
 122  have h_phi12 : phi ^ 12 = 144 * phi + 89 := by
 123    have h1 : phi ^ 12 = (phi ^ 6) ^ 2 := by ring
 124    rw [h1, h_phi6]
 125    ring_nf
 126    rw [h_phi_sq]
 127    ring
 128  -- Now compute bounds
 129  rw [h_phi12]
 130  have h_val_lo : (144 * phi + 89) / 2 > 160 := by linarith
 131  have h_val_hi : (144 * phi + 89) / 2 < 162 := by linarith