e_fails_selection
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.