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

目標與範圍

只用遞迴定義 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²。

逐步主鏈

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

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

(-2)^1

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

(-2)^2

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

(-2)^3

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

(-2)^4

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

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

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

y_1=y_2

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

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

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

\sqrt{a^2}=|a|

\sqrt{49}

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

\sqrt{(-5)^2}

|-5|=5

y^2=9

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

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

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

\{-3,3\}

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

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

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

局部子步與引理

y_1^2=y_2^2

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

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

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

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

y_1=y_2

a\geq 0

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

a<0

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

逐步反向審查

• 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|，不是 a

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

0^0=1 是代數慣例；a^n 不是 a·n

MKO 指出的第三個誤解是把 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、反控制與修訂記錄）