絕對值：由分段定義證明非負性、零點與 |a−b|=|b−a|

目標與範圍

只用分段定義（x≥0 時 |x|=x，x<0 時 |x|=−x）與實數的序和加法，證明對所有實數 x、a、b：(1) |x|≥0；(2) |x|=0 ⇔ x=0；(3) |−x|=|x|；(4) |a−b|=|b−a|。並計算 |−3|、|2−7|、|7−2|，說明「|x|=x 對所有 x 成立」是錯的。

在 MKO 的範圍內：實數及其標準線性序與加法反元素（假設 a1），以分段定義的函數 A(x)=|x|。所有性質都由分段定義推出，不使用現成的絕對值規則；不處理三角不等式、不等式解法、複數模或範數（MKO 指出這些是後續內容）；不改動 canonical MKO 或英文 edition。

已知條件與符號

• order_basics
• add_inverse
• add_assoc
• add_comm
• add_zero
• numeric_evaluation

• G1 — x、a、b 是實數；ℝ 具有標準線性序與加法反元素（MKO 假設 a1）。
• G2 — 定義：若 x≥0，則 |x|=x；若 x<0，則 |x|=−x。

• |x| — x 的絕對值 A(x)
• -x — x 的加法反元素
• a,\ b — 數線上的兩個實數
• |a-b| — a 與 b 的距離

規則與來源

• 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。
• add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
• add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
• add_comm · prerequisite — 加法交換律：u+v=v+u。
• add_zero · prerequisite — 加法單位元：u+0=u。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
• iff_intro · prerequisite — 雙條件：P⇒Q 與 Q⇒P 都成立時，P⇔Q 成立；反之亦然。
• forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_abs_def · cited — 函數 A:ℝ→ℝ 定義為：若 x≥0，則 A(x)=x；若 x<0，則 A(x)=−x。慣用記號為 |x|，且 |x|≥0。 · mko-absolute-value
• L_sign · lemma — 對實數 x：若 x<0 則 0<−x；若 0<x 則 −x<0。
• L_inv_unique · lemma — 對實數 u、v：若 u+v=0，則 v=−u。特別地 −(−x)=x，且 −0=0。

逐步主鏈

|x|

|x|=x\ \ (x\geq 0),\qquad |x|=-x\ \ (x<0)

x\geq 0

|x|=x\geq 0

x<0

|x|=-x>0

x\geq 0\ \lor\ x<0

\forall x\in\mathbb{R}:\ |x|\geq 0

x\neq 0

|x|>0,\ \text{hence}\ |x|\neq 0;\ \text{so}\ |x|=0\Rightarrow x=0

x=0

|0|=0;\ \ \text{hence}\ |x|=0\Leftrightarrow x=0

x>0

|-x|=-(-x)=x=|x|

x<0

|-x|=-x=|x|

x>0\ \lor\ x<0\ \lor\ x=0

\forall x\in\mathbb{R}:\ |-x|=|x|

(a-b)+(b-a)

(a-b)+(b-a)=0,\ \text{hence}\ b-a=-(a-b)

|b-a|

|b-a|=|-(a-b)|=|a-b|

|-3|

|-3|=-(-3)=3

|2-7|,\ |7-2|

|2-7|=|-5|=5,\ \ |7-2|=|5|=5

\forall x\in\mathbb{R}:\ |x|=x

\text{false, since}\ |-3|=3\neq -3

S04,\ S06,\ S09,\ S11

|x|\geq 0,\ \ |x|=0\Leftrightarrow x=0,\ \ |-x|=|x|,\ \ |a-b|=|b-a|

局部子步與引理

x<0

x+(-x)<0+(-x)

x+(-x)<0+(-x)

0<-x

u+v=0

v=-u

逐步反向審查

• S15 · sufficient_goal_reduction · S04, S06, S09, S11, and_intro_elim — 目標 G：(1) 到 (4) 同時成立。足夠條件 H：S04、S06、S09、S11 各自成立；H⇒G 由合取引入。H 由定義正向證成，沒有把 G 當作前提；S12 到 S14 是例子與反例。
• S14 · premise_audit · S12, quantifier_negation, order_basics — 推翻全稱命題只需要一個反例；這不宣稱 |x|=x 對其他 x 是否成立。
• S13 · premise_audit · S01, S11, numeric_evaluation — 必須先求出 2−7 的值再判定分支；不能看到式子中的減號就直接刪掉。
• S12 · premise_audit · S01, L_inv_unique, numeric_evaluation — 先判定 −3 的正負才選分支；N1 重算 −(−3)=3。
• S11 · premise_audit · S09, S10, forall_elim, eq_replace — S09 對所有實數成立，所以可代入 x=a−b；N6 只是 a、b 在 −6 到 6 的有限核對，不是證明。
• S10 · premise_audit · L_inv_unique, add_assoc, add_comm, add_inverse — 重排只用加法的結合律與交換律；N5 以多項式恆等式核對 (a−b)+(b−a)=0。
• S09 · premise_audit · S07, S08, case_analysis, order_basics — 三種情況必須都處理；只看 x>0 不能推出一般結論。
• S08 · premise_audit · S01, L_sign — 兩次展開定義所用的分支不同（−x 用第一分支、x 用第二分支），各自由相應數值的正負判定。
• S07.1 · premise_audit · add_zero, add_inverse, add_assoc, add_comm, eq_replace — 每一步都是對所有實數成立的恆等式或假設 u+v=0 的代換；結論只說反元素唯一。
• S07 · premise_audit · L_sign, L_inv_unique, S01 — 分支是依 −x 這個數的正負選的，不是依 x 的正負；這正是容易弄錯的地方。
• S06 · premise_audit · S05, iff_intro, def_unfold — 雙條件需要兩個方向都已證：⇐ 在此步，⇒ 在 S05。
• S05 · premise_audit · S02, S03, contrapositive, case_analysis — 逆否命題與原命題等價；此步只得到一個方向，另一方向在 S06。
• S04 · premise_audit · S02, S03, case_analysis, forall_intro — 分情況論證要求情況涵蓋全部可能；x≥0 與 x<0 由三一律涵蓋所有實數。
• S03.2 · inverse_equivalence · add_inverse, add_zero, add_comm, eq_replace — 只把式子換成相等的式子，不等式的真假不變，雙向成立。
• S03.1 · premise_audit · order_basics — 兩邊加同一個數保持嚴格不等號的方向，對任何實數 w 都成立，沒有附加條件。
• S03 · premise_audit · S01, L_sign — 需要本情況的假設 x<0 與引理；引理在 S03.1、S03.2 證明。
• S02 · premise_audit · S01, def_unfold — 只在 x≥0 的情況下使用第一分支；不宣稱 x<0 時 |x|=x。
• S01 · premise_audit · G2, mko_abs_def, order_basics — 此步只寫出定義；分支互斥且涵蓋全部實數，靠的是三一律。

錯誤控制與反例

|x| 不一律等於 x

MKO 指出的第一個誤解是把 |x| 一律寫成 x。|x|=x 只是 x≥0 時的分支；x<0 時 |x|=−x。反例：x=−3 時 |x|=3，而 x=−3。使用絕對值前，先判定裡面那個數的正負。

絕對值不是刪除負號的文字規則

MKO 指出的第二個誤解是把絕對值當成刪除負號。把 |2−7| 的減號刪掉得 2+7=9，但 2−7=−5，|−5|=5。又如 x=−2 時 |−x|=|2|=2，而刪除負號會得到 x=−2。定義看的是數值的正負，不是符號的外觀。

|x| 不會是負數，而 −x 不一定是負數

MKO 指出的第三個誤解是認為 |x| 可以是負數。第二分支寫成 |x|=−x，看起來帶負號，但它只在 x<0 時使用，而依 L_sign，此時 −x>0；例如 x=−3 時 −x=3。所以 S04 證明 |x|≥0 對所有實數成立。

• 對所有實數 x，|x|=x → reject — x=−3 時 |x|=3≠−3。
• |2−7|=2+7=9 → reject — 2−7=−5，|−5|=5。
• 對所有實數 x，|−x|=x → reject — x=−2 時 |−x|=|2|=2≠−2；正確的是 |−x|=|x|。
• 存在實數 x 使 |x|<0 → reject — S04 證明對所有實數 |x|≥0。
• 因為 a−b≠b−a（a≠b 時），所以 |a−b| 與 |b−a| 一般不相等 → reject — b−a=−(a−b)，而 |−x|=|x|（S11）；例如 |2−7|=|7−2|=5。

結論與限制

由分段定義可證：對所有實數 |x|≥0；|x|=0 ⇔ x=0；|−x|=|x|；|a−b|=|b−a|。例子：|−3|=3，|2−7|=|7−2|=5；|x|=x 在 x=−3 時不成立，所以不是一般規則。

• N6 與 N10 是整數點上的有限核對（分別為 a、b 從 −6 到 6，x 從 −10 到 10），只支持這些點；一般結論來自 S04 與 S11 的證明。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: ca5b2649a099d99d3fc2f80cd2245c776c98a9a136217dfab0d702504caa791f
• original source SHA-256: 34445117b994db885a5ef32034463f123a04ed40293eda3d29414fa6e7d493f6
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）