e_gt_two
plain-language theorem explainer
Researchers comparing Euler's number to the golden ratio in Recognition Science cite the fact that exp(1) exceeds 2. This inequality follows from the strict convexity of the exponential function. The proof invokes the standard library result that 1 + x < exp(x) for x not zero and concludes via linear arithmetic.
Claim. $e > 2$, where $e = {exp}(1)$.
background
The Mathematics.Euler module targets derivation of Euler's number e from φ-related summations under MATH-003. e is the base of the natural logarithm, the limit of (1 + 1/n)^n, and the sum of the series 1/n!. In Recognition Science, e emerges from J-cost exponential decay, φ-related continued fractions, and 8-tick probability normalization.
proof idea
The proof applies the Mathlib lemma Real.add_one_lt_exp to the nonzero real 1, yielding 1 + 1 < exp(1). Linear arithmetic then closes the claim exp(1) > 2.
why it matters
e_gt_two is invoked by e_gt_one and e_gt_phi to establish e > 1 and e > φ. It supports the module's exploration of e-φ connections within Recognition Science, where e is tied to J-cost decay and the eight-tick normalization. No simple algebraic relation between e and φ is asserted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.