sqrt2_fails_selection

proof body

Tactic-mode proof.

  23  intro h
  24  have heq : (Real.sqrt 2) ^ 2 = Real.sqrt 2 + 1 := h.left
  25  -- (√2)² = 2 exactly
  26  have sqrt2_sq : (Real.sqrt 2) ^ 2 = 2 := Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)
  27  -- √2 > 1 (since 2 > 1)
  28  have sqrt2_gt_one : 1 < Real.sqrt 2 := by
  29    rw [← Real.sqrt_one]
  30    exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num : (1 : ℝ) < 2)
  31  -- So √2 + 1 > 2
  32  have h2lt : (2 : ℝ) < Real.sqrt 2 + 1 := by linarith [sqrt2_gt_one]
  33  -- Contradiction: 2 = (√2)² = √2 + 1 > 2
  34  have : (2 : ℝ) < 2 := by
  35    calc (2 : ℝ)
  36        < Real.sqrt 2 + 1 := h2lt
  37        _ = (Real.sqrt 2) ^ 2 := heq.symm
  38        _ = 2 := sqrt2_sq
  39  linarith
  40
  41/-- √3 fails the PhiSelection criterion.
  42    (√3)² = 3 but √3 + 1 ≈ 2.732, so (√3)² ≠ √3 + 1. -/