畢達哥拉斯定理：在座標模型中以內積證明

目標與範圍

在以 ℝ² 表示的歐幾里得平面中（距離為歐幾里得長度），證明：對任何直角三角形 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 — 實數的序：任兩數恰有 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。
• 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²。

逐步主鏈

\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

B-C,\ A-C

u=(u_1,u_2)=B-C,\ v=(v_1,v_2)=A-C,\ u\neq 0,\ v\neq 0

A-B

v-u

\gamma=\tfrac{\pi}{2}

u\cdot v=u_1v_1+u_2v_2=0

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

(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)

(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

c^2=a^2+b^2-2\,u\cdot v,\ u\cdot v=0

a^2+b^2=c^2

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

C=(1,2),\ B=(4,6),\ A=(-7,8)

\triangle ABC\ \text{nondegenerate}

u=B-C=(3,4),\ v=A-C=(-8,6)

u\cdot v=-24+24=0,\ \gamma=\tfrac{\pi}{2}

a^2,\ b^2,\ c^2\ \text{for the example}

25+100=125

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

\text{S08, S09, S12, S13}

\forall\ \text{right triangles}:\ a^2+b^2=c^2

局部子步與引理

\cos\theta=\frac{u\cdot v}{|u|\,|v|},\ u\neq 0,\ v\neq 0

\cos\theta=0\iff u\cdot v=0

\theta\in[0,\pi]

\theta=\tfrac{\pi}{2}\iff\cos\theta=0\iff u\cdot v=0

(p-q)^2=(p-q)(p-q)

p^2-2pq+q^2

逐步反向審查

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