e_fails_selection
Euler's number fails the PhiSelection equation x² = x + 1. Researchers ruling out alternative scaling constants in Recognition Science cite this to isolate the golden ratio. The proof assumes the equation, proves e > 2 using bounds on exp(1/2), squares to get e² > 4, then uses e < 3 to force the impossible 4 < e + 1 < 4.
claimThe number $e := e^1$ does not satisfy the equation $x^2 = x + 1$.
background
The module proves that several common constants fail the PhiSelection predicate to establish uniqueness of phi. PhiSelection holds precisely when a positive real satisfies the quadratic x² = x + 1. This counters the numerology objection by explicit counterexamples. The setting draws on real analysis properties of the exponential function.
proof idea
Assume the selection equation for e, yielding e² = e + 1. Prove e > 2 by contradiction on log 2 >=1, using add_one_le_exp on 1/2 to reach e >= 2.25. Square both sides of e > 2 to obtain e² > 4. Apply exp_one_lt_d9 to bound e < 2.718 < 3, so e + 1 < 4. The chain 4 < e² = e + 1 < 4 yields the contradiction via linarith.
why it matters in Recognition Science
Feeds the bundle theorem common_constants_fail_selection that collects failures for e, pi, sqrt(2), sqrt(3), sqrt(5). This shows phi is the unique solution to the selection equation among tested constants, supporting the claim that phi arises necessarily from the structure rather than choice. Aligns with the forcing of phi as self-similar fixed point in the unified chain.
scope and limits
- Does not establish that phi is the sole positive real solution to x² = x + 1.
- Does not apply the failure to constants outside the five tested.
- Does not derive any physical predictions from the failure.
- Limits the argument to real numbers and the specific equation.
formal statement (Lean)
109theorem e_fails_selection : ¬IndisputableMonolith.RecogSpec.PhiSelection (Real.exp 1) := by
proof body
Tactic-mode proof.
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. -/