# 標準常態的對稱推導與named facts

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

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

derivation-mko-standard-normal-distribution-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

清楚分開Gaussian前提與由它們推得的CDF對稱性。

不以有限quadrature證Gaussian積分或moments。





## 已知條件與符號


- work


- G1 — φ(x)=(2π)^(-1/2)exp(-x²/2)，Z具有此density，Φ(t)=P(Z≤t)。
- G2 — 明列named theorem facts：Gaussian積分為sqrt(2π)，因此density歸一；E[Z]=0，E[Z²]=1。這些是前提，不在本例證明。


- φ — 標準常態density
- Φ — 標準常態CDF
- Z — 實值隨機變數





## 規則與來源

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


- mko_definition · cited — 本節點把 Gaussian integral normalization、E[Z]=0 與 Var(Z)=1 明列為 named theorem facts，不以有限 quadrature 偽造完整推導。題庫可精確處理 density symbolic form、evenness、phi(x)/phi(0)=exp(-x^2/2)，以及由 declared normalization 與 symmetry 推出 Phi(0)=1/2 與 Phi(-x)=1-Phi(x)。本節不計算一般非零 x 的 elementary exact CDF 數值；有限數值積分不證 normalization 或 moments，continuous CDF 也不自動有 density 或是 normal law。 · mko-standard-normal-distribution
- work · prerequisite — Gaussian積分與moments為明示named theorem前提；另假設積分線性、變數代換、density law無原子及variance二次矩identity。





## 逐步主鏈

S01 · implies操作前

\varphi(x)=\frac{e^{-x^2/2}}{\sqrt{2\pi}}

操作後

\varphi(x)>0\quad(x\in\mathbb R)

條件：無

規則：work · 依賴：G1, G2, work

葉節點依據：work

exp正且常數分母正，density非負資格成立。



S02 · implies操作前

\int_{\mathbb R}e^{-x^2/2}\,dx=\sqrt{2\pi}\quad\text{(assumed)}

操作後

\int_{\mathbb R}\varphi(x)\,dx=1

條件：無

規則：work · 依賴：G1, G2, S01, work

葉節點依據：work

只用已宣告Gaussian積分前提乘上常數。



S03 · implies操作前

(-x)^2=x^2

操作後

\varphi(-x)=\varphi(x)

條件：無

規則：work · 依賴：G1, G2, S02, work

葉節點依據：work

平方的偶性逐點給density偶性。



S04 · implies操作前

\varphi(0)=1/\sqrt{2\pi}

操作後

\varphi(x)/\varphi(0)=e^{-x^2/2}

條件：無

規則：work · 依賴：G1, G2, S03, work

葉節點依據：work

除去共同正normalization常數得到精確比值。



S05 · implies操作前

\Phi(-t)=\int_{-\infty}^{-t}\varphi(u)\,du

操作後

\Phi(-t)=\int_t^\infty\varphi(v)\,dv=1-\Phi(t)

條件：無

規則：work · 依賴：G1, G2, S04, work

葉節點依據：work

代u=-v並用偶性、歸一；density law無singleton mass。



S06 · implies操作前

t=0,\quad\Phi(0)=1-\Phi(0)

操作後

\Phi(0)=1/2

條件：無

規則：work · 依賴：G1, G2, S05, work

葉節點依據：work

對稱式在零點化為兩倍CDF等於一。



S07 · implies操作前

E[Z]=0,\quad E[Z^2]=1\quad\text{(assumed)}

操作後

\operatorname{Var}(Z)=E[Z^2]-E[Z]^2=1

條件：無

規則：work · 依賴：G1, G2, S06, work

葉節點依據：work

用已宣告moments前提代variance identity。



S08 · implies操作前

t=1

操作後

\Phi(-1)=1-\Phi(1),\quad\varphi(1)/\varphi(0)=e^{-1/2}

條件：無

規則：work · 依賴：G1, G2, S07, work

葉節點依據：work

給一個非零點的精確符號關係，不捏造elementary CDF數值。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, G2, S07, work — Φ(1)未被本推導求成有理數，有限integration也不證前提。
- S07 · premise_audit · G1, G2, S06, work — 不把moment前提重新標成此例完成的積分證明。
- S06 · premise_audit · G1, G2, S05, work — 此exact值來自對稱與歸一，非approximation。
- S05 · premise_audit · G1, G2, S04, work — 補事件的端點差因無原子為零。
- S04 · premise_audit · G1, G2, S03, work — 這是density比值，不是CDF比值。
- S03 · premise_audit · G1, G2, S02, work — 對稱中心是0，沒有引入未知μ。
- S02 · premise_audit · G1, G2, S01, work — 這不是從幾個數值積分點回推整個積分。
- S01 · premise_audit · G1, G2, work — 非負性本身不證積分等於一。





## 錯誤控制與反例

前提標記歸一與moments保持named facts，不宣稱本例已證。

事件與門檻Φ(t)=P({ω:Z(ω)≤t})，t是標量門檻。


- 取幾個quadrature值就證歸一。 → reject — 有限數值不是整實軸積分證明。
- Φ(1)=φ(1)。 → reject — φ正故Φ(1)>Φ(0)=1/2；而φ(1)<φ(0)=1/sqrt(2π)<1/2（π>2），故不等。
- 任意連續CDF都是standard normal。 → reject — 均勻分布的連續CDF即不同。





## 結論與限制

在明示Gaussian前提下，Φ(-t)=1-Φ(t)、Φ(0)=1/2、Var(Z)=1。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: ce6e79a0422b1524888abb53a308a69a70552c942a0768637ab742837af70ae2
- original source SHA-256: 9be2b5a4eeeb9649020eca8625ccd6a76eef2d3e32963e884d8eadc5a4490a58
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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