# Addition and strict positivity of the full exponential series

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-real-exponential-function/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-real-exponential-function-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

From E(x)=sum x^n/n!, prove absolute convergence for all real x, addition, inverses and positivity.

No derivative, logarithm, ODE, injectivity or transcendence claim.





## Givens and symbols


- algebra
- epsilon
- cauchy_product
- real_complete


- G1 — E(x) is the whole series x^n/n! over n≥0; x,y are arbitrary fixed real numbers.


- E(x) — whole power-series function
- u_n — absolute term
- m — arbitrary total degree





## Rules and sources

Some rule statements have reader clarifications in this revision: they are paraphrases, not verbatim quotations. Referenced original source bytes and hashes are unchanged.


- mko_definition · cited — Terms at x are x^n/n!, while the power-series coefficients 1/n! have ratio1/(n+1) tending to 0, giving infinite radius and absolute convergence for every fixed real x. The addition law needs the binomial coefficient identity at every degree and absolute convergence for Cauchy-product rearrangement; one declared degree checks only one coefficient. E(0)=1 and E(x)E(−x)=1. The half inverse identity makes E(x/2) nonzero before E(x)=E(x/2)^2 proves strict positivity. A finite partial-sum computation is not the whole exponential function, even where a special value coincides. Derivatives, logarithms, ODE uniqueness, injectivity and exact rational values at nonzero rational inputs are not automatic claims of this node. · mko-real-exponential-function
- algebra · prerequisite — Use real-field identities; division requires a nonzero denominator and multiplication by a positive number preserves inequalities.
- epsilon · prerequisite — Convergence requires for every positive epsilon an integer N controlling every n≥N by a strict error bound; use the Archimedean property of the reals.
- cauchy_product · prerequisite — The product of two absolutely convergent series equals their Cauchy product and may be grouped by total degree; the binomial theorem holds for every nonnegative integer degree.
- real_complete · prerequisite — Every nonempty bounded-above real set has a supremum, so bounded monotone real sequences converge, including bounded partial sums of nonnegative series.





## Main derivation

S01 · case_splitBefore

u_n=|x|^n/n!,\quad x\ne0

After

u_{n+1}/u_n=|x|/(n+1)

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

Fix x and compute the full absolute ratio; at x=0 only the initial term is one and all later terms vanish.



S02 · impliesBefore

N>2|x|,\quad n\ge N

After

u_{n+1}\le\tfrac12u_n,\quad u_{N+j}\le2^{-j}u_N

Conditions: N\in\mathbb N,\ N>2|x|

Rule: algebra · Uses: S01

Leaf basis: algebra

After selecting integer N, induction geometrically controls the entire tail.



S03 · impliesBefore

\sum_{j=0}^{M}u_{N+j}\le2u_N

After

\sum_{n=0}^{\infty}|x|^n/n!<\infty\quad\forall x\in\mathbb R

Conditions: \text{bounded monotone real sequences converge}

Rule: real_complete · Uses: S02, real_complete

Leaf basis: real_complete

Nonnegative tail partial sums are monotone and bounded by 2u_N; real completeness and a finite prefix give absolute convergence for every real x.



S04 · equivalentBefore

\sum_{k=0}^{m}\frac{x^ky^{m-k}}{k!(m-k)!}

After

\frac1{m!}\sum_{k=0}^{m}\binom mkx^ky^{m-k}=\frac{(x+y)^m}{m!}

Conditions: m\in\mathbb N_0

Rule: cauchy_product · Uses: G1, cauchy_product

Leaf basis: cauchy_product

For arbitrary degree m, the binomial theorem proves the coefficient identity for every degree, not just one selected m.



S05 · theorem_applicationBefore

E(x)E(y)=\sum_{m=0}^{\infty}\sum_{k=0}^{m}\frac{x^ky^{m-k}}{k!(m-k)!}

After

E(x)E(y)=E(x+y)

Conditions: none

Rule: cauchy_product · Uses: S03, S04

Leaf basis: cauchy_product

Absolute convergence first licenses the Cauchy product and regrouping by total degree; then use the identity at every degree.



S06 · impliesBefore

E(0)=1,\quad y=-x

After

E(x)E(-x)=1

Conditions: none

Rule: algebra · Uses: G1, S05

Leaf basis: algebra

The zero value comes from the sole nonzero initial term; addition then gives multiplicative inverses.



S07 · impliesBefore

E(x/2)E(-x/2)=1

After

E(x/2)\ne0

Conditions: none

Rule: algebra · Uses: S06

Leaf basis: algebra

First exclude zero using the half-point inverse identity, enabling strict positivity rather than only nonnegativity.



S08 · impliesBefore

E(x)=E(x/2+x/2)=E(x/2)^2

After

E(x)>0\quad\forall x\in\mathbb R

Conditions: none

Rule: algebra · Uses: S05, S07

Leaf basis: algebra

A nonzero real square is strictly positive, completing the full-function conclusion.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · S05, S07 — No finite partial sum at a nonzero rational point has been called exact E(x).
- S07 · premise_audit · S06 — A nonnegative square alone does not establish strict positivity.
- S06 · premise_audit · G1, S05 — Finite partial sums generally do not have this exact inverse property.
- S05 · premise_audit · S03, S04 — The coefficient identity and infinite regrouping are separate obligations, both supplied.
- S04 · inverse_equivalence · G1, cauchy_product — The factorial denominators are valid because 0≤k≤m.
- S03 · premise_audit · S02, real_complete — This step assumes real bounded-monotone convergence, not sampled finite M values.
- S02 · premise_audit · S01 — N may depend on the fixed x, but the bound covers every j.
- S01 · premise_audit · G1 — No ratio division by a zero term is performed at x=0.





## Error controls and negative controls

Whole seriesSeparate the full E from finite S_N.

Nonzero firstUse inverses to exclude zero before deriving positivity from a square.


- A finite partial sum is the general exact E(x). → reject — It omits an infinite tail; equality requires a separately proved special value.
- Checking degree three alone proves addition. → reject — Every degree identity and absolute regrouping are required.
- The square identity alone proves strict positivity. → reject — E(x/2)=0 must first be excluded.





## Result and limitations

E converges absolutely on R and satisfies addition, E(0)=1, E(x)E(-x)=1 and E(x)>0.







## Verification and source binding

1 declared checks for this guide; only the listed expressions are covered.


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: a1687161d95b6c66cce720bd37cdfa330f5a9bfd717247f0fa87c5f638f6ca35
- original source SHA-256: ea4e23ef55650baa4c70e04bfc52f0293ed62cfd1b2f52bb15cc8695fe035c75
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-real-exponential-function-01.json)