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

目標與範圍

在座標平面模型 ℝ² 中，設 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。

逐步主鏈

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

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

90^\circ

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

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

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

C\in L(A,B)

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

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

C\notin L(A,B)

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

\triangle ABC\ \text{nondegenerate}

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

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

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

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

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

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

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

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

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

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

\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}

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

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

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

\triangle ABD\ \text{nondegenerate}

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

\text{S09, S12, S13, S15}

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

局部子步與引理

\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

逐步反向審查

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