# 自然數冪與主平方根

本輪限定實數底數的自然數冪，以及非負實數的主平方根，分開冪運算、根值與解集。

mko-power-root · definition · v0.10.0



## 數學敘述

對實數 a 與自然數 n，採空乘積慣例 a^0=1（本代數語境也包括 0^0=1），並由 a^(n+1)=a^n·a 定義冪。對 r≥0，主平方根 √r 是唯一滿足 y≥0 且 y²=r 的實數 y。





## 代表公式（精確 TeX）

a^{n}





## 成立條件


- n∈N={0,1,2,…}；本輪不處理負指數、非整數指數或複數分支。
- 主平方根只在 r≥0 的實數論域定義；0^0=1 是此處的代數慣例，不是極限運算規則。





## 符號作用域


- a — 實數底數
- n — 自然數指數





## 直觀、定義與常見誤解

a^n 不是 a·n。n=0 時按空乘積得到 1；n>0 時是 n 個 a 的乘積。負底數在正奇數冪下為負、正偶數冪下為正；零底數在正冪下仍為零。

√0=0；正 r 的主平方根取非負分支。方程 y²=r 的實數解集在 r>0 時有兩根 ±√r，在 r=0 時只有零，在 r<0 時為空。因此 √(a²)=|a|，不可無條件寫成 a。

題庫採整數底數、非負整數指數和完全平方數的精確切片，另檢查負根號輸入的論域。未來 Mathlib Real.sqrt 的負輸入補零語義必須經 r≥0 的橋接前提；不能把補零當成此處的課本根值。

把主平方根寫成 ± 值、把 √(a²) 當成 a，或把 0^0 的局部代數慣例套到極限。





## 已採用的推導導讀

[自然數冪與主平方根：由遞迴算冪，並證明 √(a²)=|a|](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-power-root-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [四則運算](https://ocme.evemisslab.com/zh-Hant/mko/mko-arithmetic-operations/) — 自然數冪以乘法遞迴定義。
- [實數](https://ocme.evemisslab.com/zh-Hant/mko/mko-real-number/) — 主平方根以非負實數論域和大小關係選定分支。





## 驗證界線

本輪案例可精確重算；一般平方根存在唯一性及冪法則仍未附形式 Evidence。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。





## 下一個義務

綁定自然数冪的空乘積遞迴、主根非負前提、sqrt_sq_eq_abs 及 Real.sqrt 的補零邊界。





## 同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。

[原始 MKO JSON](https://ocme.evemisslab.com/data/mko/power-root.json) · [純文字 Markdown](https://ocme.evemisslab.com/zh-Hant/mko/mko-power-root/index.md)