IndisputableMonolith.PhiSupport.Alternatives

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.RecogSpec.PhiSelectionCore
   4
   5namespace IndisputableMonolith
   6namespace PhiSupport
   7namespace Alternatives
   8
   9/-!
  10# Alternative Scaling Constants Fail Selection
  11
  12This module explicitly proves that common mathematical constants (e, π, √2, √3, √5)
  13do NOT satisfy the PhiSelection criterion, demonstrating that φ is uniquely determined
  14by the mathematical structure rather than being an arbitrary choice.
  15
  16This addresses the "numerology objection" by showing that φ is the ONLY positive real
  17satisfying the selection equation x² = x + 1.
  18-/
  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
  53  have h3gt : Real.sqrt 3 + 1 < 3 := by linarith [sqrt3_lt_two]
  54  -- Contradiction: 3 = (√3)² = √3 + 1 < 3
  55  have : (3 : ℝ) < 3 := by
  56    calc (3 : ℝ)
  57        = (Real.sqrt 3) ^ 2 := sqrt3_sq.symm
  58        _ = Real.sqrt 3 + 1 := heq
  59        _ < 3 := h3gt
  60  linarith
  61
  62/-- √5 fails the PhiSelection criterion, despite being related to φ.
  63    (√5)² = 5 but √5 + 1 ≈ 3.236, so (√5)² ≠ √5 + 1.
  64    Note: φ = (1 + √5)/2, but √5 itself is not the solution. -/
  65theorem sqrt5_fails_selection : ¬IndisputableMonolith.RecogSpec.PhiSelection (Real.sqrt 5) := by
  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. -/
  86theorem pi_fails_selection : ¬IndisputableMonolith.RecogSpec.PhiSelection Real.pi := by
  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. -/
 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
 140      -- Break it: log 2 = 0.693... < 1 numerically
 141      -- In Mathlib, we might have a direct bound
 142      -- For now, use that if log 2 = 1, then exp(log 2) = exp(1), so 2 = exp(1)
 143      -- but exp(1) = e ≈ 2.718 ≠ 2
 144      -- The bound exp_one_lt_d9 says exp(1) < 2.7182818286
 145      -- If exp(1) = 2, then 2 < 2.72, which is true, no contradiction yet
 146      -- We need exp(1) > 2, not just exp(1) ≤ 2.72
 147      -- Use exp(1) ≥ 1 + 1 + 1/2 = 2.5 from Taylor. But add_one_le_exp only gives ≥ 2
 148      -- Actually, use exp(1/2) > 1 + 1/2 = 1.5, so exp(1) = exp(1/2)² > 2.25 > 2
 149      have h_half := Real.add_one_le_exp (1/2 : ℝ)
 150      have h_half_bound : (1.5 : ℝ) ≤ Real.exp (1/2) := by linarith
 151      have h_sq : Real.exp 1 = Real.exp (1/2) * Real.exp (1/2) := by
 152        rw [← Real.exp_add]; norm_num
 153      have h_exp1_bound : (2.25 : ℝ) ≤ Real.exp 1 := by
 154        rw [h_sq]
 155        have : (1.5 : ℝ) * 1.5 = 2.25 := by norm_num
 156        calc Real.exp (1/2) * Real.exp (1/2)
 157            ≥ 1.5 * 1.5 := mul_le_mul h_half_bound h_half_bound (by norm_num) (by linarith)
 158            _ = 2.25 := by norm_num
 159      linarith
 160    have h2pos : (0 : ℝ) < 2 := by norm_num
 161    calc (2 : ℝ)
 162        = Real.exp (Real.log 2) := (Real.exp_log h2pos).symm
 163        _ < Real.exp 1 := Real.exp_lt_exp.mpr hlog2
 164  -- So e² > 4
 165  have e_sq_gt_4 : (4 : ℝ) < (Real.exp 1) ^ 2 := by
 166    have h2sq : (2 : ℝ) ^ 2 = 4 := by norm_num
 167    rw [← h2sq]
 168    exact sq_lt_sq' (by linarith) e_gt_2
 169  -- exp(1) < 2.72 < 3 (from Mathlib)
 170  have e_lt_3 : Real.exp 1 < 3 := by
 171    have : Real.exp 1 < 2.7182818286 := Real.exp_one_lt_d9
 172    linarith
 173  have e_plus_1_lt_4 : Real.exp 1 + 1 < 4 := by linarith
 174  -- Contradiction: 4 < e² = e + 1 < 4
 175  have : (4 : ℝ) < 4 := by
 176    calc (4 : ℝ)
 177        < (Real.exp 1) ^ 2 := e_sq_gt_4
 178        _ = Real.exp 1 + 1 := heq
 179        _ < 4 := e_plus_1_lt_4
 180  linarith
 181
 182/-! ### Summary theorem: Common constants all fail
 183
 184This packages the above results into a single statement showing that
 185none of the common mathematical constants satisfy the selection criterion.
 186-/
 187
 188/-- Bundle theorem: All tested common constants fail PhiSelection.
 189    This demonstrates that φ is not an arbitrary choice from among "nice" constants. -/
 190theorem common_constants_fail_selection :
 191  ¬IndisputableMonolith.RecogSpec.PhiSelection (Real.exp 1) ∧
 192  ¬IndisputableMonolith.RecogSpec.PhiSelection Real.pi ∧
 193  ¬IndisputableMonolith.RecogSpec.PhiSelection (Real.sqrt 2) ∧
 194  ¬IndisputableMonolith.RecogSpec.PhiSelection (Real.sqrt 3) ∧
 195  ¬IndisputableMonolith.RecogSpec.PhiSelection (Real.sqrt 5) := by
 196  exact ⟨e_fails_selection, pi_fails_selection, sqrt2_fails_selection,
 197         sqrt3_fails_selection, sqrt5_fails_selection⟩
 198
 199/-! ### Uniqueness emphasis
 200
 201Combined with phi_unique_pos_root from PhiSupport.lean, these results show:
 2021. φ is the ONLY positive solution to x² = x + 1 (constructive uniqueness)
 2032. Common alternatives (e, π, √2, √3, √5) all fail the criterion (exclusion)
 2043. Therefore φ is mathematically forced, not chosen by fitting
 205-/
 206
 207end Alternatives
 208end PhiSupport
 209end IndisputableMonolith
 210