e_pos
plain-language theorem explainer
The positivity of Euler's number e follows directly from the range of the exponential function. Researchers deriving constants via φ-summations in Recognition Science cite it to anchor basic inequalities before addressing series or limits. The proof applies the standard exponential positivity lemma in one step.
Claim. The number $e = e^1$ is strictly positive: $e > 0$.
background
Module MATH-003 derives Euler's number from φ-related summations. In Recognition Science, e arises via J-cost exponential decay, φ-continued fractions, and 8-tick normalization. The upstream structure from NucleosynthesisTiers records that physical quantities sit on discrete φ-tiers, with nuclear density scaling as φ to an integer power times Planck density. The PhiForcingDerived structure encodes the J-cost functional.
proof idea
One-line wrapper that applies the Mathlib lemma establishing positivity of the real exponential at every real input, instantiated at 1.
why it matters
The result supplies the minimal positivity fact required for e in the φ-summation setting. It supports downstream divisor-exponent constructions in Erdos-Straus box phases, where component positivity closes the balanced-pair support. It aligns with the module target of extracting e from J-cost decay without invoking the forcing chain T0-T8 or the Euler-Mascheroni constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.