sqrt2_fails_selection

formal source

  19
  20/-- √2 fails the PhiSelection criterion.
  21    (√2)² = 2 but √2 + 1 ≈ 2.414, so (√2)² ≠ √2 + 1. -/
  22theorem sqrt2_fails_selection : ¬IndisputableMonolith.RecogSpec.PhiSelection (Real.sqrt 2) := by
  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. -/
  43theorem sqrt3_fails_selection : ¬IndisputableMonolith.RecogSpec.PhiSelection (Real.sqrt 3) := by
  44  intro h
  45  have heq : (Real.sqrt 3) ^ 2 = Real.sqrt 3 + 1 := h.left
  46  have sqrt3_sq : (Real.sqrt 3) ^ 2 = 3 := Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 3)
  47  -- √3 < 2 (since 3 < 4 = 2²)
  48  have sqrt3_lt_two : Real.sqrt 3 < 2 := by
  49    have h4 : Real.sqrt 4 = 2 := by norm_num
  50    rw [← h4]
  51    exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num : (3 : ℝ) < 4)
  52  -- So √3 + 1 < 3