自然數冪與主平方根

數學敘述

對實數 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 的局部代數慣例套到極限。

已採用的推導導讀

原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。

前置知識

• 四則運算 — 自然數冪以乘法遞迴定義。
• 實數 — 主平方根以非負實數論域和大小關係選定分支。

驗證界線

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

not_formalized

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

下一個義務

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

同源結構化資料

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