# 自然數冪與主平方根：由遞迴算冪，並證明 √(a²)=|a|

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

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

derivation-mko-power-root-01 · production-20261019-adopted-96



## 目標與範圍

只用遞迴定義 a^0=1、a^(n+1)=a^n·a 算出 (−2)^n（n=0,1,2,3,4）與 0^0、0^3；證明非負平方根的唯一性，並證明對每個實數 a，√(a²)=|a|；再求 √49、√((−5)²)、方程 y²=9 的實數解集，並說明 √(−4) 在實數中沒有定義。

在 MKO 的範圍內工作：實數底數、自然數指數（含 0），主平方根只對 r≥0 的實數定義。不處理負指數、非整數指數或複數分支；0^0=1 只作為本代數語境的慣例，不推出任何極限規則。對一般 r≥0 的平方根存在性（例如 √2）不在本稿證明，本稿只需 r=a² 的情形；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- distributive
- neg_mul
- zero_product
- order_basics
- square_nonneg
- abs_rules
- numeric_evaluation


- G1 — a∈ℝ，n∈ℕ（ℕ 含 0）；冪由 a^0=1（本代數語境也包括 0^0=1）與 a^(n+1)=a^n·a 遞迴定義（MKO 陳述與假設 a1）。
- G2 — 對 r≥0，主平方根 √r 是滿足 y≥0 且 y²=r 的實數 y；MKO 斷言這樣的 y 唯一。r<0 時本語境不定義 √r（MKO 假設 a2）。
- G3 — 題目資料：底數 −2 與 0；根號輸入 49、(−5)²、9、−4。


- a^n — 實數 a 的 n 次冪（n∈ℕ）
- \sqrt{r} — r≥0 的主平方根：唯一滿足 y≥0、y²=r 的實數
- |a| — 絕對值：a≥0 時為 a，a<0 時為 −a
- y_1,\ y_2 — 唯一性證明中的兩個非負候選根





## 規則與來源


- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
- zero_product · prerequisite — 零乘積性質：在 ℤ、ℚ、ℝ、ℂ（或任何整域）中，uv=0 ⇔ u=0 或 v=0。
- order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
- square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。
- abs_rules · prerequisite — 絕對值（實數）：|u|=u（u≥0）、|u|=−u（u<0）；|u|≥0；|uv|=|u||v|；三角不等式 |u+v|≤|u|+|v|；|u|<r ⇔ −r<u<r。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- sqrt_def · prerequisite — 主平方根：對 a≥0，√a 是唯一滿足 b≥0 且 b²=a 的實數 b。負數在實數中沒有平方根。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- mko_power_root · cited — 對實數 a 與自然數 n，採空乘積慣例 a^0=1（本代數語境也包括 0^0=1），並由 a^(n+1)=a^n·a 定義冪。對 r≥0，主平方根 √r 是唯一滿足 y≥0 且 y²=r 的實數 y。 · mko-power-root
- L_root_unique · lemma — 若實數 y_1、y_2 都 ≥0 且 y_1²=y_2²，則 y_1=y_2。
- L_abs_sq · lemma — 對每個實數 a，|a|≥0 且 |a|²=a²。





## 逐步主鏈

S01 · definition操作前

a^n,\quad a\in\mathbb{R},\ n\in\mathbb{N}

操作後

a^0=1,\qquad a^{n+1}=a^n\cdot a

條件：n\in\mathbb{N}

規則：mko_power_root · 依賴：G1

葉節點依據：mko_power_root + def_intro

依 MKO，冪以遞迴定義：指數為 0 時是空乘積 1（包括 0^0=1，這是本代數語境的慣例），指數加一時再乘一次底數。所以 n>0 時 a^n 是 n 個 a 的乘積，而不是 a·n。指數限於自然數；負指數、非整數指數與複數分支不在範圍內。



S02 · equivalent操作前

(-2)^1

操作後

(-2)^0\cdot(-2)=1\cdot(-2)=-2

條件：無

規則：def_unfold · 依賴：S01, G3

葉節點依據：def_unfold + mko_power_root + mul_one

用遞迴的第二條（n=0）：(−2)^1=(−2)^0·(−2)；再用第一條 (−2)^0=1，以及 1·u=u，得 −2。



S03 · equivalent操作前

(-2)^2

操作後

(-2)^1\cdot(-2)=(-2)(-2)=4

條件：無

規則：neg_mul · 依賴：S01, S02

葉節點依據：def_unfold + neg_mul + numeric_evaluation

遞迴（n=1）：(−2)^2=(−2)^1·(−2)=(−2)(−2)。依 (−u)(−v)=uv，(−2)(−2)=2·2=4。



S04 · equivalent操作前

(-2)^3

操作後

(-2)^2\cdot(-2)=4\cdot(-2)=-8

條件：無

規則：neg_mul · 依賴：S01, S03

葉節點依據：def_unfold + neg_mul + mul_comm + numeric_evaluation

遞迴（n=2）：(−2)^3=(−2)^2·(−2)=4·(−2)。依 u(−v)=−(uv)，4·(−2)=−8。注意這不是 (−2)·3=−6：冪是重複乘底數，不是乘以指數。



S05 · equivalent操作前

(-2)^4

操作後

(-2)^3\cdot(-2)=(-8)(-2)=16

條件：無

規則：neg_mul · 依賴：S01, S04

葉節點依據：def_unfold + neg_mul + numeric_evaluation

遞迴（n=3）：(−2)^4=(−8)(−2)=16。於是 (−2)^n 在 n=0,1,2,3,4 依次為 1、−2、4、−8、16：這幾個奇次冪為負、偶次冪為正，與 MKO para0 的描述一致。這只是五個指數的計算，不當作對所有 n 的證明。



S06 · equivalent操作前

0^0,\ 0^1,\ 0^2,\ 0^3

操作後

0^0=1,\ 0^1=1\cdot 0=0,\ 0^2=0\cdot 0=0,\ 0^3=0\cdot 0=0

條件：無

規則：mul_zero · 依賴：S01, G3

葉節點依據：def_unfold + mko_power_root + mul_zero + mul_one

0^0=1 直接來自定義的第一條（MKO 明示的代數慣例）。之後 0^1=0^0·0=1·0=0，0^2=0^1·0=0，0^3=0^2·0=0（u·0=0）。所以零底數在正冪下仍為零，而 n=0 的值 1 是慣例給的，不是由任何極限決定。



S07 · implies操作前

y_1\geq 0,\ y_2\geq 0,\ y_1^2=y_2^2

操作後

y_1=y_2

條件：y_1\geq 0; y_2\geq 0

規則：L_root_unique · 依賴：G2

葉節點依據：L_root_unique + order_basics

MKO 說主平方根是「唯一」滿足 y≥0、y²=r 的實數；這個唯一性可以證明。依引理 L_root_unique，兩個非負數平方相等時本身相等。證明在 S07.1 至 S07.3。



S08 · implies操作前

|a|\quad(a\in\mathbb{R})

操作後

|a|\geq 0\ \land\ |a|^2=a^2

條件：無

規則：L_abs_sq · 依賴：abs_rules

葉節點依據：L_abs_sq + abs_rules + case_analysis

依引理 L_abs_sq，|a| 是非負數，且平方等於 a²。依三一律 a≥0 或 a<0 兩種情形涵蓋全部實數，證明在 S08.1、S08.2。



S09 · implies操作前

\sqrt{a^2}\quad(a\in\mathbb{R})

操作後

\sqrt{a^2}=|a|

條件：a^2\geq 0

規則：L_root_unique · 依賴：G2, S07, S08, square_nonneg

葉節點依據：L_root_unique + L_abs_sq + square_nonneg + sqrt_def

先確認 √(a²) 有意義：依 square_nonneg，a²≥0，所以 G2 的定義適用於 r=a²。y=|a| 滿足 y≥0 與 y²=a²（S08），所以至少有一個這樣的 y；依 S07，這樣的非負 y 至多一個。因此 √(a²) 存在且等於 |a|。注意結論是 |a| 而不是 a。



S10 · implies操作前

\sqrt{49}

操作後

\sqrt{7^2}=|7|=7

條件：7\geq 0

規則：forall_elim · 依賴：S09, G3

葉節點依據：forall_elim + abs_rules + numeric_evaluation

49=7²，代入 S09（a=7）得 √49=|7|=7。−7 的平方也是 49，但 −7<0，不符合 y≥0，所以不是主平方根。



S11 · implies操作前

\sqrt{(-5)^2}

操作後

|-5|=5

條件：-5<0

規則：forall_elim · 依賴：S09, G3

葉節點依據：forall_elim + abs_rules + numeric_evaluation

代入 S09（a=−5）：√((−5)²)=|−5|=5。直接核對：(−5)²=25，5≥0 且 5²=25。若寫成 √((−5)²)=−5，右邊是負數，違反主平方根的 y≥0。



S12 · equivalent操作前

y^2=9

操作後

(y-3)(y+3)=0

條件：無

規則：distributive · 依賴：G3, distributive

葉節點依據：distributive + eq_congruence + add_inverse

兩邊同減 9 得 y²−9=0；展開 (y−3)(y+3)=y²+3y−3y−9=y²−9，所以 y²=9 等價於 (y−3)(y+3)=0。



S13 · equivalent操作前

(y-3)(y+3)=0

操作後

y=3\ \lor\ y=-3,\quad\text{solution set}\ \{-3,3\}

條件：無

規則：zero_product · 依賴：S12, zero_product

葉節點依據：zero_product + eq_congruence

依零乘積性質，y−3=0 或 y+3=0，即 y=3 或 y=−3。所以方程 y²=9 的實數解集是 {−3,3}，有兩個元素。



S14 · implies操作前

\{-3,3\}

操作後

\sqrt{9}=3,\quad \{-3,3\}=\{-\sqrt{9},\sqrt{9}\}

條件：無

規則：L_root_unique · 依賴：S09, S13

葉節點依據：L_root_unique + forall_elim + order_basics

解集中只有 3 滿足 y≥0，依 S09（a=3），√9=|3|=3。所以方程有兩個解 ±√9，但符號 √9 只表示一個數 3。「方程的解」與「主平方根」是兩件事。



S15 · implies操作前

y^2=-4,\ y\in\mathbb{R}

操作後

\text{no real solution};\ \sqrt{-4}\ \text{undefined here}

條件：-4<0

規則：square_nonneg · 依賴：G2, G3, square_nonneg

葉節點依據：square_nonneg + order_basics + sqrt_def

對每個實數 y，y²≥0>−4，所以 y²≠−4，方程 y²=−4 沒有實數解。G2 也只對 r≥0 定義 √r，所以 √(−4) 在本語境沒有定義。寫成 −2 是錯的：(−2)²=4≠−4，而且 −2<0。







## 局部子步與引理

S07.1 · equivalent操作前

y_1^2=y_2^2

操作後

(y_1-y_2)(y_1+y_2)=0

條件：無

規則：distributive · 依賴：distributive

葉節點依據：distributive + mul_comm + add_inverse + eq_congruence

展開 (y_1−y_2)(y_1+y_2)=y_1²+y_1y_2−y_2y_1−y_2²=y_1²−y_2²（分配律、乘法交換律、加法反元素）。所以 y_1²=y_2² 等價於 y_1²−y_2²=0，即 (y_1−y_2)(y_1+y_2)=0。



S07.2 · equivalent操作前

(y_1-y_2)(y_1+y_2)=0

操作後

y_1-y_2=0\ \lor\ y_1+y_2=0

條件：無

規則：zero_product · 依賴：S07.1, zero_product

葉節點依據：zero_product

依零乘積性質，實數乘積為 0 當且僅當至少一個因子為 0。



S07.3 · case_split操作前

y_1-y_2=0\ \lor\ y_1+y_2=0

操作後

y_1=y_2

條件：y_1\geq 0; y_2\geq 0

規則：case_analysis · 依賴：S07.2, order_basics

葉節點依據：case_analysis + order_basics + add_inverse

情形一：y_1−y_2=0，兩邊加 y_2 得 y_1=y_2。情形二：y_1+y_2=0，則 y_1=−y_2；因 y_2≥0，−y_2≤0，所以 y_1≤0，又 y_1≥0，故 y_1=0，進而 y_2=−y_1=0，也有 y_1=y_2。兩種情形都得 y_1=y_2。S07.1 至 S07.3 合起來證得引理 L_root_unique。



S08.1 · implies操作前

a\geq 0

操作後

|a|=a\geq 0,\quad |a|^2=a^2

條件：a\geq 0

規則：abs_rules · 依賴：abs_rules

葉節點依據：abs_rules + eq_replace

a≥0 時 |a|=a，所以 |a|≥0，且 |a|²=a²（等值代換）。



S08.2 · implies操作前

a<0

操作後

|a|=-a>0,\quad |a|^2=(-a)(-a)=a^2

條件：a<0

規則：neg_mul · 依賴：abs_rules, neg_mul, order_basics

葉節點依據：abs_rules + neg_mul + order_basics

a<0 時 |a|=−a。由 a<0 兩邊加 −a 得 0<−a，所以 |a|>0。又 (−a)(−a)=a·a=a²（neg_mul）。S08.1 與 S08.2 合起來證得引理 L_abs_sq。







## 逐步反向審查


- S15 · premise_audit · square_nonneg, G2, order_basics — 結論是「在實數中無定義」；本稿不討論複數分支，也不採用把負輸入補成 0 的程式語義（MKO para2）。
- S14 · premise_audit · S09, S13, L_root_unique — 需要非負條件從兩個解中選出一個；把 √9 寫成 ±3 違反唯一性。
- S13 · inverse_equivalence · zero_product, eq_congruence — 零乘積性質雙向成立；代回 3²=9、(−3)²=9（N19、N20）。
- S12 · inverse_equivalence · distributive, eq_congruence, add_inverse — 同減 9 與同加 9 互為反運算，展開式是恆等式（N18），雙向成立。
- S11 · premise_audit · S09, forall_elim, abs_rules — 這是 MKO 指出的誤解所在：√(a²) 不能無條件寫成 a；a<0 時兩者不同（N15 至 N17）。
- S10 · premise_audit · S09, forall_elim, numeric_evaluation — 需要 49 寫成某數的平方（N13）；−7 被非負條件排除（N14 顯示它的平方也是 49）。
- S09 · sufficient_goal_reduction · S07, S08, square_nonneg, G2 — 目標 G：√(a²)=|a|。足夠條件 H：a²≥0、|a| 是一個非負且平方為 a² 的數、而且這樣的數唯一；H⇒G 由主平方根的定義。H 由 square_nonneg、S08 與 S07 正向證成，沒有把 G 當作前提。
- S08.2 · premise_audit · abs_rules, neg_mul, order_basics — 需要 a<0 才能用 |a|=−a；恆等式 (−a)(−a)=a² 對所有 a 成立（N11）。
- S08.1 · premise_audit · abs_rules, eq_replace — 只在 a≥0 的情形使用 |a|=a；另一情形見 S08.2。
- S08 · premise_audit · L_abs_sq, abs_rules, case_analysis — 兩個情形必須涵蓋全部實數；三一律保證沒有遺漏。
- S07.3 · premise_audit · S07.2, case_analysis, order_basics — 情形二正是非負條件發揮作用之處；若允許 y_2<0，例如 y_1=3、y_2=−3，情形二成立但 y_1≠y_2。
- S07.2 · inverse_equivalence · zero_product — 零乘積性質本身是雙向的（ℝ 是整域）。
- S07.1 · inverse_equivalence · distributive, mul_comm, add_inverse, eq_congruence — 兩邊同減 y_2² 與同加 y_2² 互為反運算，展開式是恆等式（N10），所以雙向成立。
- S07 · premise_audit · L_root_unique, G2 — 唯一性需要非負條件；沒有它，3 與 −3 平方相等卻不相等。反向（相等推出平方相等）顯然但未使用。
- S06 · inverse_equivalence · def_unfold, mul_zero — 每個等號都是定義或 u·0=0 的代換，雙向成立；0^0=1 不能用來推出極限結論。
- S05 · inverse_equivalence · def_unfold, neg_mul — 等值代換，雙向成立；正負交替的一般命題本稿不宣稱已證。
- S04 · inverse_equivalence · def_unfold, neg_mul, mul_comm — 等值代換，雙向成立；N3、N4 重算，N5 確認 −8≠−6。
- S03 · inverse_equivalence · def_unfold, neg_mul — 等值代換，雙向成立；N2 可重算。
- S02 · inverse_equivalence · def_unfold, mul_one — 每個等號都是把式子換成相等的式子，倒著讀就回到 (−2)^1；兩式表示同一個數。
- S01 · premise_audit · G1, mko_power_root — 此步只寫出定義；後面每個冪的值都只由這兩條遞迴算出，不另外假設指數律。





## 錯誤控制與反例

主平方根不是 ± 值MKO 指出的第一個誤解是把主平方根寫成 ± 值。方程 y²=9 有兩個解 ±3（S13），但 √9 由 y≥0 與唯一性（S07）確定為 3 一個數（S14）。需要兩個解時要寫 ±√9，而不是說 √9 等於 ±3。

√(a²)=|a|，不是 aMKO 指出的第二個誤解是把 √(a²) 當成 a。a=−5 時 √((−5)²)=√25=5=|−5|，而 −5 不滿足 y≥0（S11）。只有 a≥0 時才可寫 √(a²)=a。

0^0=1 是代數慣例；a^n 不是 a·nMKO 指出的第三個誤解是把 0^0=1 套到極限。數列 0^n 的值依次為 1、0、0、0，以此類推，n≥1 時都是 0，所以極限是 0，不是 1；n=0 的值只是慣例（S06）。另外 (−2)^3=−8，不是 (−2)·3=−6（S04）。


- √9=±3 → reject — 主平方根要求 y≥0 且唯一，√9=3；±3 是方程 y²=9 的兩個解。
- √((−5)²)=−5 → reject — √((−5)²)=√25=5=|−5|；−5<0 不符合主平方根的條件。
- (−2)³=(−2)·3=−6 → reject — 冪是重複乘底數：(−2)³=4·(−2)=−8≠−6。
- 因為 0^0=1，數列 0^n 的極限是 1 → reject — n≥1 時 0^n=0，數列極限是 0；0^0=1 是代數慣例，不決定極限。
- √(−4)=−2 → reject — (−2)²=4≠−4，且 −2<0；沒有實數平方等於 −4，√(−4) 在實數中無定義。





## 結論與限制

由遞迴：(−2)^0、(−2)^1、(−2)^2、(−2)^3、(−2)^4 依次為 1、−2、4、−8、16；0^0=1（慣例）、0^3=0。非負平方根唯一；對每個實數 a，√(a²)=|a|。因此 √49=7，√((−5)²)=5（不是 −5），y²=9 的解集是 {−3,3} 而 √9=3，√(−4) 在實數中沒有定義。


- 本稿證明唯一性，並對 r=a² 給出存在性（取 y=|a|）。對一般 r≥0（例如 r=2）的存在性需要實數完備性，本稿沒有證明，也沒有用到。
- N12 只是 a 從 −20 到 20 的有限點核對；|a|²=a² 的一般證明是 S08。
- Mathlib Real.sqrt 對負輸入回傳 0 的語義與本稿「無定義」不同，橋接需要 r≥0 的前提（MKO para2），不在本稿範圍。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 500af794d5ac8f50bed01f893eca7a76224302cea15cd5ef78efee08f8a81236
- original source SHA-256: 500af794d5ac8f50bed01f893eca7a76224302cea15cd5ef78efee08f8a81236
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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