e_times_phi
This definition supplies the product of Euler's number and the golden ratio for use in Recognition Science explorations of exponential and self-similar constants. Researchers working on J-cost decay or phi-ladder normalizations would cite it when testing numerical links between e and phi. The declaration is a direct noncomputable abbreviation that multiplies exp(1) by the imported phi value.
claimLet $e = e^1$ and let $phi$ denote the golden ratio fixed point. The quantity $e times phi$ is the real number obtained by their ordinary product.
background
The Mathematics.Euler module targets derivation of Euler's number from phi-related summations. Euler's number is introduced as the base of the natural logarithm, the limit of (1 + 1/n)^n, and the series sum 1/n!. In Recognition Science, e is expected to arise from J-cost exponential decay, phi-related continued fractions, and 8-tick probability normalization. The module records that no simple algebraic relation between e and phi is known, yet lists several exploratory definitions including this product.
proof idea
The declaration is a direct noncomputable definition that applies the real multiplication operator to exp(1) and the phi constant imported from PhiForcing.
why it matters in Recognition Science
It forms one of the concrete attempts listed under the MATH-003 target of deriving e from phi-summation. The definition sits beside e_as_series, e_fixed_point, and e_over_phi, supporting the broader claim that e emerges from J-cost and phi-ladder structures. No downstream theorem yet consumes it, leaving open the question of whether a closed algebraic or numerical relation will appear.
scope and limits
- Does not establish any functional equation linking e and phi.
- Does not compute or bound the numerical value of the product.
- Does not reference physical constants or the forcing chain.
- Does not depend on any upstream lemma.
formal statement (Lean)
77noncomputable def e_times_phi : ℝ := exp 1 * phi