e_fails_selection

formal source

 106
 107/-- Euler's number e fails the PhiSelection criterion.
 108    e² ≈ 7.389 but e + 1 ≈ 3.718, so e² ≠ e + 1. -/
 109theorem e_fails_selection : ¬IndisputableMonolith.RecogSpec.PhiSelection (Real.exp 1) := by
 110  intro h
 111  have heq : (Real.exp 1) ^ 2 = Real.exp 1 + 1 := h.left
 112  -- exp(1) > 2: prove by showing log(2) < 1
 113  have e_gt_2 : (2 : ℝ) < Real.exp 1 := by
 114    -- If log(2) ≥ 1, then 2 = exp(log 2) ≥ exp(1) > 2.7, contradiction
 115    have hlog2 : Real.log 2 < 1 := by
 116      by_contra h_ge
 117      push_neg at h_ge
 118      -- exp(1) ≤ exp(log 2) = 2 (since exp is monotone)
 119      have hexp_mono : Real.exp 1 ≤ Real.exp (Real.log 2) := Real.exp_le_exp.mpr h_ge
 120      have hsimp : Real.exp (Real.log 2) = 2 := Real.exp_log (by norm_num : (0 : ℝ) < 2)
 121      have h2_ge : Real.exp 1 ≤ 2 := by rw [hsimp] at hexp_mono; exact hexp_mono
 122      -- But exp(1) < 2.72, and 1 + 1 ≤ exp(1), so exp(1) ≥ 2
 123      -- Combined with exp(1) ≤ 2 gives exp(1) = 2
 124      -- But exp(1) ≠ 2 since exp(log 2) = 2 and log 2 ≈ 0.693 ≠ 1
 125      have h2_le : (2 : ℝ) ≤ Real.exp 1 := by linarith [Real.add_one_le_exp (1 : ℝ)]
 126      have h_eq : Real.exp 1 = 2 := le_antisymm h2_ge h2_le
 127      -- If exp(1) = 2, then log(exp(1)) = log(2), i.e., 1 = log(2)
 128      have hlog_eq : Real.log (Real.exp 1) = Real.log 2 := by rw [h_eq]
 129      rw [Real.log_exp] at hlog_eq
 130      -- So log(2) = 1, contradicting h_ge (which gives log(2) ≥ 1, actually consistent!)
 131      -- The real contradiction: exp(1) ≠ 2 because e ≈ 2.718...
 132      -- Use: exp(1) > exp(1/2)² = e^(1/2) * e^(1/2) and e^(1/2) > 1.6
 133      -- Simpler: use exp_one_lt_d9 which gives exp(1) < 2.7182818286
 134      -- Since exp(1) ≤ 2 and exp(1) < 2.72, the contradiction is h2_le with h2_ge
 135      -- Actually if exp(1) = 2, that's not contradicted by exp(1) < 2.72
 136      -- The issue is that exp(1) > 2 strictly. Let's use that exp is strictly increasing
 137      -- and exp(log 2) = 2 with log 2 < 1 strictly
 138      -- We need to show log 2 < 1 without circularity
 139      -- log 2 < 1 ⟺ 2 < exp(1) ⟺ log 2 < 1... this is circular