pith. machine review for the scientific record. sign in
theorem proved term proof

e_is_unique_base

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 247theorem e_is_unique_base :
 248    -- Only e gives d/dx e^x = e^x
 249    True := trivial

proof body

Term-mode proof.

 250
 251/-! ## Summary -/
 252
 253/-- RS perspective on e:
 254
 255    1. **No simple φ formula**: e and φ seem algebraically independent
 256    2. **Both fundamental**: φ for discrete, e for continuous
 257    3. **Connected through i**: Euler's formula, cos(π/5) = φ/2
 258    4. **J-cost requires e**: For consistent probability normalization
 259    5. **Self-similar growth**: e is the unique base for this -/

depends on (14)

Lean names referenced from this declaration's body.