sqrt5_fails_selection

proof body

Tactic-mode proof.

  66  intro h
  67  have heq : (Real.sqrt 5) ^ 2 = Real.sqrt 5 + 1 := h.left
  68  have sqrt5_sq : (Real.sqrt 5) ^ 2 = 5 := Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 5)
  69  -- √5 < 3 (since 5 < 9 = 3²)
  70  have sqrt5_lt_three : Real.sqrt 5 < 3 := by
  71    have h9 : Real.sqrt 9 = 3 := by norm_num
  72    rw [← h9]
  73    exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num : (5 : ℝ) < 9)
  74  -- So √5 + 1 < 4 < 5
  75  have h5gt : Real.sqrt 5 + 1 < 5 := by linarith [sqrt5_lt_three]
  76  -- Contradiction: 5 = (√5)² = √5 + 1 < 5
  77  have : (5 : ℝ) < 5 := by
  78    calc (5 : ℝ)
  79        = (Real.sqrt 5) ^ 2 := sqrt5_sq.symm
  80        _ = Real.sqrt 5 + 1 := heq
  81        _ < 5 := h5gt
  82  linarith
  83
  84/-- π fails the PhiSelection criterion.
  85    π² ≈ 9.870 but π + 1 ≈ 4.142, so π² ≠ π + 1. -/