# 歐氏距離公式：計算距離、拒絕負根並以平方比較

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

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

derivation-mko-distance-formula-01 · production-20261019-adopted-96



## 目標與範圍

在同一個等單位正交座標系中，設 P=(1,2)、Q=(4,6)、R=(6,−1)。求 d(P,Q)，並說明候選值 −5 為何不是距離；求 d(P,R) 的精確形式並判定它不是整數；以平方比較 d(P,Q) 與 d(P,R)；最後核對重合點的距離為零，以及距離與兩點的書寫順序無關。

只在 MKO 的範圍內工作：平面、兩點位於同一個兩軸同單位的正交座標系、整數座標。完整證明「兩個非負量可用平方比較」的引理；不證明三角不等式或 d 是度量，不處理斜交或不等尺度的框架（只在錯誤控制中說明差異），也不建立 Lean 的 EuclideanSpace 橋接；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- numeric_evaluation
- power_laws
- square_nonneg
- sqrt_def
- order_basics


- G1 — 框架：所有點的座標都取自同一個正交座標系，兩軸採同一長度單位（MKO 假設 a1）。
- G2 — P=(1,2)、Q=(4,6)、R=(6,−1)，座標為整數（MKO 假設 a2）。
- G3 — 有人提出候選值 c=−5 作為 d(P,Q)，理由是 (−5)²=25。


- d(P,Q) — P 與 Q 的歐氏距離
- (p_x,p_y),\ (q_x,q_y) — P、Q 在同一框架中的座標
- Q-P — 逐坐標相減得到的座標差
- \sqrt{a} — a≥0 的主平方根（非負）
- a,b — 引理中的兩個非負實數





## 規則與來源


- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
- 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。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
- 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。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_distance_def · cited — 在平面同一等單位正交座標系，P=(px,py)、Q=(qx,qy) 的歐氏距離為 d(P,Q)=√((qx−px)²+(qy−py)²)≥0。距離平方是兩個座標差平方之和；比較兩個距離可比較其非負平方值。 · mko-distance-formula
- L_sq_order · lemma — 對實數 a≥0、b≥0：a<b ⇔ a²<b²。





## 逐步主鏈

S01 · definition操作前

d(P,Q),\ P=(p_x,p_y),\ Q=(q_x,q_y)

操作後

d(P,Q)=\sqrt{(q_x-p_x)^2+(q_y-p_y)^2}

條件：P,Q\ \text{in one orthonormal equal-unit frame}

規則：mko_distance_def · 依賴：G1

葉節點依據：mko_distance_def + def_unfold

先寫出 MKO 的定義。公式只在 G1 的框架中代表歐氏距離：兩軸互相垂直，而且使用同一長度單位。做法是座標差先平方、再相加，最後取主平方根。



S02 · implies操作前

(q_x-p_x)^2+(q_y-p_y)^2

操作後

(q_x-p_x)^2+(q_y-p_y)^2\ge 0,\ \ d(P,Q)\ge 0

條件：無

規則：square_nonneg · 依賴：S01, square_nonneg

葉節點依據：square_nonneg + order_basics + sqrt_def

兩個平方各自 ≥0（square_nonneg），兩個非負數之和仍 ≥0（order_basics：由 0≤u 得 0+v≤u+v，再用 0≤v）。所以根號內的數非負，主平方根有定義；依 sqrt_def，主平方根本身 ≥0。因此對任何兩點，d(P,Q) 都有定義而且非負。



S03 · equivalent操作前

Q-P

操作後

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

條件：無

規則：numeric_evaluation · 依賴：S01, G2

葉節點依據：numeric_evaluation + add_inverse

代入 P=(1,2)、Q=(4,6)，逐坐標相減：4−1=3、6−2=4。兩個座標差都取自同一框架（G1），所以可以放進同一個公式。



S04 · equivalent操作前

(q_x-p_x)^2+(q_y-p_y)^2

操作後

3^2+4^2=9+16=25

條件：無

規則：numeric_evaluation · 依賴：S03

葉節點依據：numeric_evaluation + power_laws

把 S03 的差代入根號內：3²=3·3=9，4²=4·4=16，相加得 25。這就是 d(P,Q)²（MKO：距離平方是座標差平方之和）。



S05 · equivalent操作前

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

操作後

d(P,Q)=5

條件：25\ge 0

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

葉節點依據：sqrt_def + eq_replace

由 S01、S04，d(P,Q)=√25。依 sqrt_def，√25 是唯一滿足 b≥0 且 b²=25 的實數 b；S05.1 檢查 5 滿足這兩個條件，S05.2 用唯一性得 √25=5。



S06 · implies操作前

c=-5,\ c^2=25

操作後

c\neq d(P,Q)

條件：無

規則：sqrt_def · 依賴：G3, S05

葉節點依據：sqrt_def + neg_mul + numeric_evaluation

候選值 −5 的平方確實是 (−5)(−5)=25（neg_mul），但 −5<0，不滿足 sqrt_def 的非負條件；而且 S05 已得 d(P,Q)=5，而 −5≠5。所以 −5 不是 d(P,Q)。這正是 MKO 指出的誤解：平方正確不足以成為距離（假設 a3）。



S07 · equivalent操作前

R-P

操作後

(6-1,\ -1-2)=(5,-3)

條件：無

規則：numeric_evaluation · 依賴：S01, G2

葉節點依據：numeric_evaluation + add_inverse

對 P=(1,2)、R=(6,−1) 逐坐標相減：6−1=5，−1−2=−3。座標差可以是負數；下一步平方後符號消失。



S08 · equivalent操作前

d(P,R)=\sqrt{5^2+(-3)^2}

操作後

d(P,R)=\sqrt{34},\ \ d(P,R)^2=34

條件：34\ge 0

規則：numeric_evaluation · 依賴：S07, sqrt_def

葉節點依據：numeric_evaluation + neg_mul + sqrt_def

5²=25，(−3)²=(−3)(−3)=9（neg_mul），和為 34，所以 d(P,R)=√34。34≥0，依 sqrt_def，(√34)²=34，即 d(P,R)²=34。



S09 · theorem_application操作前

d(P,Q)^2=25,\ d(P,R)^2=34,\ 25<34

操作後

d(P,Q)<d(P,R)

條件：d(P,Q)\ge 0; d(P,R)\ge 0

規則：L_sq_order · 依賴：S02, S04, S05, S08, L_sq_order

葉節點依據：L_sq_order + numeric_evaluation

依 S02 兩個距離都非負，所以可用引理 L_sq_order（a=d(P,Q)、b=d(P,R)）：25<34 推出 d(P,Q)<d(P,R)。這正是 MKO 說的「比較兩個距離可比較其非負平方值」；不需要求出 √34 的小數。引理在 S09.1、S09.2 證明。



S10 · implies操作前

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

操作後

5<\sqrt{34}<6,\ \ \sqrt{34}\notin\mathbb{Z}

條件：5\ge 0; \sqrt{34}\ge 0; 6\ge 0

規則：L_sq_order · 依賴：S08, S09, L_sq_order, sqrt_def

葉節點依據：L_sq_order + sqrt_def + order_basics + numeric_evaluation

5、√34、6 都非負（√34≥0 由 sqrt_def），它們的平方 25、34、36 滿足 25<34<36。用 L_sq_order 兩次得 5<√34<6。5 與 6 之間沒有整數，所以 √34 不是整數；這符合 MKO 假設 a2：要得到整數距離，平方和必須是完全平方，而 34 不是。答案以精確形式 √34 保存，不以浮點值冒充精確值。



S11 · equivalent操作前

d(P,P)

操作後

\sqrt{0^2+0^2}=\sqrt{0}=0

條件：無

規則：sqrt_def · 依賴：S01, S02, G2

葉節點依據：sqrt_def + numeric_evaluation

對重合點，座標差是 1−1=0 與 2−2=0，根號內為 0。0≥0 且 0²=0，依 sqrt_def 的唯一性 √0=0。所以重合點的距離是 0，這是合法的距離值（假設 a3），不是錯誤。



S12 · equivalent操作前

(p_x-q_x)^2+(p_y-q_y)^2

操作後

(q_x-p_x)^2+(q_y-p_y)^2

條件：無

規則：neg_mul · 依賴：S01, neg_mul

葉節點依據：neg_mul + add_inverse + eq_replace

p_x−q_x=−(q_x−p_x)，依 neg_mul，(−u)(−u)=uu，所以 (p_x−q_x)²=(q_x−p_x)²；y 坐標同理。兩個根號內的數相同，所以 d(Q,P)=d(P,Q)。例如 d(Q,P)²=(1−4)²+(2−6)²=9+16=25。依 MKO 第二段，交換兩點不構成新的計算。



S13 · implies操作前

\text{tasks of the goal}

操作後

d(P,Q)=5,\ d(P,R)=\sqrt{34},\ 5<\sqrt{34}<6,\ -5\neq d(P,Q)

條件：無

規則：and_intro_elim · 依賴：S05, S06, S08, S09, S10, S11, S12

葉節點依據：and_intro_elim

把各步結論合併：d(P,Q)=5（S05），−5 被拒絕（S06），d(P,R)=√34 不是整數且介於 5 與 6 之間（S08、S10），d(P,Q)<d(P,R)（S09），重合點距離為 0（S11），距離與順序無關（S12）。







## 局部子步與引理

S05.1 · implies操作前

b=5

操作後

b\ge 0\ \land\ b^2=25

條件：無

規則：numeric_evaluation · 依賴：numeric_evaluation

葉節點依據：numeric_evaluation + order_basics

5>0，所以 5≥0；5²=5·5=25。這兩項正是 sqrt_def 對 √25 的兩個要求。



S05.2 · implies操作前

5\ge 0,\ 5^2=25

操作後

\sqrt{25}=5

條件：無

規則：sqrt_def · 依賴：S05.1, sqrt_def

葉節點依據：sqrt_def

sqrt_def 說滿足 b≥0 且 b²=25 的實數恰有一個，記為 √25。S05.1 顯示 5 是這樣的數，所以 √25=5。



S09.1 · implies操作前

0\le a<b

操作後

a^2<b^2

條件：a\ge 0

規則：order_basics · 依賴：order_basics, distributive

葉節點依據：order_basics + distributive + mul_zero + add_inverse

由 a≥0 與 a<b 得 b>0，所以 b+a≥b>0；又 b−a>0。依 order_basics（u<v 且 w>0 ⇒ uw<vw，取 u=0、v=b−a、w=b+a）得 0<(b−a)(b+a)。依分配律 (b−a)(b+a)=b²−a²，所以 b²−a²>0，兩邊同加 a² 得 a²<b²。



S09.2 · implies操作前

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

操作後

a<b

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

規則：contradiction · 依賴：S09.1, order_basics

葉節點依據：contradiction + order_basics + eq_congruence + case_analysis

假設 a<b 不成立。依三分律，b=a 或 b<a。若 b=a，則 b²=a²（eq_congruence），與 a²<b² 矛盾。若 b<a，因 b≥0，可用 S09.1（角色互換）得 b²<a²，也與 a²<b² 矛盾。所以 a<b。S09.1 與 S09.2 合起來證得引理 L_sq_order 的兩個方向。







## 逐步反向審查


- S13 · sufficient_goal_reduction · S05, S06, S09, S10, S11, S12 — 目標 G：題目要求的各項結論。足夠條件 H：S05 到 S12 的結論同時成立；H⇒G 只用合取。H 都由 G1 到 G3 正向推出，沒有把 G 當作前提。
- S12 · inverse_equivalence · neg_mul, add_inverse — 這是對所有實數成立的恆等式（N14），兩個方向都成立。
- S11 · inverse_equivalence · sqrt_def, numeric_evaluation — 每一個等號都是同一個數的不同寫法，雙向成立。
- S10 · premise_audit · S08, L_sq_order, sqrt_def, order_basics — 三個數都非負才能用引理；「5 與 6 之間沒有整數」是整數的序性質。只推出 √34 不是整數，不宣稱任何小數展開。
- S09.2 · premise_audit · S09.1, order_basics, contradiction, eq_congruence — 反證需要三分律涵蓋所有情況，並需要 b≥0 才能套用 S09.1。
- S09.1 · premise_audit · order_basics, distributive, mul_zero — 需要 a≥0 才能保證 b+a>0；若允許 a 為負，例如 a=−6、b=5，結論 a²<b² 不成立。
- S09 · premise_audit · S02, L_sq_order — 引理的前提是兩邊非負（S02）；對可能為負的數，平方比較不成立（見錯誤控制）。
- S08 · inverse_equivalence · numeric_evaluation, sqrt_def — 反向：若 d≥0 且 d²=34，依 sqrt_def 的唯一性 d=√34；根號內的計算可重算（N9）。
- S07 · inverse_equivalence · numeric_evaluation — 反向：1+5=6、2+(−3)=−1，還原 R 的座標。
- S06 · premise_audit · S05, sqrt_def, neg_mul — 拒絕的理由是符號條件與唯一性；不宣稱 −5 與 d(P,Q) 毫無關係，兩者只差一個負號。
- S05.2 · premise_audit · S05.1, sqrt_def — 需要 sqrt_def 的唯一性與 S05.1 的兩個條件；少了 b≥0 就無法排除 −5。
- S05.1 · premise_audit · numeric_evaluation, order_basics — 只檢查一個候選值；不宣稱 5 是唯一滿足 b²=25 的實數（−5 也滿足），唯一性還要加上 b≥0。
- S05 · inverse_equivalence · sqrt_def, eq_replace — √25 與 5 是同一個數，以等值代換互換，雙向成立。
- S04 · inverse_equivalence · numeric_evaluation, power_laws — 每一個等號都是精確整數計算，可以獨立重算（N3），雙向成立。
- S03 · inverse_equivalence · numeric_evaluation — 反向：1+3=4、2+4=6，還原 Q 的座標；兩邊是同一對數。
- S02 · premise_audit · S01, square_nonneg, order_basics, sqrt_def — 只需要實數平方非負與主平方根的定義；反向（由 d≥0 推出任何關於座標的資訊）並未宣稱。
- S01 · premise_audit · G1, mko_distance_def — 此步只寫出定義並確認框架條件，不推出新事實；若框架不符合 G1，後面的計算都不適用。





## 錯誤控制與反例

負根不是距離MKO 指出的第一個誤解是把負平方根當距離。方程 b²=25 有兩個實數解 5 與 −5，但距離是主平方根，必須非負（S02、S06）。檢查候選距離要同時核對兩件事：平方等於平方和，而且值非負。

先確認框架公式只在兩軸互相垂直且同單位的框架中給出歐氏距離。若 x 軸一格是 1 cm、y 軸一格是 2 cm，座標差 (3,4) 代表實際位移 3 cm 與 8 cm，實際距離是 √(9+64)=√73 cm，不是 5 cm。若兩軸夾 60° 且同單位，向量 3e₁+4e₂ 的長度平方是 9+16+2·3·4·cos60°=37，也不是 25（這個計算用到內積，本稿不證明）。所以 S01 先確認 G1。

平方比較需要非負引理 L_sq_order 要求 a、b≥0。對一般實數它不成立：−6<5，但 (−6)²=36>25。距離可以用平方比較，是因為 S02 保證距離非負。


- 因為 (−5)²=25，所以 d(P,Q)=−5 也是正確答案 → reject — 距離是主平方根，必須 ≥0；−5<0。
- d(P,Q)=|3|+|4|=7 → reject — 這是曼哈頓（L¹）距離，屬於另一個度量；歐氏距離是 √25=5，而 7≠5。
- d(P,R) 恰好等於 5.83 → reject — 5.83²=33.9889≠34；精確值是 √34。
- −6<5，所以 (−6)²<5² → reject — (−6)²=36>25；平方比較只對非負數成立。





## 結論與限制

在同一等單位正交框架中，d(P,Q)=5；候選值 −5 雖然平方為 25，但為負，不是距離。d(P,R)=√34，不是整數，且 5<√34<6；由 25<34 得 d(P,Q)<d(P,R)。重合點距離為 0，且 d(Q,P)=d(P,Q)。


- 本稿不證明三角不等式，也不證明 d 滿足全部度量公理；只用到 d≥0、平方公式與對稱性。
- 錯誤控制中 60° 斜交框架的長度計算用到內積公式，本稿未證明，只作對照說明。
- MKO 的 formal next（綁定 EuclideanSpace ℝ (Fin 2)）未做。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 7504f016b13763fd8c797e2dbf0a09a7117e6f60892b44e03628e66cbaba7743
- original source SHA-256: 7504f016b13763fd8c797e2dbf0a09a7117e6f60892b44e03628e66cbaba7743
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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