# 直角三角形：用座標判定哪一個內角是直角

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

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

derivation-mko-right-triangle-01 · production-20261019-adopted-96



## 目標與範圍

在座標平面模型 ℝ² 中，設 A=(1,1)、B=(5,3)、C=(0,3)。證明 A、B、C 構成非退化三角形，且其在 A 的內角等於 90°（即 π/2），所以 ABC 是直角三角形；說明另外兩角不是直角、任何非退化三角形至多一個直角，並指出斜邊與兩股。再以 D=(1,4) 說明三角形 ABD 不是直角三角形。

在 ℝ² 座標模型中工作，內角量值以 G2 的餘弦式定義，取值於 [0,π]；直接使用 MKO 的定義（一個內角等於 90°=π/2），並先確認非退化三角形（MKO 假設 a1）。內角和定理以外部文獻引用（citation_verified），餘弦函數與直線唯一性作為前提。不證明畢氏定理，也不證明「斜邊最長」的一般敘述；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- cartesian_product_def
- image_preimage_def
- square_nonneg
- sqrt_def
- numeric_evaluation


- G1 — 模型：點是 ℝ² 的有序實數對，運算逐坐標進行；內積 u·v=u₁v₁+u₂v₂，長度 |u|=√(u₁²+u₂²)；對相異點 P≠Q，直線 L(P,Q)={P+t(Q−P) ∣ t∈ℝ}。
- G2 — 內角量值：對非退化三角形的頂點 X 與另兩頂點 Y、Z，令 u=Y−X、v=Z−X（皆非零），X 處內角的量值是唯一滿足 cos θ=(u·v)/(|u||v|) 的 θ∈[0,π]（弧度）。
- G3 — A=(1,1)、B=(5,3)、C=(0,3)、D=(1,4)。


- u\cdot v — 內積 u₁v₁+u₂v₂
- |u| — 向量長度 √(u₁²+u₂²)
- \theta_A,\theta_B,\theta_C — 三角形在 A、B、C 的內角量值（弧度）
- L(P,Q) — 通過相異點 P、Q 的直線
- 90^\circ,\ \tfrac{\pi}{2} — 同一個角的度數與弧度寫法





## 規則與來源


- cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
- image_preimage_def · prerequisite — 像與原像：f(S)={f(a) ∣ a∈S}；f⁻¹(T)={a∈A ∣ f(a)∈T}。原像記號不預設 f 有反函數。
- square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。
- sqrt_def · prerequisite — 主平方根：對 a≥0，√a 是唯一滿足 b≥0 且 b²=a 的實數 b。負數在實數中沒有平方根。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- 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。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- de_morgan_logic · prerequisite — 邏輯的德摩根律：¬(P∧Q) ⇔ ¬P∨¬Q；¬(P∨Q) ⇔ ¬P∧¬Q。
- mko_right_triangle_def · cited — 若三角形的一個內角等於九十度，或以弧度表示為 π/2，則此三角形稱為直角三角形。 · mko-right-triangle
- mko_triangle_def · cited — 給定平面中三個相異且不共線的點 A、B、C，線段 AB、BC、CA 的聯合界定非退化三角形 ABC。 · mko-triangle
- deg_rad · prerequisite — 度數與弧度：θ 度等於 θ·π/180 弧度；90° 與 π/2 表示同一角度（MKO 假設 a2）。
- 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)。
- collinear_def · prerequisite — 共線：若存在一條直線同時包含若干點，這些點稱為共線。
- thm_angle_sum · cited — 歐幾里得平面中，非退化三角形的三個內角之和等於兩個直角，即 π（180°）。 · Euclid, Elements, Book I, Proposition 32
- angle_positive · prerequisite — 非退化三角形的每個內角量值都嚴格介於 0 與 π 之間。
- L_right_iff_dot · lemma — 對非零向量 u、v 與 θ∈[0,π]，若 cos θ=(u·v)/(|u||v|)，則 θ=π/2 ⇔ u·v=0。





## 逐步主鏈

S01 · definition操作前

\triangle ABC\ \text{is a right triangle}

操作後

\triangle ABC\ \text{nondegenerate and some interior angle}=90^\circ=\tfrac{\pi}{2}

條件：無

規則：mko_right_triangle_def · 依賴：G2, mko_right_triangle_def

葉節點依據：mko_right_triangle_def + def_unfold

依 MKO，直角三角形是一個內角等於 90°（或弧度 π/2）的三角形，而且討論對象是平面中的非退化三角形（假設 a1）。所以要判定 ABC 是直角三角形，必須做兩件事：先確認 A、B、C 構成非退化三角形，再找出一個等於 π/2 的內角。內角量值用 G2 的定義。



S02 · equivalent操作前

90^\circ

操作後

\tfrac{\pi}{2}\ \text{rad}

條件：無

規則：deg_rad · 依賴：deg_rad

葉節點依據：deg_rad + frac_rules + numeric_evaluation

依換算 θ 度=θ·π/180 弧度：90·π/180=(90/180)·π=π/2。G2 的量值以弧度表示，所以之後的目標是 θ=π/2。



S03 · implies操作前

A=(1,1),\ B=(5,3),\ C=(0,3)

操作後

A\neq B,\ B\neq C,\ C\neq A

條件：無

規則：cartesian_product_def · 依賴：G3, cartesian_product_def

葉節點依據：cartesian_product_def + numeric_evaluation

第一坐標 1≠5、5≠0、0≠1，所以三點兩兩相異。特別地，u=B−A 與 v=C−A 都不是零向量，這是 G2 與之後引理所需的條件。



S04 · equivalent操作前

C\in L(A,B)

操作後

\exists t\in\mathbb{R}:\ t=-\tfrac{1}{4}\ \land\ t=1

條件：4\neq 0; 2\neq 0

規則：image_preimage_def · 依賴：G1, G3, S03

葉節點依據：image_preimage_def + cartesian_product_def + eq_congruence + mul_inverse_nonzero

B−A=(4,2)，L(A,B)={(1+4t, 1+2t) ∣ t∈ℝ}。C∈L(A,B) ⇔ 有 t 使 (0,3)=(1+4t, 1+2t) ⇔ 0=1+4t 且 3=1+2t。第一式兩邊減 1 再除以 4（4≠0）得 t=−1/4；第二式兩邊減 1 再除以 2（2≠0）得 t=1。每個變形都是等價。



S05 · implies操作前

\exists t:\ t=-\tfrac{1}{4}\ \land\ t=1

操作後

C\notin L(A,B)

條件：無

規則：contradiction · 依賴：S04

葉節點依據：contradiction + eq_refl_symm_trans + numeric_evaluation

若同一個 t 同時等於 −1/4 與 1，依等號的對稱與傳遞得 −1/4=1，但 −1/4≠1。所以沒有這樣的 t，依 S04，C∉L(A,B)。



S06 · implies操作前

A\neq B,\ C\notin L(A,B)

操作後

\triangle ABC\ \text{nondegenerate}

條件：A\neq B

規則：line_unique · 依賴：S03, S05, line_unique, mko_triangle_def

葉節點依據：line_unique + collinear_def + contradiction + mko_triangle_def

若某條直線同時包含 A、B、C，因 A≠B，依 line_unique 它就是 L(A,B)，於是 C∈L(A,B)，與 S05 矛盾。所以 A、B、C 不共線；加上 S03 的相異，依三角形的 MKO，ABC 是非退化三角形，MKO 假設 a1 成立。



S07 · equivalent操作前

u=B-A,\ v=C-A

操作後

u=(4,2),\ v=(-1,2),\ u\cdot v=0

條件：無

規則：dot_def · 依賴：G1, G3, S03

葉節點依據：dot_def + coord_ops + numeric_evaluation

逐坐標：u=(5−1, 3−1)=(4,2)，v=(0−1, 3−1)=(−1,2)。內積 u·v=4·(−1)+2·2=−4+4=0。這是精確的整數計算，沒有誤差。



S08 · equivalent操作前

u\cdot v=0,\ u\neq 0,\ v\neq 0

操作後

\theta_A=\tfrac{\pi}{2}

條件：u\neq 0; v\neq 0

規則：L_right_iff_dot · 依賴：S03, S06, S07, L_right_iff_dot

葉節點依據：L_right_iff_dot + angle_cos_def

ABC 非退化（S06），所以 G2 給出 A 處內角 θ_A∈[0,π]，cos θ_A=(u·v)/(|u||v|)，且 u、v 非零（S03）。依引理 L_right_iff_dot，u·v=0 ⇔ θ_A=π/2，所以 θ_A=π/2。引理在 S08.1、S08.2 證明。



S09 · implies操作前

\triangle ABC\ \text{nondegenerate},\ \theta_A=\tfrac{\pi}{2}

操作後

\triangle ABC\ \text{is a right triangle with the right angle at}\ A

條件：無

規則：mko_right_triangle_def · 依賴：S02, S06, S08, mko_right_triangle_def

葉節點依據：mko_right_triangle_def + exists_intro + and_intro_elim

非退化三角形 ABC 有一個內角 θ_A=π/2=90°（S02、S08），符合 MKO 的定義，所以 ABC 是直角三角形，直角在 A。



S10 · equivalent操作前

(A-B)\cdot(C-B)=(-4,-2)\cdot(-5,0)

操作後

20\neq 0,\ \theta_B\neq\tfrac{\pi}{2}

條件：A-B\neq 0; C-B\neq 0

規則：L_right_iff_dot · 依賴：S03, S06, G3, L_right_iff_dot

葉節點依據：L_right_iff_dot + dot_def + numeric_evaluation

在 B：A−B=(1−5, 1−3)=(−4,−2)，C−B=(0−5, 3−3)=(−5,0)，皆非零；內積 (−4)(−5)+(−2)·0=20≠0。引理是雙條件，兩邊同時否定仍等價：內積 ≠0 ⇔ θ_B≠π/2。



S11 · equivalent操作前

(A-C)\cdot(B-C)=(1,-2)\cdot(5,0)

操作後

5\neq 0,\ \theta_C\neq\tfrac{\pi}{2}

條件：A-C\neq 0; B-C\neq 0

規則：L_right_iff_dot · 依賴：S03, S06, G3, L_right_iff_dot

葉節點依據：L_right_iff_dot + dot_def + numeric_evaluation

在 C：A−C=(1−0, 1−3)=(1,−2)，B−C=(5−0, 3−3)=(5,0)，皆非零；內積 1·5+(−2)·0=5≠0，所以 θ_C≠π/2。



S12 · implies操作前

\theta_X=\theta_Y=\tfrac{\pi}{2}\ \text{at two vertices}\ X\neq Y

操作後

\text{contradiction; a nondegenerate triangle has at most one right angle}

條件：無

規則：contradiction · 依賴：thm_angle_sum, angle_positive

葉節點依據：thm_angle_sum + angle_positive + contradiction + forall_intro

對任意非退化三角形：若兩個內角都等於 π/2，依內角和定理，第三個角等於 π−π/2−π/2=0；但非退化三角形的每個內角都大於 0（angle_positive），矛盾。所以至多一個直角。這個論證不依賴具體座標，對每個非退化三角形成立；它與 S10、S11 的直接計算一致。



S13 · definition操作前

\theta_A=\tfrac{\pi}{2}

操作後

\text{hypotenuse}\ BC,\ \text{legs}\ AB,\ AC

條件：無

規則：def_intro · 依賴：S09, dot_def

葉節點依據：def_intro + dot_def + numeric_evaluation

直角所對的邊稱為斜邊，另外兩邊稱為股（MKO 說明）。A 的對邊是 BC，所以 BC 是斜邊，AB、AC 是股。核對長度平方：|AB|²=4²+2²=20，|AC|²=(−1)²+2²=5，|BC|²=(−5)²+0²=25；本例中斜邊最長（25>20>5）。這只是此例的核對，不是「斜邊最長」的一般證明。



S14 · implies操作前

A,\ B,\ D=(1,4)

操作後

\triangle ABD\ \text{nondegenerate}

條件：A\neq B

規則：line_unique · 依賴：G1, G3, line_unique

葉節點依據：line_unique + image_preimage_def + contradiction + mko_triangle_def

D 與 A、B 相異（D 的第二坐標 4 與 1、3 不同）。D∈L(A,B) ⇔ 有 t 使 1=1+4t 且 4=1+2t ⇔ t=0 且 t=3/2，不可能；所以 D∉L(A,B)。與 S06 同理，依直線唯一性 A、B、D 不共線，ABD 是非退化三角形。



S15 · implies操作前

(B-A)\cdot(D-A),\ (A-B)\cdot(D-B),\ (A-D)\cdot(B-D)

操作後

6,\ 14,\ 3\neq 0;\ \triangle ABD\ \text{not right}

條件：無

規則：L_right_iff_dot · 依賴：S14, L_right_iff_dot, G3

葉節點依據：L_right_iff_dot + dot_def + numeric_evaluation + de_morgan_logic

在 A：(4,2)·(0,3)=0+6=6；在 B：(−4,−2)·(−4,1)=16−2=14；在 D：(0,−3)·(4,−1)=0+3=3。三個內積都非零，依引理三個內角都不是 π/2，所以 ABD 沒有直角，依 MKO 不是直角三角形。AD 是鉛直的，但只有一邊鉛直不能決定直角。



S16 · implies操作前

\text{S09, S12, S13, S15}

操作後

\triangle ABC\ \text{right at}\ A;\ \triangle ABD\ \text{not right}

條件：無

規則：mko_right_triangle_def · 依賴：S09, S10, S11, S12, S13, S15

葉節點依據：mko_right_triangle_def + and_intro_elim

ABC 是直角三角形，直角在 A，另兩角不是直角，斜邊 BC、股 AB 與 AC；ABD 是非退化三角形但沒有直角。







## 局部子步與引理

S08.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|=√(u₁²+u₂²)>0。同理 |v|>0，故 |u||v|>0，特別是 ≠0。於是 cos θ=0 時兩邊乘 |u||v| 得 u·v=0；反之 u·v=0 時 cos θ=0/(|u||v|)=0。



S08.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, S08.1

葉節點依據：cos_facts + logic_chain + injective_surjective_def

⇒：cos(π/2)=0。⇐：cos 在 [0,π] 上嚴格遞減，所以在那裡單射；若 θ∈[0,π] 且 cos θ=0=cos(π/2)，則 θ=π/2。再與 S08.1 串接得 θ=π/2 ⇔ u·v=0。S08.1 與 S08.2 合起來證得引理 L_right_iff_dot。







## 逐步反向審查


- S16 · sufficient_goal_reduction · S06, S08, S14, S15, mko_right_triangle_def — 目標：ABC 是直角三角形而 ABD 不是。足夠條件 H：ABC 非退化且 θ_A=π/2（S06、S08），ABD 非退化且三個角都不是 π/2（S14、S15）；H 推出目標由 MKO 的定義。H 由前面各步正向證成，沒有把目標當作前提。
- S15 · premise_audit · S14, L_right_iff_dot, dot_def, numeric_evaluation — 要證「不是直角三角形」，三個角都必須排除；只排除一個不夠。
- S14 · premise_audit · line_unique, contradiction, mko_triangle_def — 與 S04 到 S06 相同的三個檢查：相異、不在 L(A,B) 上、直線唯一。
- S13 · premise_audit · S09, def_intro, dot_def — 命名只依賴直角的位置（S09）；長度平方只作核對，不參與推論。
- S12 · premise_audit · thm_angle_sum, angle_positive, contradiction, forall_intro — 需要內角和定理（外部引用，citation_verified）與每角為正；只靠一個例子的計算，不能推出「所有非退化三角形至多一個直角」。
- S11 · inverse_equivalence · L_right_iff_dot, dot_def, numeric_evaluation — 與 S10 相同，引理的雙條件兩邊同時否定（N7）。
- S10 · inverse_equivalence · L_right_iff_dot, dot_def, numeric_evaluation — P⇔Q 與 ¬P⇔¬Q 等價；計算可重算（N6）。
- S09 · premise_audit · S06, S08, mko_right_triangle_def, exists_intro — 定義只要求存在一個直角；兩個要求（非退化、有一角為 π/2）都已證。
- S08.2 · inverse_equivalence · cos_facts, logic_chain, S08.1 — ⇐ 方向需要 θ 限制在 [0,π]；若允許 θ=3π/2，cos θ=0 也成立，所以 G2 的取值範圍不可省略。
- S08.1 · inverse_equivalence · mul_inverse_nonzero, square_nonneg, sqrt_def — 乘以 |u||v| 與除以 |u||v| 互為反運算，前提 |u||v|≠0；若 u=0，分母為 0，cos θ 的式子沒有定義。
- S08 · inverse_equivalence · L_right_iff_dot, S03, S06 — 引理是雙條件，兩個方向都在子步證明；u、v 非零的條件不可省略。
- S07 · inverse_equivalence · dot_def, coord_ops, numeric_evaluation — 反向：A+u=(1+4,1+2)=(5,3)=B、A+v=(1−1,1+2)=(0,3)=C；內積可獨立重算（N5）。
- S06 · premise_audit · S03, S05, line_unique, collinear_def, mko_triangle_def, contradiction — 唯一性是關鍵：只有 C∉L(A,B)，若不知道通過 A、B 的直線只有一條，就不能排除其他直線。
- S05 · premise_audit · S04, contradiction, eq_refl_symm_trans — 每個坐標方程單獨都有解；矛盾來自兩式要用同一個 t。
- S04 · inverse_equivalence · image_preimage_def, cartesian_product_def, eq_congruence, mul_inverse_nonzero — 代回：1+4·(−1/4)=0、1+2·1=3；每個變形可逆（除數非零）。
- S03 · premise_audit · G3, cartesian_product_def — 一個坐標不同即可推出兩點不等；三對都要檢查。
- S02 · inverse_equivalence · deg_rad, numeric_evaluation — 反向：(π/2)·(180/π)=90，回到 90°；兩種寫法表示同一角度。
- S01 · premise_audit · mko_right_triangle_def, G2 — 此步只寫出定義，尚未推出任何事實；順序很重要：沒有非退化三角形，就沒有內角可談。





## 錯誤控制與反例

先確認非退化三角形MKO 指出的誤解是只看到兩條邊互相垂直，卻沒有確認它們與第三邊構成非退化三角形。例如 E=(1,1)=A 時 (B−A)·(E−A)=(4,2)·(0,0)=0（N18），內積為 0 只是因為 E−A 是零向量，A、B、E 根本不是三個相異點，沒有角可談。又如線段 [(0,0),(2,0)] 與 [(5,1),(5,3)] 方向互相垂直，但它們沒有共同端點，不是同一個三角形的兩邊。所以 S03 到 S06 必須在算角之前完成。

度數與弧度不可混用90° 與 π/2 弧度是同一角度（S02），但數字 90 與 π/2 不相等。若把 θ=90 代入以弧度為單位的 G2，它表示 90 弧度，不是直角：因為 π<4，π/2<2<90。寫角度時必須標明單位。

程式的容差檢查只是具體輸入檢查MKO 說明程式可以檢查三個輸入角是否在容差內加總為 180°、其中是否有 90°，但這只是對具體輸入的檢查。本稿用整數內積做精確判定（0、20、5），不需容差；而「至多一個直角」是 S12 的一般論證，不能由任何有限個例子的計算取代。


- E=(1,1) 時 (B−A)·(E−A)=0，所以 ABE 是直角三角形，直角在 A → reject — E=A，三點不相異，E−A 是零向量；沒有非退化三角形，也沒有角（MKO 假設 a1、G2）。
- 三角形 ABD 的邊 AD 是鉛直的，所以 ABD 有直角 → reject — 三個頂點的內積為 6、14、3，都非零（S15），沒有任何內角等於 π/2。
- 某些非退化三角形有兩個直角 → reject — 若有兩個直角，第三角即為 π−π/2−π/2=0，與每個內角大於 0 矛盾（S12）。
- ABC 的直角在 A，所以斜邊是 AB → reject — 斜邊是直角所對的邊，即 BC；AB 以 A 為端點，是股。本例 |BC|²=25 也大於 |AB|²=20。





## 結論與限制

A=(1,1)、B=(5,3)、C=(0,3) 構成非退化三角形；u=B−A=(4,2)、v=C−A=(−1,2) 的內積為 0，所以 θ_A=π/2=90°，ABC 是直角三角形，直角在 A，斜邊是 BC，股是 AB 與 AC。B、C 處的內積為 20、5，不是直角；任何非退化三角形至多一個直角。三角形 ABD（D=(1,4)）三個內積為 6、14、3，沒有直角，不是直角三角形。


- 內角量值以 G2 的餘弦式定義；它與綜合幾何中角的量測一致這一點，本稿不證明。
- cos_facts、line_unique、angle_positive 是前提，未在本稿推導。
- N17（20+5=25）只是與畢氏定理一致的旁證，本稿論證不使用它。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 59d80db968e3384bccfcb59d56d000c022e245739089f60fee3f366ca873745c
- original source SHA-256: 59d80db968e3384bccfcb59d56d000c022e245739089f60fee3f366ca873745c
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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