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

目標與範圍

在以 ℝ² 表示的歐幾里得平面中，設 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²。

逐步主鏈

d(P,Q)

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

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

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

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

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

3^2+4^2

25

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

d(P,Q)=5

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)

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

\sqrt{0}=0

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

s=0

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

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

d(P,R)

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

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

5<\sqrt{26}<6

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

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

\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

局部子步與引理

(p-q)^2

(q-p)^2

a^2+b^2=0

a=0\ \land\ b=0

a=0\ \land\ b=0

a^2+b^2=0

0\le a<b

a^2<b^2

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

a<b

逐步反向審查

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