# 畢達哥拉斯定理：在座標模型中以內積證明 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-euclid-pythagorean-theorem/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-euclid-pythagorean-theorem-01 · production-20261019-adopted-96 ## 目標與範圍 在以 ℝ² 表示的歐幾里得平面中（距離為歐幾里得長度），證明：對任何直角三角形 ABC，若直角在 C，兩股長 a=d(C,B)、b=d(C,A)，斜邊長 c=d(B,A)，則 a²+b²=c²。再以 C=(1,2)、B=(4,6)、A=(−7,8) 驗算（25+100=125），並以非直角三角形 E=(0,0)、F=(4,0)、H=(1,2) 說明沒有直角時關係一般不成立。 在 ℝ² 座標模型中證明定理：長度用歐幾里得長度的 MKO，直角用直角三角形的 MKO，內角量值用 G2 的餘弦式。證明是內積版本，相當於 MKO 所說的向量夾角版本；不證明 MKO 摘要中的面積拼補法，也不證明逆定理；不處理綜合幾何模型或其他頂點表示法與本模型的等價（MKO formal next）；不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - square_nonneg - sqrt_def - distributive - cartesian_product_def - numeric_evaluation - G1 — 模型：歐幾里得平面以 ℝ² 表示（MKO 假設 a1），點的坐標為實數，運算逐坐標；距離 d(P,Q)=√((x₂−x₁)²+(y₂−y₁)²)；內積 u·v=u₁v₁+u₂v₂；對相異點 P≠Q，直線 L(P,Q)={P+t(Q−P) ∣ t∈ℝ}。 - G2 — 內角量值：非退化三角形的頂點 X 處，令 u=Y−X、v=Z−X（皆非零），內角是唯一滿足 cos θ=(u·v)/(|u||v|) 的 θ∈[0,π]，其中 |u|=√(u·u)。 - G3 — ABC 是任意一個非退化三角形，其 C 處內角 γ=π/2（MKO 假設 a2）；a=d(C,B)、b=d(C,A) 是兩股長，c=d(B,A) 是斜邊長（假設 a3），三者都是非負實數（假設 a4）。除此之外對 ABC 不作任何假設。 - G4 — 例子：C=(1,2)、B=(4,6)、A=(−7,8)；對照：E=(0,0)、F=(4,0)、H=(1,2)。 - a,b,c — 兩股長與斜邊長 - u=B-C,\ v=A-C — 從直角頂點 C 出發的兩個邊向量 - u\cdot v — 內積 u₁v₁+u₂v₂ - d(P,Q) — 歐幾里得距離 - \gamma — C 處的內角量值 ## 規則與來源 - square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。 - sqrt_def · prerequisite — 主平方根：對 a≥0，√a 是唯一滿足 b≥0 且 b²=a 的實數 b。負數在實數中沒有平方根。 - distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。 - cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。 - add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。 - add_comm · prerequisite — 加法交換律：u+v=v+u。 - add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。 - mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。 - order_basics · prerequisite — 實數的序：任兩數恰有 uv 之一；u0 推出 uwvw。 - mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。 - logic_chain · prerequisite — 推論的傳遞：由 P⇒Q 與 Q⇒R 得 P⇒R；⇔ 同理。 - injective_surjective_def · prerequisite — 單射：f(a)=f(a′) ⇒ a=a′。滿射：每個 b∈B 都有 a∈A 使 f(a)=b。雙射：既單又滿，此時有唯一反函數 f⁻¹ 使 f⁻¹∘f=id_A、f∘f⁻¹=id_B。 - eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。 - mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。 - neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。 - add_zero · prerequisite — 加法單位元：u+0=u。 - eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。 - forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。 - image_preimage_def · prerequisite — 像與原像：f(S)={f(a) ∣ a∈S}；f⁻¹(T)={a∈A ∣ f(a)∈T}。原像記號不預設 f 有反函數。 - contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。 - power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - mko_right_triangle_def · cited — 若三角形的一個內角等於九十度，或以弧度表示為 π/2，則此三角形稱為直角三角形。 · mko-right-triangle - mko_length_def · cited — 獨立來源追加式勘誤（使用者已採用於本地修訂；未合併或發布）：在歐幾里得平面中，若 P=(x₁,y₁)、Q=(x₂,y₂)，則兩點距離取座標差平方和的非負主平方根；P=Q 時此值為 0。原來源的「正平方根」字樣保留於父版與修訂紀錄。 · mko-euclidean-length - dot_def · prerequisite — 內積與長度：u·v=u₁v₁+u₂v₂，|u|=√(u₁²+u₂²)。 - coord_ops · prerequisite — 逐坐標運算：(a,b)+(c,d)=(a+c,b+d)，(a,b)−(c,d)=(a−c,b−d)，t(a,b)=(ta,tb)。 - angle_cos_def · prerequisite — 座標模型中的內角量值：頂點 X、u=Y−X、v=Z−X 非零時，X 處內角是唯一滿足 cos θ=(u·v)/(|u||v|) 的 θ∈[0,π]。 - cos_facts · prerequisite — 餘弦函數在 [0,π] 上嚴格遞減（因此在 [0,π] 上單射），且 cos(π/2)=0。 - line_unique · prerequisite — 在 ℝ² 中，通過相異兩點 X、Y 的直線恰有一條，就是 L(X,Y)。 - L_right_iff_dot · lemma — 對非零向量 u、v 與 θ∈[0,π]，若 cos θ=(u·v)/(|u||v|)，則 θ=π/2 ⇔ u·v=0。 - L_sq_diff · lemma — 對實數 p、q：(p−q)²=p²−2pq+q²。 ## 逐步主鏈 S01 · definition操作前 \text{right triangle }ABC,\ \gamma=\tfrac{\pi}{2} 操作後 a=d(C,B),\ b=d(C,A),\ c=d(B,A);\ \text{goal}\ a^2+b^2=c^2 條件：無 規則：def_intro · 依賴：G1, G3, mko_length_def, mko_right_triangle_def 葉節點依據：def_intro + mko_right_triangle_def + mko_length_def 把定理的資料寫成模型中的量：依直角三角形的 MKO，ABC 有一個內角等於 π/2；把直角的頂點命名為 C（頂點名稱可以任意調換，所以不失一般性）。兩股是以 C 為端點的兩邊，斜邊是 C 的對邊，三者的長度依歐幾里得長度的 MKO 計算，都是非負實數（假設 a4）。目標是 a²+b²=c²。 S02 · definition操作前 B-C,\ A-C 操作後 u=(u_1,u_2)=B-C,\ v=(v_1,v_2)=A-C,\ u\neq 0,\ v\neq 0 條件：無 規則：def_intro · 依賴：G1, G3 葉節點依據：def_intro + coord_ops 以 C 為起點引入兩個邊向量 u=B−C、v=A−C。三角形非退化，所以 B≠C、A≠C，於是 u、v 都不是零向量。 S03 · equivalent操作前 A-B 操作後 v-u 條件：無 規則：coord_ops · 依賴：S02 葉節點依據：coord_ops + add_assoc + add_comm + add_inverse v−u=(A−C)−(B−C)=A−C−B+C=A−B，逐坐標都是恆等式（N3）。所以斜邊方向的差向量可以用兩個股向量表示。 S04 · equivalent操作前 \gamma=\tfrac{\pi}{2} 操作後 u\cdot v=u_1v_1+u_2v_2=0 條件：u\neq 0; v\neq 0 規則：L_right_iff_dot · 依賴：S02, G2, L_right_iff_dot 葉節點依據：L_right_iff_dot + angle_cos_def 依 G2，C 處內角 γ∈[0,π] 滿足 cos γ=(u·v)/(|u||v|)。依引理 L_right_iff_dot，γ=π/2 ⇔ u·v=0。這把幾何的「直角」轉成代數的「內積為零」。引理在 S04.1、S04.2 證明。 S05 · equivalent操作前 a=d(C,B),\ b=d(C,A),\ c=d(B,A) 操作後 a^2=u_1^2+u_2^2,\ b^2=v_1^2+v_2^2,\ c^2=(v_1-u_1)^2+(v_2-u_2)^2 條件：a,b,c\ge 0 規則：sqrt_def · 依賴：S02, S03, G1, sqrt_def 葉節點依據：sqrt_def + mko_length_def + eq_replace 依距離定義，a=√((x_B−x_C)²+(y_B−y_C)²)=√(u₁²+u₂²)；被開方數 ≥0，主平方根滿足 (√s)²=s，所以 a²=u₁²+u₂²。同理 b²=v₁²+v₂²。對 c，A−B=v−u（S03），所以 c²=(v₁−u₁)²+(v₂−u₂)²。 S06 · equivalent操作前 (v_1-u_1)^2+(v_2-u_2)^2 操作後 (v_1^2-2u_1v_1+u_1^2)+(v_2^2-2u_2v_2+u_2^2) 條件：無 規則：L_sq_diff · 依賴：S05, L_sq_diff 葉節點依據：L_sq_diff + mul_comm + eq_replace 對每個坐標使用引理 L_sq_diff（p=v_i、q=u_i）：(v_i−u_i)²=v_i²−2v_iu_i+u_i²，再用乘法交換律把中間項寫成 −2u_iv_i。引理在 S06.1 證明。 S07 · equivalent操作前 (v_1^2-2u_1v_1+u_1^2)+(v_2^2-2u_2v_2+u_2^2) 操作後 c^2=a^2+b^2-2\,u\cdot v 條件：無 規則：add_comm · 依賴：S05, S06 葉節點依據：add_comm + add_assoc + distributive + dot_def 重新分組（加法交換律與結合律、分配律）：=(u₁²+u₂²)+(v₁²+v₂²)−2(u₁v₁+u₂v₂)。依 S05 與內積定義，這是 a²+b²−2u·v。注意這個等式對任何三角形都成立（N1 是四個變數的多項式恆等式），尚未用到直角。 S08 · implies操作前 c^2=a^2+b^2-2\,u\cdot v,\ u\cdot v=0 操作後 a^2+b^2=c^2 條件：u\cdot v=0 規則：eq_replace · 依賴：S04, S07 葉節點依據：eq_replace + mul_zero + add_zero + eq_refl_symm_trans 直角在這裡才用上：依 S04，u·v=0，代入 S07 得 c²=a²+b²−2·0=a²+b²；由等號的對稱即 a²+b²=c²。 S09 · implies操作前 a^2+b^2=c^2\ \text{for the arbitrary right triangle of G3} 操作後 \text{every right triangle of the model}:\ a^2+b^2=c^2 條件：無 規則：forall_intro · 依賴：S01, S08 葉節點依據：forall_intro S01 到 S08 只用到 G3 所說的「非退化、C 處為直角」，沒有用到任何具體坐標，所以 ABC 是任意的；依全稱推廣，模型中每個直角三角形都有 a²+b²=c²。若直角在其他頂點，只要重新命名頂點即可。 S10 · implies操作前 C=(1,2),\ B=(4,6),\ A=(-7,8) 操作後 \triangle ABC\ \text{nondegenerate} 條件：C\neq B 規則：line_unique · 依賴：G4, line_unique 葉節點依據：line_unique + image_preimage_def + contradiction + numeric_evaluation 三點兩兩相異（第一坐標 1、4、−7 互不相同）。B−C=(3,4)，A∈L(C,B) ⇔ 有 t 使 (−7,8)=(1+3t, 2+4t) ⇔ t=−8/3 且 t=3/2，不可能，所以 A∉L(C,B)；依直線唯一性三點不共線，三角形非退化。 S11 · equivalent操作前 u=B-C=(3,4),\ v=A-C=(-8,6) 操作後 u\cdot v=-24+24=0,\ \gamma=\tfrac{\pi}{2} 條件：u\neq 0; v\neq 0 規則：L_right_iff_dot · 依賴：S10, S04, G4 葉節點依據：L_right_iff_dot + dot_def + numeric_evaluation u=(4−1, 6−2)=(3,4)，v=(−7−1, 8−2)=(−8,6)；u·v=3·(−8)+4·6=−24+24=0。依 S04 的等價，C 處是直角，例子符合 G3。 S12 · implies操作前 a^2,\ b^2,\ c^2\ \text{for the example} 操作後 25+100=125 條件：無 規則：numeric_evaluation · 依賴：S05, S11, G4 葉節點依據：numeric_evaluation + sqrt_def + power_laws a²=3²+4²=25，b²=(−8)²+6²=64+36=100；A−B=(−7−4, 8−6)=(−11,2)，c²=121+4=125；25+100=125，與 S08 一致。a=5、b=10、c=√125=5√5（因 5√5≥0 且 (5√5)²=25·5=125）。這只是一個例子的核對，不是定理的證明。 S13 · implies操作前 E=(0,0),\ F=(4,0),\ H=(1,2) 操作後 d(E,F)^2=16\neq 13+5=d(H,F)^2+d(H,E)^2 條件：無 規則：eq_replace · 依賴：S07, G4 葉節點依據：eq_replace + dot_def + numeric_evaluation 非直角的對照：H 不在 x 軸 L(E,F)={(4t,0)} 上（第二坐標 2≠0），所以 EFH 非退化。在 H：u=F−H=(3,−2)、v=E−H=(−1,−2)，u·v=−3+4=1≠0，所以 H 處不是直角。d(H,F)²=9+4=13，d(H,E)²=1+4=5，d(E,F)²=16；13+5=18≠16。S07 的一般等式給出 16=13+5−2·1，正好說明少掉的是 −2u·v 這一項。E、F 處的內積分別是 4 與 12，也都不是直角；三種配對 13+5=16、13+16=5、5+16=13 都不成立。 S14 · implies操作前 \text{S08, S09, S12, S13} 操作後 \forall\ \text{right triangles}:\ a^2+b^2=c^2 條件：無 規則：and_intro_elim · 依賴：S08, S09, S12, S13 葉節點依據：and_intro_elim + forall_intro 定理在模型中成立：每個直角三角形的兩股平方和等於斜邊平方。例子 25+100=125 與之一致；EFH 顯示沒有直角時一般不成立。 ## 局部子步與引理 S04.1 · equivalent操作前 \cos\theta=\frac{u\cdot v}{|u|\,|v|},\ u\neq 0,\ v\neq 0 操作後 \cos\theta=0\iff u\cdot v=0 條件：|u|\,|v|\neq 0 規則：mul_inverse_nonzero · 依賴：dot_def, square_nonneg 葉節點依據：square_nonneg + sqrt_def + order_basics + mul_inverse_nonzero + mul_zero u≠0 表示 u₁、u₂ 不全為 0；平方非負，且非零數的平方大於 0，所以 u₁²+u₂²>0，|u|>0。同理 |v|>0，故 |u||v|>0，特別是 ≠0。於是 cos θ=0 時兩邊乘 |u||v| 得 u·v=0；反之 u·v=0 時 cos θ=0/(|u||v|)=0。 S04.2 · equivalent操作前 \theta\in[0,\pi] 操作後 \theta=\tfrac{\pi}{2}\iff\cos\theta=0\iff u\cdot v=0 條件：\theta\in[0,\pi] 規則：cos_facts · 依賴：cos_facts, S04.1 葉節點依據：cos_facts + logic_chain + injective_surjective_def ⇒：cos(π/2)=0。⇐：cos 在 [0,π] 上嚴格遞減，所以在那裡單射；若 θ∈[0,π] 且 cos θ=0=cos(π/2)，則 θ=π/2。再與 S04.1 串接得 θ=π/2 ⇔ u·v=0。S04.1 與 S04.2 合起來證得引理 L_right_iff_dot。 S06.1 · equivalent操作前 (p-q)^2=(p-q)(p-q) 操作後 p^2-2pq+q^2 條件：無 規則：distributive · 依賴：distributive, neg_mul 葉節點依據：distributive + mul_comm + neg_mul + add_assoc 用分配律展開：(p−q)(p−q)=p·p−p·q−q·p+q·q；依交換律 qp=pq，兩個 −pq 合併成 −2pq（2pq=pq+pq）；(−q)(−q)=q²（負號與乘法）。得 p²−2pq+q²，是多項式恆等式（N2）。這證得引理 L_sq_diff。 ## 逐步反向審查 - S14 · sufficient_goal_reduction · S04, S07, S08, S09 — 目標：模型中所有直角三角形 a²+b²=c²。足夠條件 H：對任意直角三角形，c²=a²+b²−2u·v（S07）且 u·v=0（S04）；H 推出目標由 S08 與 S09。H 由定義與恆等式正向證成，沒有把目標當作前提。 - S13 · premise_audit · S07, dot_def, numeric_evaluation — 這說明定理的直角前提不可省；它不是定理的反例，因為 EFH 不是直角三角形。 - S12 · premise_audit · S05, S11, numeric_evaluation — 可獨立重算（N8 到 N12）；它支持 S08，但不能取代 S01 到 S09 的一般證明。 - S11 · inverse_equivalence · L_right_iff_dot, dot_def, numeric_evaluation — 精確計算可重算（N7）；引理雙向成立。 - S10 · premise_audit · line_unique, contradiction — 例子也必須先確認非退化，否則 G3 不適用。 - S09 · premise_audit · S01, S08, forall_intro — 全稱推廣要求沒有對 ABC 加額外假設；有限個例子（如 S12）不能取代這一步。 - S08 · premise_audit · S04, S07, eq_replace, mul_zero — 需要 u·v=0；沒有直角時多出的 −2u·v 一般不為 0（見 S13）。此步不宣稱逆命題。 - S07 · inverse_equivalence · add_comm, add_assoc, distributive, dot_def — 恆等式，雙向成立。 - S06.1 · inverse_equivalence · distributive, mul_comm, neg_mul — 恆等式，雙向成立。 - S06 · inverse_equivalence · L_sq_diff, mul_comm — 恆等式，雙向成立。 - S05 · inverse_equivalence · sqrt_def, mko_length_def — 對非負的 x 與 s，x=√s ⇔ x²=s；三個長度都非負（假設 a4），所以平方前後資訊相同。 - S04.2 · inverse_equivalence · cos_facts, logic_chain, S04.1 — ⇐ 方向需要 θ 限制在 [0,π]；若允許 θ=3π/2，cos θ=0 也成立。 - S04.1 · inverse_equivalence · mul_inverse_nonzero, square_nonneg, sqrt_def — 乘以與除以 |u||v| 互為反運算，前提 |u||v|≠0；若 u=0，分母為 0，式子沒有定義。 - S04 · inverse_equivalence · L_right_iff_dot, S02 — 引理是雙條件；u、v 非零（S02）不可省。 - S03 · inverse_equivalence · coord_ops, add_inverse — 恆等式，雙向成立。 - S02 · premise_audit · G3, def_intro, cartesian_product_def — 非零性來自非退化；若 B=C，u=0，C 處沒有角。 - S01 · premise_audit · G3, def_intro, mko_right_triangle_def, mko_length_def — 此步只命名；沒有對 ABC 加任何額外假設，這是 S09 能推廣到所有直角三角形的前提。 ## 錯誤控制與反例 只對直角三角形成立MKO 指出的誤解是把 a²+b²=c² 套用到任意三角形。S07 顯示一般三角形滿足的是 c²=a²+b²−2u·v；只有直角（u·v=0）時才去掉最後一項。EFH 沒有直角，13+5=18≠16（S13），所以不能把定理用在它身上。 模型的範圍MKO 的另一個誤解是把已形式化的指定向量邊長模型，誤認為所有仿射表示法都已自動完成等價證明。本稿同樣只在 ℝ² 座標模型中、以 C 出發的邊向量證明；其他頂點表示法、或綜合幾何的歐幾里得平面與本模型的等價，需要另外的定理（MKO formal next），本稿沒有證明。 斜邊必須是直角的對邊；例子不是證明公式中的 c 必須是直角所對的邊。在例子中若把股 b=10 誤當斜邊，會寫出 25+125=100，這不成立（N23）。另外，MKO 提醒有限檢查不能取代普遍證明：S12 的 25+100=125 只核對一個例子，定理的普遍性來自 S01 到 S09。 - 對三角形 EFH，兩短邊平方和等於最長邊平方：13+5=16 → reject — 13+5=18≠16；EFH 沒有直角（S13）。 - 例子中 25+100=125 成立，所以定理對所有直角三角形得證 → reject — 有限個例子只是核對；普遍性來自 S01 到 S09 的任意三角形論證。 - 在例子中把 b=10 當作斜邊：25+125=100 → reject — 150≠100（N23）；斜邊是直角 C 的對邊 AB。 - 直角三角形的兩股長相加等於斜邊長：5+10=√125 → reject — (5+10)²=225≠125（N24）；定理說的是平方的關係。 ## 結論與限制 在 ℝ² 座標模型中，對任意直角三角形（直角在 C），以 u=B−C、v=A−C 表示，恆有 c²=a²+b²−2u·v，而直角等價於 u·v=0，所以 a²+b²=c²。例子 C=(1,2)、B=(4,6)、A=(−7,8) 給出 25+100=125；非直角的 EFH 給出 13+5=18≠16，差額正是 2u·v=2。 - 內角量值以 G2 的餘弦式定義；cos_facts 與 line_unique 是前提，未在本稿推導。 - 本稿不證明逆定理（a²+b²=c² 推出直角），也不證明 MKO 摘要中的面積拼補法。 - 本稿的模型是 ℝ² 與歐幾里得長度；與綜合歐幾里得幾何或其他仿射表示法的等價需要另外的定理（MKO formal next）。 ## 驗證及來源綁定 24 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 8723c1e344103a9b4fb116bcfed73b10bf9b0fbc16c5935a181e826d20f1685b - original source SHA-256: 54d2c3d929a38adb25ccbcded51b2cfc53d2a26489ddb50f38f6f0d5fd2b93e7 - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-euclid-pythagorean-theorem-01.json)