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

目標與範圍

從 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，故單調有界實數列收斂；這也適用非負級數有界部分和。

逐步主鏈

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

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

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

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

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

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

\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!}

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)

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

E(x)E(-x)=1

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

E(x/2)\ne0

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

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

局部子步與引理

本稿無局部子步。

逐步反向審查

• 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、反控制與修訂記錄）