# 全級數的加法律與嚴格正性

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-real-exponential-function/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

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



## 目標與範圍

從 E(x)=sum x^n/n! 證全實數絕對收斂、加法律、逆元與正性。

不引入導數、log、ODE、單射或超越性。





## 已知條件與符號


- algebra
- epsilon
- cauchy_product
- real_complete


- G1 — E(x) 定義為 n≥0 的全級數 x^n/n!；x,y 為任意固定實數。


- E(x) — 完整冪級數函數
- u_n — 絕對項
- m — 任意總次數





## 規則與來源

本稿部分規則文字經本輪讀者釐清，屬於改述而非逐字引文；被引用的原始來源內容及雜湊沒有改動。


- mko_definition · cited — 完整級數在 x 處的項為 x^n/n!，而冪級數係數為 1/n!；係數相鄰比 1/(n+1) 趨 0，因此 radius 為 infinity 且對每個實 x 絕對收斂。Addition law 需對所有 degree 使用二項式係數合併 Cauchy product，且重排責任由絕對收斂支撐；單一 declared degree 只核一個係數。E(0)=1；E(x)E(-x)=1，且 E(x/2)E(-x/2)=1 先給 E(x/2) 非零，再由 E(x)=E(x/2)^2 推出嚴格正。有限 partial sum 不是 E(x)，也不由本節點自動推出導數、log、ODE 唯一性、injectivity 或非零有理點的 exact rational value。 · mko-real-exponential-function
- algebra · prerequisite — 實數域的等式運算；除法前分母必非零，不等式乘正數保持方向。
- epsilon · prerequisite — 收斂表示每個正 epsilon 有一個整數 N，使全部 n≥N 的誤差嚴格小於 epsilon；使用實數 Archimedean 性。
- cauchy_product · prerequisite — 兩個絕對收斂級數的乘積等於其 Cauchy product，且可依總次數重排；二項式定理對每個非負整數 degree 成立。
- real_complete · prerequisite — 非空有上界的實集合有 supremum，故單調有界實數列收斂；這也適用非負級數有界部分和。





## 逐步主鏈

S01 · case_split操作前

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

操作後

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

條件：無

規則：algebra · 依賴：G1

葉節點依據：algebra

先固定 x 計算完整相鄰絕對比；x=0 則首項為 1、其餘全零。



S02 · implies操作前

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

操作後

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

條件：N\in\mathbb N,\ N>2|x|

規則：algebra · 依賴：S01

葉節點依據：algebra

選整數 N 後歸納幾何控制整個尾項。



S03 · implies操作前

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

操作後

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

條件：\text{bounded monotone real sequences converge}

規則：real_complete · 依賴：S02, real_complete

葉節點依據：real_complete

非負尾部分和單調有界（實數完備性），有限前綴不影響收斂，故全實數絕對收斂。



S04 · equivalent操作前

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

操作後

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

條件：m\in\mathbb N_0

規則：cauchy_product · 依賴：G1, cauchy_product

葉節點依據：cauchy_product

對任意 degree m 以二項式定理核全體係數恆等式，不只一個選定 m。



S05 · theorem_application操作前

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

操作後

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

條件：無

規則：cauchy_product · 依賴：S03, S04

葉節點依據：cauchy_product

兩級數絕對收斂先允許 Cauchy product 與按總次數重排，再用所有 degree 的恆等式。



S06 · implies操作前

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

操作後

E(x)E(-x)=1

條件：無

規則：algebra · 依賴：G1, S05

葉節點依據：algebra

零值由唯一非零首項給出，再以加法律得乘法逆元。



S07 · implies操作前

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

操作後

E(x/2)\ne0

條件：無

規則：algebra · 依賴：S06

葉節點依據：algebra

先以半點逆元性排除零，之後才能證嚴格正而不只是非負。



S08 · implies操作前

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

操作後

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

條件：無

規則：algebra · 依賴：S05, S07

葉節點依據：algebra

實數非零平方嚴格正，完成全函數的結論。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · S05, S07 — 此證明沒有將非零有理點的有限部分和稱為 exact E(x)。
- S07 · premise_audit · S06 — 不能從平方非負單獨推出嚴格正。
- S06 · premise_audit · G1, S05 — 有限部分和通常沒有此精確逆元性。
- S05 · premise_audit · S03, S04 — 係數恆等式與無窮重排是不同責任，都已列前提。
- S04 · inverse_equivalence · G1, cauchy_product — factorial 分母滿足 0≤k≤m，所以均合法。
- S03 · premise_audit · S02, real_complete — 需實數單調有界收斂性作此步前提，而非有限 M 抽樣。
- S02 · premise_audit · S01 — N 可依固定 x，但 j 的界是全稱。
- S01 · premise_audit · G1 — 不在 x=0 的零項上做除零比值。





## 錯誤控制與反例

全級數區分完整 E 與有限 S_N。

先非零用逆元性再用平方推出嚴格正。


- 有限部分和等於一般 exact E(x)。 → reject — 仍缺非零無窮尾，除特值另證外不能如此等同。
- 驗 m=3 係數足以證加法律。 → reject — 需每個 m 的二項式恆等式與絕對重排依據。
- E(x)=E(x/2)^2 單獨就證 >0。 → reject — 必先排除 E(x/2)=0。





## 結論與限制

E 全實數絕對收斂，滿足 E(x+y)=E(x)E(y)、E(0)=1、E(x)E(-x)=1 且 E(x)>0。







## 驗證及來源綁定

1 個本稿宣告算術檢查；只支持所列算式。


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

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-real-exponential-function-01.json)