# 歐幾里得長度：由座標精確計算兩點距離

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

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

derivation-mko-euclidean-length-01 · production-20261019-adopted-96



## 目標與範圍

在以 ℝ² 表示的歐幾里得平面中，設 P=(1,−2)、Q=(4,2)、R=(2,3)。精確算出 d(P,Q)=5；算出 d(P,R)=√26，並以平方比較證明 5.09<√26<5.1，說明 5.1 只是近似值。另對一般的實數坐標證明：距離有定義且非負、d(Q,P)=d(P,Q)、d(P,P)=0，以及 d(P,Q)=0 ⇔ P=Q。

只使用 MKO 的二維座標距離公式（實數坐標、非負主平方根）。證明公式的基本性質（非負、對稱、與點相同的關係），不證明三角不等式，不處理與抽象度量或 Mathlib EuclideanSpace 的對接，也不證明 √26 是無理數；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- square_nonneg
- sqrt_def
- order_basics
- cartesian_product_def
- numeric_evaluation


- G1 — 模型：歐幾里得平面以 ℝ² 表示，點的座標為實數（MKO 假設 a1、a2）。
- G2 — 距離的定義：P=(x₁,y₁)、Q=(x₂,y₂) 時，d(P,Q)=√((x₂−x₁)²+(y₂−y₁)²)，√ 取非負主值（MKO 假設 a3）。
- G3 — P=(1,−2)、Q=(4,2)、R=(2,3)。


- d(P,Q) — P、Q 兩點的歐幾里得距離
- x_2-x_1,\ y_2-y_1 — 兩個座標差
- s — 被開方數 (x₂−x₁)²+(y₂−y₁)²
- \sqrt{s} — s≥0 的非負主平方根





## 規則與來源


- square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。
- sqrt_def · prerequisite — 主平方根：對 a≥0，√a 是唯一滿足 b≥0 且 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。
- cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
- power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- add_zero · prerequisite — 加法單位元：u+0=u。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_length_def · cited — 獨立來源追加式勘誤（使用者已採用於本地修訂；未合併或發布）：在歐幾里得平面中，若 P=(x₁,y₁)、Q=(x₂,y₂)，則兩點距離取座標差平方和的非負主平方根；P=Q 時此值為 0。原來源的「正平方根」字樣保留於父版與修訂紀錄。 · mko-euclidean-length
- L_neg_sq · lemma — 對實數 p、q：(p−q)²=(q−p)²。
- L_sum_sq_zero · lemma — 對實數 a、b：a²+b²=0 ⇔ a=0 且 b=0。
- L_sq_mono · lemma — 對實數 a≥0、b≥0：a<b ⇔ a²<b²。





## 逐步主鏈

S01 · definition操作前

d(P,Q)

操作後

\sqrt{(x_2-x_1)^2+(y_2-y_1)^2}

條件：無

規則：mko_length_def · 依賴：G1, G2, mko_length_def

葉節點依據：mko_length_def + def_unfold

依 MKO 的定義：先算兩個座標差，各自平方，相加，最後取非負主平方根。順序是「差、平方、相加、開方」，不可把座標差直接相加。這個定義把水平位移與垂直位移看成互相垂直的兩個分量。



S02 · implies操作前

s=(x_2-x_1)^2+(y_2-y_1)^2

操作後

s\ge 0,\ d(P,Q)=\sqrt{s}\ge 0

條件：x_1,y_1,x_2,y_2\in\mathbb{R}

規則：square_nonneg · 依賴：S01, square_nonneg

葉節點依據：square_nonneg + order_basics + sqrt_def

兩個平方都 ≥0（實數平方非負），兩個非負數的和也 ≥0（序與加法），所以被開方數 s≥0，√s 有定義；依主平方根的定義，√s≥0。所以對任何兩點，距離都有定義且非負（MKO 假設 a3）。



S03 · equivalent操作前

x_2-x_1,\ y_2-y_1\ \text{for}\ P,Q

操作後

4-1=3,\ 2-(-2)=4

條件：無

規則：numeric_evaluation · 依賴：G3, S01

葉節點依據：numeric_evaluation + add_inverse + neg_mul

P=(1,−2)、Q=(4,2)：x₂−x₁=4−1=3，y₂−y₁=2−(−2)=2+2=4。減去負數等於加上它的相反數。



S04 · equivalent操作前

3^2+4^2

操作後

25

條件：無

規則：numeric_evaluation · 依賴：S03

葉節點依據：numeric_evaluation + power_laws

先平方再相加：3²=9、4²=16，9+16=25。



S05 · equivalent操作前

d(P,Q)=\sqrt{25}

操作後

d(P,Q)=5

條件：25\ge 0

規則：sqrt_def · 依賴：S02, S04, sqrt_def

葉節點依據：sqrt_def + numeric_evaluation + order_basics

依主平方根的定義，√25 是唯一滿足 b≥0 且 b²=25 的實數 b。b=5 滿足 5≥0 且 5²=25，所以 √25=5。−5 也滿足 (−5)²=25，但 −5<0，不是主值；距離不能是 −5。



S06 · equivalent操作前

d(Q,P)=\sqrt{(x_1-x_2)^2+(y_1-y_2)^2}

操作後

\sqrt{(x_2-x_1)^2+(y_2-y_1)^2}=d(P,Q)

條件：無

規則：L_neg_sq · 依賴：S01, L_neg_sq

葉節點依據：L_neg_sq + eq_replace

交換 P、Q 時，每個座標差變號：x₁−x₂=−(x₂−x₁)。依引理 L_neg_sq，(x₁−x₂)²=(x₂−x₁)²，y 坐標同理，所以被開方數相同，d(Q,P)=d(P,Q)，對所有實數坐標都成立。例：d(Q,P)=√((1−4)²+(−2−2)²)=√(9+16)=5。引理在 S06.1 證明。



S07 · equivalent操作前

d(P,P)=\sqrt{(x_1-x_1)^2+(y_1-y_1)^2}

操作後

\sqrt{0}=0

條件：無

規則：sqrt_def · 依賴：S01, sqrt_def

葉節點依據：sqrt_def + mul_zero + add_zero + add_inverse

P 與自己比較時，兩個座標差都是 0，被開方數是 0²+0²=0；0≥0 且 0²=0，所以 √0=0，d(P,P)=0。



S08 · equivalent操作前

\sqrt{s}=0\ \ (s\ge 0)

操作後

s=0

條件：s\ge 0

規則：sqrt_def · 依賴：S02, S07, sqrt_def

葉節點依據：sqrt_def + eq_congruence + mul_zero

⇒：依主平方根定義 (√s)²=s，所以 s=0²=0。⇐：s=0 時 √0=0（S07）。這把「距離為 0」轉成「被開方數為 0」。



S09 · equivalent操作前

(x_2-x_1)^2+(y_2-y_1)^2=0

操作後

x_2=x_1\ \land\ y_2=y_1\ \iff\ P=Q

條件：無

規則：L_sum_sq_zero · 依賴：S08, L_sum_sq_zero

葉節點依據：L_sum_sq_zero + cartesian_product_def + add_inverse

依引理 L_sum_sq_zero（a=x₂−x₁、b=y₂−y₁）：平方和為 0 ⇔ 兩個差都是 0 ⇔ x₂=x₁ 且 y₂=y₁；依有序對相等，這就是 P=Q。結合 S08：d(P,Q)=0 ⇔ P=Q。引理在 S09.1、S09.2 證明。



S10 · equivalent操作前

d(P,R)

操作後

\sqrt{(2-1)^2+(3-(-2))^2}=\sqrt{26}

條件：無

規則：mko_length_def · 依賴：G3, S01

葉節點依據：mko_length_def + numeric_evaluation

R=(2,3)：x 差 2−1=1，y 差 3−(−2)=5；1²+5²=1+25=26，所以 d(P,R)=√26。這裡保留精確形式 √26，不用小數取代。



S11 · equivalent操作前

5^2=25<26<36=6^2

操作後

5<\sqrt{26}<6

條件：5\ge 0,\ \sqrt{26}\ge 0,\ 6\ge 0

規則：L_sq_mono · 依賴：S10, L_sq_mono, sqrt_def

葉節點依據：L_sq_mono + sqrt_def + numeric_evaluation

5、√26、6 都 ≥0，且 (√26)²=26（主平方根定義）。依引理 L_sq_mono：25<26 ⇔ 5<√26；26<36 ⇔ √26<6。所以 √26 在 5 與 6 之間。引理在 S11.1、S11.2 證明。



S12 · implies操作前

5.09^2=25.9081<26<26.01=5.1^2

操作後

5.09<\sqrt{26}<5.1,\ \sqrt{26}\neq 5.1

條件：5.09\ge 0,\ 5.1\ge 0

規則：L_sq_mono · 依賴：S10, L_sq_mono, sqrt_def

葉節點依據：L_sq_mono + sqrt_def + numeric_evaluation + contradiction

精確計算 5.09²=25.9081<26，5.1²=26.01>26，依 L_sq_mono 得 5.09<√26<5.1。特別是 5.1²=26.01≠26，所以 √26≠5.1：程式印出的 5.1 或 5.0990195 這類有限小數只是近似值（5.0990195²<26，N14），√26 才是精確距離。



S13 · implies操作前

\text{S02, S05, S06, S07, S09, S12}

操作後

d(P,Q)=5,\ d(P,R)=\sqrt{26}\in(5.09,\,5.1);\ d\ge 0,\ d(Q,P)=d(P,Q),\ d(P,Q)=0\iff P=Q

條件：無

規則：and_intro_elim · 依賴：S02, S05, S06, S07, S09, S12

葉節點依據：and_intro_elim

把各步合起來：例子中 d(P,Q)=5，d(P,R)=√26 且介於 5.09 與 5.1 之間；對所有實數坐標，距離有定義且非負、對稱，而且距離為 0 恰好在兩點相同時發生。







## 局部子步與引理

S06.1 · equivalent操作前

(p-q)^2

操作後

(q-p)^2

條件：無

規則：neg_mul · 依賴：add_inverse, neg_mul

葉節點依據：neg_mul + add_inverse + distributive

p−q=−(q−p)（加法反元素）；依負號與乘法 (−w)(−w)=w·w，所以 (p−q)²=(−(q−p))²=(q−p)²。這證得引理 L_neg_sq；它是多項式恆等式（N6）。



S09.1 · implies操作前

a^2+b^2=0

操作後

a=0\ \land\ b=0

條件：a,b\in\mathbb{R}

規則：square_nonneg · 依賴：square_nonneg

葉節點依據：square_nonneg + order_basics + eq_congruence

a²≥0 且 b²≥0。由 a²+b²=0 得 a²=−b²≤0；又 a²≥0，依序的三一律 a²=0，再依 square_nonneg（u²=0 ⇔ u=0）得 a=0。b 同理。



S09.2 · implies操作前

a=0\ \land\ b=0

操作後

a^2+b^2=0

條件：無

規則：mul_zero · 依賴：mul_zero

葉節點依據：mul_zero + add_zero

反向：0·0+0·0=0+0=0。S09.1 與 S09.2 合起來證得引理 L_sum_sq_zero 的兩個方向。



S11.1 · implies操作前

0\le a<b

操作後

a^2<b^2

條件：a\ge 0

規則：order_basics · 依賴：distributive, order_basics

葉節點依據：distributive + order_basics + neg_mul

b²−a²=(b−a)(b+a)（用分配律展開可驗，N17）。b−a>0；又 b>a≥0，所以 b>0，b+a>0。兩個正數相乘為正（序與乘法），所以 b²−a²>0，即 a²<b²。



S11.2 · implies操作前

a,b\ge 0,\ a^2<b^2

操作後

a<b

條件：a\ge 0; b\ge 0

規則：contrapositive · 依賴：S11.1, order_basics

葉節點依據：contrapositive + case_analysis + order_basics

用逆否：若 a<b 不成立，依三一律 a=b 或 b<a。a=b 時 a²=b²；b<a 時由 S11.1（角色互換，0≤b<a）得 b²<a²。兩種情況都使 a²<b² 不成立。所以 a²<b² 推出 a<b。S11.1 與 S11.2 合起來證得引理 L_sq_mono。







## 逐步反向審查


- S13 · sufficient_goal_reduction · S02, S05, S06, S07, S08, S09, S12 — 目標是 goal 中的五個敘述。足夠條件 H：S05（例子）、S12（範圍）、S02（非負）、S06（對稱）、S07 到 S09（為 0 的條件）各自成立；H 推出目標只用合取。每個 H 都由定義與前提正向證成，沒有把目標當作前提。
- S12 · premise_audit · L_sq_mono, sqrt_def, numeric_evaluation, contradiction — 若 √26=5.1，則 (√26)²=5.1²，即 26=26.01，矛盾；有限位小數只給出範圍，不給出等式。
- S11.2 · premise_audit · S11.1, order_basics, contrapositive, case_analysis — 兩種情況涵蓋 a<b 不成立的全部可能；用到 S11.1 時需要 b≥0。
- S11.1 · premise_audit · distributive, order_basics — 需要 a≥0 才能保證 b+a>0；若 a=−7、b=6，b+a<0，結論失敗。
- S11 · inverse_equivalence · L_sq_mono, sqrt_def — 引理是雙條件，但只對非負數成立；例如 −7<6 而 (−7)²=49>36（N18）。
- S10 · inverse_equivalence · mko_length_def, numeric_evaluation — 與 S03 到 S04 相同的計算，可重算（N8）。
- S09.2 · premise_audit · mul_zero, add_zero — 直接代入計算，沒有附加條件。
- S09.1 · premise_audit · square_nonneg, order_basics — 需要兩個平方都非負；若允許負數項（例如 1+(−1)=0，N19），和為 0 並不推出各項為 0。所以只對實數的平方成立。
- S09 · inverse_equivalence · L_sum_sq_zero, cartesian_product_def, S08 — 引理與有序對相等都是雙條件，兩向成立。
- S08 · inverse_equivalence · sqrt_def, S07 — 兩個方向各有理由；需要 s≥0（S02），否則 √s 沒有定義。
- S07 · inverse_equivalence · sqrt_def, mul_zero, add_zero — 唯一滿足 b≥0、b²=0 的是 b=0，雙向成立。
- S06.1 · inverse_equivalence · neg_mul, add_inverse — 恆等式，雙向成立。
- S06 · inverse_equivalence · L_neg_sq, eq_replace — 兩邊的被開方數逐項相等，等值代換雙向成立。
- S05 · inverse_equivalence · sqrt_def, numeric_evaluation — 反向：5²=25 且 5≥0，正是 √25=5 的刻畫；唯一性由定義保證。
- S04 · inverse_equivalence · numeric_evaluation — 精確整數運算，可獨立重算（N3）。
- S03 · inverse_equivalence · numeric_evaluation, add_inverse — 反向：1+3=4、−2+4=2，還原 Q 的座標。
- S02 · premise_audit · square_nonneg, order_basics, sqrt_def — 需要實數平方非負；若坐標可以是一般的複數，這一步不成立，所以假設 a2（實數坐標）不可省。
- S01 · premise_audit · G2, mko_length_def — 此步只寫出定義；√ 是否有定義要在 S02 確認。





## 錯誤控制與反例

先平方再相加MKO 指出的誤解之一是把座標差直接相加而沒有先平方。對 P、Q，3+4=7，但 7²=49≠25（N16），所以 7 不是 d(P,Q)；正確順序是先平方 9+16=25，再開方得 5。座標差可能為負，直接相加還可能互相抵消：差為 1 與 −1 時和為 0，但距離是 √(1+1)=√2≠0（N20）。

平方根取非負主值MKO 指出的另一誤解是忽略非負主值。−5 也滿足 x²=25，但距離取主值 √25=5（S05）；寫成 d=±5 或 d=−5 違反 MKO 假設 a3。S02 證明對任何兩點 d≥0。

浮點數不是精確值MKO 說明程式可用 hypot 或平方根計算距離，但浮點表示與實數不同。√26 的小數顯示只是近似：5.1²=26.01≠26（N13），5.0990195²<26（N14）。精確答案是 √26，可用 S11 到 S12 的平方比較給出有保證的範圍。


- d(P,Q)=3+4=7 → reject — 7²=49≠25；距離公式先平方再相加（N16）。
- d(P,Q)=−5，因為 (−5)²=25 → reject — 主平方根取非負值，√25=5（S05）。
- √26=5.1 → reject — 5.1²=26.01≠26（N13）；5.1 只是近似值。
- 若 x 差為 1、y 差為 −1，兩差相加為 0，所以兩點距離為 0 → reject — 距離是 √(1²+(−1)²)=√2≠0；依 S09，距離為 0 只在兩點相同時發生（N20）。





## 結論與限制

d(P,Q)=√(3²+4²)=√25=5；d(P,R)=√(1²+5²)=√26，且 5.09<√26<5.1，所以 5.1 只是近似值。對任何實數坐標，d(P,Q) 有定義且 ≥0，d(Q,P)=d(P,Q)，d(P,P)=0，並且 d(P,Q)=0 ⇔ P=Q。


- 本稿不證明三角不等式，也不處理 d 作為度量的完整性質；MKO 所說與 Mathlib EuclideanSpace、dist 的對接未在此處理。
- 本稿不證明 √26 是無理數，只證明它不等於 5.1 並給出範圍。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 539f8e100b34dcd38a4feb966f262090b32061cef14dde0554cb042ed2f3f5ba
- original source SHA-256: 59692cf052ef581c917f890361bf9fcff19ab54ab5de2bfb61c90c72770ae0f2
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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