e_ne_phi
plain-language theorem explainer
Euler's number differs from the golden ratio. Researchers deriving e from phi-summations in Recognition Science would cite the separation to keep the constants distinct in J-cost and fixed-point arguments. The result follows at once from the prior strict inequality e > phi.
Claim. $e = e^1$ is not equal to the golden ratio $phi = (1 + sqrt(5))/2$.
background
The Mathematics.Euler module (MATH-003) derives Euler's number from phi-related summations, presenting e as the base of the natural logarithm, the limit of (1 + 1/n)^n, and the series sum 1/n!. In Recognition Science, e arises from J-cost exponential decay and 8-tick probability normalization, while phi is the self-similar fixed point. The upstream lemma e_gt_phi establishes phi < exp(1) by combining phi_lt_two, e_gt_two, and linarith.
proof idea
One-line term proof that applies ne_of_gt directly to the theorem e_gt_phi.
why it matters
The declaration supplies the explicit distinction required by the module's known-relationship section, which notes the absence of any simple algebraic link between e and phi. It supports the broader forcing-chain separation of phi (T6 fixed point) from e (summation-derived). No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.