pi_fails_selection

proof body

Tactic-mode proof.

  87  intro h
  88  have heq : Real.pi ^ 2 = Real.pi + 1 := h.left
  89  -- π > 3 (from Mathlib)
  90  have pi_gt_3 : (3 : ℝ) < Real.pi := Real.pi_gt_three
  91  -- So π² > 9
  92  have pi_sq_gt_9 : (9 : ℝ) < Real.pi ^ 2 := by
  93    have h3sq : (3 : ℝ) ^ 2 = 9 := by norm_num
  94    rw [← h3sq]
  95    exact sq_lt_sq' (by linarith) pi_gt_3
  96  -- But π < 4, so π + 1 < 5
  97  have pi_lt_4 : Real.pi < 4 := Real.pi_lt_four
  98  have pi_plus_1_lt_5 : Real.pi + 1 < 5 := by linarith
  99  -- Contradiction: 9 < π² = π + 1 < 5
 100  have : (9 : ℝ) < 5 := by
 101    calc (9 : ℝ)
 102        < Real.pi ^ 2 := pi_sq_gt_9
 103        _ = Real.pi + 1 := heq
 104        _ < 5 := pi_plus_1_lt_5
 105  linarith
 106
 107/-- Euler's number e fails the PhiSelection criterion.
 108    e² ≈ 7.389 but e + 1 ≈ 3.718, so e² ≠ e + 1. -/