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

目標與範圍

在同一個等單位正交座標系中，設 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²。

逐步主鏈

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}

(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

Q-P

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

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

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

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

d(P,Q)=5

c=-5,\ c^2=25

c\neq d(P,Q)

R-P

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

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

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

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

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

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

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

d(P,P)

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

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

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

\text{tasks of the goal}

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

局部子步與引理

b=5

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

5\ge 0,\ 5^2=25

\sqrt{25}=5

0\le a<b

a^2<b^2

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

a<b

逐步反向審查

• 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、反控制與修訂記錄）