# 三角形：在座標模型中確認三點界定非退化三角形

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

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

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



## 目標與範圍

在座標平面模型 ℝ² 中，設 A=(0,0)、B=(4,0)、C=(1,3)。確認 A、B、C 兩兩相異且不共線，因而依 MKO 界定非退化三角形 ABC；寫出三條邊與各頂點的對邊，並說明三頂點的平均點 G=(5/3,1) 不在三角形 ABC 上。另設 D=(2,1)、E=(6,3)，說明相異三點 A、D、E 共線，不界定非退化三角形。

只在 ℝ² 的座標模型中工作（直線與線段以參數式定義），處理 MKO 所建立的頂點、邊、對邊與非退化條件。不處理按邊或角的分類、內角和、面積、全等與相似（MKO 指出這些需要額外資料與定理）；不由綜合幾何公理推導座標模型；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- cartesian_product_def
- image_preimage_def
- set_operations_def
- eq_congruence
- numeric_evaluation


- G1 — 模型：點是 ℝ² 中的有序實數對，加法、減法與實數倍數逐坐標進行。對相異點 P≠Q，直線 L(P,Q)={P+t(Q−P) ∣ t∈ℝ}；模型中的直線恰好是這些集合。對任意點 P、Q，線段 [P,Q]={P+t(Q−P) ∣ 0≤t≤1}。
- G2 — 共線：若模型中有一條直線同時包含若干點，這些點稱為共線。
- G3 — A=(0,0)、B=(4,0)、C=(1,3)、G=(5/3,1)；D=(2,1)、E=(6,3)。


- A,B,C — 三角形的三個頂點
- L(P,Q) — 通過相異點 P、Q 的直線
- [P,Q] — 以 P、Q 為端點的線段
- \triangle ABC — 三條邊的聯集 [A,B]∪[B,C]∪[C,A]
- t,s,u,r — 實數參數
- G — 三個頂點的平均點 (5/3,1)





## 規則與來源


- 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 有反函數。
- set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- 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。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- imp_intro · prerequisite — →引入（釋放假設）：若在暫時假設 P 的作用域中推出 Q，則得到 P⇒Q；此後 P 不再可當作已知使用。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- 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。
- de_morgan_logic · prerequisite — 邏輯的德摩根律：¬(P∧Q) ⇔ ¬P∨¬Q；¬(P∨Q) ⇔ ¬P∧¬Q。
- mko_triangle_def · cited — 給定平面中三個相異且不共線的點 A、B、C，線段 AB、BC、CA 的聯合界定非退化三角形 ABC。 · mko-triangle
- mko_model_dependence · cited — 在指定的幾何模型中，點表示位置；線與面是承載點並具有相應維度的幾何對象，其精確性質由該模型的公理與結構決定。 · mko-point-line-plane
- coord_ops · prerequisite — 逐坐標運算：(a,b)+(c,d)=(a+c,b+d)，(a,b)−(c,d)=(a−c,b−d)，t(a,b)=(ta,tb)。
- line_def · prerequisite — 本模型的直線：對相異點 P≠Q，L(P,Q)={P+t(Q−P) ∣ t∈ℝ}；模型中的每一條直線都是某個這樣的 L(P,Q)。
- segment_def · prerequisite — 線段：對點 P、Q，[P,Q]={P+t(Q−P) ∣ 0≤t≤1}；P、Q 是它的端點。
- collinear_def · prerequisite — 共線：若存在一條直線同時包含若干點，這些點稱為共線。
- L_line_unique · lemma — 若 P≠Q，且 X、Y 是 L(P,Q) 上的相異兩點，則 L(X,Y)=L(P,Q)。
- L_seg_reverse · lemma — 對任意點 P、Q：[P,Q]=[Q,P]。





## 逐步主鏈

S01 · definition操作前

\text{three points }A,B,C\text{ of the model}

操作後

\triangle ABC=[A,B]\cup[B,C]\cup[C,A]\ \text{when}\ A,B,C\ \text{are distinct and noncollinear}

條件：無

規則：mko_triangle_def · 依賴：G1, G2, mko_model_dependence

葉節點依據：mko_triangle_def + mko_model_dependence

MKO 的定義有兩個前提：三點相異，且不共線；在這兩個前提下，三條線段的聯集就是非退化三角形 ABC。線、線段與共線的精確意義取決於所選模型，所以先固定 ℝ² 的座標模型（G1、G2）。之後的工作是逐一核對兩個前提，再寫出聯集。



S02 · implies操作前

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

操作後

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

條件：無

規則：cartesian_product_def · 依賴：G3, cartesian_product_def

葉節點依據：cartesian_product_def + numeric_evaluation

有序對相等必須兩個坐標都相等。A 與 B 的第一坐標 0≠4，B 與 C 的第一坐標 4≠1，C 與 A 的第一坐標 1≠0，所以三點兩兩相異。這是 MKO 的第一個前提，也提供了 G1 中 L(A,B) 有定義所需的 A≠B。



S03 · equivalent操作前

L(A,B)=\{A+t(B-A)\mid t\in\mathbb{R}\}

操作後

L(A,B)=\{(4t,\,0)\mid t\in\mathbb{R}\}

條件：A\neq B

規則：coord_ops · 依賴：G1, G3, S02

葉節點依據：coord_ops + mul_zero + add_zero

逐坐標計算：B−A=(4−0, 0−0)=(4,0)，所以 A+t(B−A)=(0+4t, 0+0·t)=(4t,0)。對每個 t 兩種寫法是同一點，所以兩個集合相同。條件 A≠B 已在 S02 確認。



S04 · equivalent操作前

C\in L(A,B)

操作後

\exists t\in\mathbb{R}:\ 1=4t\ \land\ 3=0

條件：無

規則：image_preimage_def · 依賴：S03, G3

葉節點依據：image_preimage_def + cartesian_product_def

L(A,B) 是 t↦(4t,0) 的像，所以 C∈L(A,B) 恰好表示有某個實數 t 使 (1,3)=(4t,0)；有序對相等拆成兩個坐標方程 1=4t 與 3=0，兩個方程用同一個 t。



S05 · implies操作前

\exists t\in\mathbb{R}:\ 1=4t\ \land\ 3=0

操作後

C\notin L(A,B)

條件：無

規則：contradiction · 依賴：S04

葉節點依據：contradiction + quantifier_negation + numeric_evaluation

第二個方程 3=0 不含 t，對每個 t 都不成立，所以合取對每個 t 都不成立，不存在這樣的 t；依 S04 的等價，C∉L(A,B)。注意第一個方程單獨有解 t=1/4，只看第一坐標會誤判。



S06 · equivalent操作前

A,B,C\ \text{collinear}

操作後

\exists P,Q,\ P\neq Q:\ A,B,C\in L(P,Q)

條件：無

規則：collinear_def · 依賴：G1, G2

葉節點依據：collinear_def + line_def + def_unfold

依 G2，三點共線表示有一條直線同時包含三點；依 G1，模型中的直線恰好是相異兩點 P、Q 給出的 L(P,Q)。兩個定義合起來就是右式。下一步暫時假設三點共線，看會推出什麼。



S07 · implies操作前

A,B,C\in L(P,Q),\ P\neq Q,\ A\neq B

操作後

L(P,Q)=L(A,B),\ C\in L(A,B)

條件：P\neq Q; A\neq B

規則：L_line_unique · 依賴：S02, S06, L_line_unique

葉節點依據：L_line_unique + exists_elim + eq_replace

假設 A、B、C 共線；依 S06 取 P≠Q 使 A、B、C∈L(P,Q)（∃消去，P、Q 是新名字）。A、B 是 L(P,Q) 上的兩點且 A≠B（S02），由引理 L_line_unique（X=A、Y=B）得 L(P,Q)=L(A,B)。於是 C∈L(P,Q) 推出 C∈L(A,B)。引理在 S07.1 到 S07.3 證明。



S08 · implies操作前

C\in L(A,B)\ \text{(under the assumption)},\ C\notin L(A,B)

操作後

A,B,C\ \text{noncollinear}

條件：無

規則：contradiction · 依賴：S05, S07

葉節點依據：contradiction + imp_intro

共線的假設推出 C∈L(A,B)（S07），但 S05 已證 C∉L(A,B)，矛盾。依反證法，假設不成立：沒有任何直線同時包含 A、B、C，即三點不共線。這是 MKO 的第二個前提。



S09 · theorem_application操作前

A,B,C\ \text{distinct and noncollinear}

操作後

\triangle ABC=[A,B]\cup[B,C]\cup[C,A]\ \text{nondegenerate}

條件：A\neq B,\ B\neq C,\ C\neq A; A,B,C\ \text{noncollinear}

規則：mko_triangle_def · 依賴：S02, S08, mko_triangle_def

葉節點依據：mko_triangle_def + and_intro_elim

兩個前提都已成立（S02、S08），依 MKO，三條線段的聯集界定非退化三角形 ABC。頂點是 A、B、C 三個點；邊是 [A,B]、[B,C]、[C,A] 三條線段。每個頂點的對邊是不以它為端點的那條邊：A 的對邊是 BC，B 的對邊是 CA，C 的對邊是 AB。



S10 · equivalent操作前

[A,B],\ [B,C],\ [C,A]

操作後

\{(4t,0)\},\ \{(4-3t,\,3t)\},\ \{(1-t,\,3-3t)\}\quad(0\le t\le 1)

條件：無

規則：segment_def · 依賴：S09, G1, G3

葉節點依據：segment_def + coord_ops + numeric_evaluation

依線段定義與逐坐標運算：B−A=(4,0)，[A,B]={(4t,0)}；C−B=(1−4, 3−0)=(−3,3)，[B,C]={(4−3t, 3t)}；A−C=(0−1, 0−3)=(−1,−3)，[C,A]={(1−t, 3−3t)}；三者都取 0≤t≤1。



S11 · equivalent操作前

\triangle ACB=[A,C]\cup[C,B]\cup[B,A]

操作後

[C,A]\cup[B,C]\cup[A,B]=\triangle ABC

條件：無

規則：L_seg_reverse · 依賴：S09, L_seg_reverse

葉節點依據：L_seg_reverse + set_operations_def + set_extensionality

改變頂點順序只改變名稱：依引理 L_seg_reverse，[A,C]=[C,A]、[C,B]=[B,C]、[B,A]=[A,B]；聯集與次序無關，所以 ACB 與 ABC 是同一個集合。引理在 S11.1、S11.2 證明。



S12 · implies操作前

A=(4-3t,\,3t),\ 0\le t\le 1

操作後

A\notin[B,C]

條件：無

規則：contradiction · 依賴：S10, G3

葉節點依據：contradiction + cartesian_product_def + numeric_evaluation

若 A∈[B,C]，則某個 t 使 (0,0)=(4−3t, 3t)。第二坐標 0=3t 給出 t=0，代入第一坐標得 4−3·0=4≠0，矛盾。所以頂點 A 不在它的對邊 BC 上。一般理由：[B,C]⊆L(B,C)，而 A∈L(B,C) 會使三點共線，與 S08 矛盾。



S13 · equivalent操作前

G\in\triangle ABC

操作後

G\in[A,B]\ \lor\ G\in[B,C]\ \lor\ G\in[C,A]

條件：無

規則：set_operations_def · 依賴：S09, G3

葉節點依據：set_operations_def + def_unfold

G=((0+4+1)/3, (0+0+3)/3)=(5/3,1) 是三個頂點的平均。依 MKO，三角形 ABC 是三條邊的聯集，所以 G 在三角形上恰好表示 G 至少在其中一條邊上。以下三個子步逐邊檢查。



S14 · implies操作前

G\notin[A,B],\ G\notin[B,C],\ G\notin[C,A]

操作後

G\notin\triangle ABC

條件：無

規則：de_morgan_logic · 依賴：S13, S13.1, S13.2, S13.3

葉節點依據：de_morgan_logic + set_operations_def

三個析取項都不成立，依德摩根律析取為假；依 S13 的等價，G∉△ABC。示意圖上 G 位於三角形圍住的區域內，但 MKO 所說的三角形是三條邊的聯集，不包含內部點。相對地，M=(2,0)=(4·(1/2),0) 在 [A,B] 上，所以 M∈△ABC。



S15 · implies操作前

A=(0,0),\ D=(2,1),\ E=(6,3)

操作後

A,D,E\in L(A,D)

條件：A\neq D

規則：collinear_def · 依賴：G1, G2, G3

葉節點依據：collinear_def + exists_intro + coord_ops + numeric_evaluation

A≠D（第一坐標 0≠2），所以 L(A,D) 有定義；D−A=(2,1)。t=0 給出 A，t=1 給出 D，t=3 給出 A+3(D−A)=(6,3)=E。三點都在同一條直線 L(A,D) 上，依 G2 共線。三點也兩兩相異（E 的第一坐標 6 與 0、2 都不同）。



S16 · implies操作前

\text{S09, S10, S14, S15}

操作後

\triangle ABC\ \text{nondegenerate};\ A,D,E\ \text{give no nondegenerate triangle}

條件：無

規則：mko_triangle_def · 依賴：S09, S10, S12, S14, S15

葉節點依據：mko_triangle_def + and_intro_elim

A、B、C 相異且不共線，界定非退化三角形 ABC，三邊如 S10，對邊關係如 S09，且 G 不在三角形上。A、D、E 雖然相異，卻共線，違反 MKO 的第二個前提，所以不界定本條目所指的非退化三角形。







## 局部子步與引理

S07.1 · implies操作前

X,Y\in L(P,Q),\ X\neq Y,\ D=Q-P

操作後

X=P+sD,\ Y=P+uD,\ s\neq u

條件：無

規則：exists_elim · 依賴：G1

葉節點依據：exists_elim + contrapositive + eq_replace

X∈L(P,Q) 給出某個實數 s 使 X=P+sD；Y∈L(P,Q) 給出某個實數 u 使 Y=P+uD（∃消去，s、u 是新名字）。若 s=u，則 X=P+sD=P+uD=Y，與 X≠Y 矛盾；所以 s≠u。



S07.2 · equivalent操作前

X+t(Y-X)

操作後

P+\bigl(s+t(u-s)\bigr)D

條件：無

規則：distributive · 依賴：S07.1

葉節點依據：distributive + add_assoc + add_comm + mul_comm + coord_ops

先算 Y−X=(P+uD)−(P+sD)=(u−s)D；再代入 X+t(Y−X)=P+sD+t(u−s)D=P+(s+t(u−s))D。每個坐標都只用到加法與乘法的結合律、交換律與分配律，所以對每個實數 t 成立（N14 以多項式恆等式核對）。



S07.3 · implies操作前

L(X,Y)=\{P+(s+t(u-s))D\mid t\in\mathbb{R}\}

操作後

L(X,Y)=\{P+rD\mid r\in\mathbb{R}\}=L(P,Q)

條件：u-s\neq 0

規則：set_extensionality · 依賴：S07.1, S07.2

葉節點依據：set_extensionality + subset_def + mul_inverse_nonzero + exists_intro

⊆：每個 s+t(u−s) 都是實數 r，所以 L(X,Y) 的每一點都在 L(P,Q) 中。⊇：給定實數 r，取 t=(r−s)/(u−s)，因 u−s≠0 這個 t 有定義，且 s+t(u−s)=r，所以 P+rD∈L(X,Y)。兩個包含合起來得集合相等。S07.1 到 S07.3 合起來證得引理 L_line_unique。



S11.1 · equivalent操作前

P+t(Q-P)

操作後

Q+(1-t)(P-Q)

條件：無

規則：distributive · 依賴：G1

葉節點依據：distributive + add_inverse + add_comm + add_assoc + coord_ops

展開右式：Q+(1−t)(P−Q)=Q+P−Q−tP+tQ=P+t(Q−P)。每個坐標都是實數的多項式恆等式，對所有 t、P、Q 成立（N15）。



S11.2 · implies操作前

0\le t\le 1

操作後

[P,Q]=[Q,P]

條件：無

規則：set_extensionality · 依賴：S11.1

葉節點依據：order_basics + set_extensionality + subset_def

0≤t≤1 ⇔ 0≤1−t≤1（乘以 −1 使不等號反向，再加 1）。所以 t 走遍 [0,1] 時，1−t 也恰好走遍 [0,1]；配合 S11.1，[P,Q] 的每一點都是 [Q,P] 的點，反之亦然。S11.1 與 S11.2 合起來證得引理 L_seg_reverse。



S13.1 · implies操作前

(5/3,\,1)=(4t,\,0)

操作後

G\notin[A,B]

條件：無

規則：contradiction · 依賴：S10

葉節點依據：cartesian_product_def + contradiction

[A,B] 上每一點的第二坐標都是 0，G 的第二坐標是 1，而 1≠0，所以 G∉[A,B]。



S13.2 · implies操作前

(5/3,\,1)=(4-3t,\,3t)

操作後

G\notin[B,C]

條件：無

規則：contradiction · 依賴：S10

葉節點依據：eq_congruence + mul_inverse_nonzero + contradiction + numeric_evaluation

第二坐標 1=3t ⇔ t=1/3（3≠0）；代入第一坐標得 4−3·(1/3)=3，而 3≠5/3，所以沒有 t 同時滿足兩式，G∉[B,C]。



S13.3 · implies操作前

(5/3,\,1)=(1-t,\,3-3t)

操作後

G\notin[C,A]

條件：無

規則：contradiction · 依賴：S10

葉節點依據：eq_congruence + mul_inverse_nonzero + contradiction + numeric_evaluation

第二坐標 1=3−3t ⇔ t=(3−1)/3=2/3；代入第一坐標得 1−2/3=1/3，而 1/3≠5/3，所以 G∉[C,A]。







## 逐步反向審查


- S16 · sufficient_goal_reduction · S02, S08, S09, S14, S15, mko_triangle_def — 目標：ABC 是非退化三角形，而 A、D、E 不界定非退化三角形。足夠條件 H：A、B、C 相異（S02）且不共線（S08），而 A、D、E 共線（S15）；H 推出目標由 MKO 的定義。H 由 S02 到 S15 從已知正向證成，沒有把目標當作前提。
- S15 · premise_audit · G2, collinear_def, exists_intro — 共線只需找到一條包含三點的直線，各點各給一個參數值即可；不需要唯一性。
- S14 · premise_audit · S13, S13.1, S13.2, S13.3, de_morgan_logic — 要證不在聯集中，三條邊都必須排除；只排除一條不夠。
- S13.3 · premise_audit · S10, contradiction, mul_inverse_nonzero — 與 S13.2 相同：第二坐標決定 t，再看第一坐標是否吻合。
- S13.2 · premise_audit · S10, contradiction, mul_inverse_nonzero — 第二坐標唯一決定 t；兩個坐標必須用同一個 t。
- S13.1 · premise_audit · S10, cartesian_product_def — 一個坐標不等就足以排除；不需解第一坐標。
- S13 · inverse_equivalence · set_operations_def, S09 — 聯集的成員條件是雙向的。
- S12 · premise_audit · S10, contradiction — 第二坐標唯一決定 t=0；只需檢查這個 t 是否也滿足第一坐標。
- S11.2 · premise_audit · S11.1, order_basics, set_extensionality — 此證明需要所用參數範圍在 t↦1−t 下不變；[0,1] 確實如此。換成 [0,2] 時不再不變，但不能由「不是 [0,1]」一概判定失敗，例如 [1/4,3/4] 也不變。本稿的線段仍依既定 [0,1] 定義。
- S11.1 · inverse_equivalence · distributive, add_inverse — 恆等式，雙向成立。
- S11 · inverse_equivalence · L_seg_reverse, set_operations_def — 每個替換都是集合相等，重排聯集也是相等，雙向成立。
- S10 · inverse_equivalence · segment_def, coord_ops — 反向核對端點：t=0 與 t=1 分別給出 A 與 B；B 與 C=(4−3,3)=(1,3)；C 與 A=(1−1,3−3)=(0,0)。每個 t 兩種寫法是同一點。
- S09 · premise_audit · S02, S08, mko_triangle_def — MKO 的兩個前提缺一不可；這裡不宣稱三角形的任何長度、角度或面積性質。
- S08 · premise_audit · S05, S07, contradiction — 反證需要一個命題與其否定同時成立：C∈L(A,B) 與 C∉L(A,B)。只有 C∉L(A,B) 還不夠；必須靠 S07 的唯一性才能排除其他直線。
- S07.3 · premise_audit · S07.1, set_extensionality, mul_inverse_nonzero — ⊇ 方向要除以 u−s，正需要 S07.1 的 s≠u。若 s=u，集合只剩一點 P+sD，不是直線。
- S07.2 · inverse_equivalence · distributive, coord_ops — 兩式對每個 t 給出同一點，是恆等式，雙向成立。
- S07.1 · premise_audit · exists_elim, contrapositive — s≠u 由 X≠Y 的逆否得出；反向（s≠u 推出 X≠Y）需要 D≠0，這裡不需要也不宣稱。
- S07 · premise_audit · S02, S06, L_line_unique, exists_elim — 引理需要 A≠B；若 A=B，通過 A 的直線有很多條，推不出 L(P,Q)=L(A,B)。此步在共線假設之下，結論是條件式，不宣稱 C∈L(A,B) 真的成立。
- S06 · inverse_equivalence · collinear_def, line_def — 只是展開兩個定義，雙向成立。
- S05 · premise_audit · S04, contradiction, quantifier_negation — 結論只需「沒有任何 t 同時滿足兩式」；3≠0 與 t 無關，所以存在命題為假。
- S04 · inverse_equivalence · image_preimage_def, cartesian_product_def — 像集合的展開與有序對相等的條件都是雙向的。
- S03 · inverse_equivalence · coord_ops, S02 — 反向：t=1 時 (4,0)=B，t=0 時 (0,0)=A；每個 t 在兩種寫法中給出同一點，雙向成立。
- S02 · premise_audit · G3, cartesian_product_def — 每一對只需一個不同的坐標；只檢查其中兩對不夠，三對都要檢查。反向（兩點不等推出某個指定坐標不等）並未宣稱。
- S01 · premise_audit · G1, G2, mko_triangle_def, mko_model_dependence — 此步只寫出定義與模型，不推出新事實；兩個前提尚未核對，還不能寫「ABC 是三角形」。





## 錯誤控制與反例

任三點不一定構成三角形MKO 指出常見誤解是以為任何三點都形成非退化三角形。A、D、E 兩兩相異，粗略的示意圖上也可能像一個很扁的三角形，但 E=A+3(D−A)，三點在同一直線上（S15）。若三點中有重合，例如 A、A、B，連「相異」都不成立。所以 S02 與 S08 兩個前提都必須明確核對，只說「有三個點」不夠。

頂點、邊與三角形本身頂點是點（例如 A），邊是線段（AB 指 [A,B]），兩者不能互換：說「頂點 AB」是把邊的名稱當成頂點。依 MKO，三角形 ABC 是三條邊的聯集：G=(5/3,1) 在圖上看起來「在三角形裡」，卻不在任何一條邊上（S13 到 S14），所以 G∉△ABC。

不從圖形比例猜邊長或角度MKO 提醒不要從畫圖比例猜性質。示意圖上 AC 與 BC 也許看起來差不多長，但另行計算長度平方，|AC|²=(−1)²+(−3)²=10、|BC|²=(−3)²+3²=18（N20、N21），兩者不同。這類長度與角度結論屬於其他 MKO，需要各自的定義與定理；本稿只建立頂點、邊與對邊。


- A、D、E 三點兩兩相異，所以界定一個非退化三角形 → reject — E=A+3(D−A)，三點共線（S15），違反不共線的前提。
- G=(5/3,1) 在三角形 ABC 上，因為它在三角形圍住的區域內 → reject — 依 MKO，三角形是三條邊的聯集；G 不在任何一條邊上（S13.1 到 S13.3）。
- AB 是三角形 ABC 的一個頂點 → reject — AB 是邊，即線段 [A,B]；頂點是 A、B、C 三個點。
- 1=4t 有解 t=1/4，所以 C 在直線 AB 上 → reject — 同一個 t 還須滿足第二坐標方程 3=0，對任何 t 都不成立（S05）。





## 結論與限制

A=(0,0)、B=(4,0)、C=(1,3) 兩兩相異且不共線，依 MKO 界定非退化三角形 ABC=[A,B]∪[B,C]∪[C,A]；三邊為 {(4t,0)}、{(4−3t,3t)}、{(1−t,3−3t)}（0≤t≤1），A、B、C 的對邊分別是 BC、CA、AB。三頂點的平均點 G=(5/3,1) 不在任何一條邊上，所以不在三角形上。A、D=(2,1)、E=(6,3) 相異但共線（E=A+3(D−A)），不界定非退化三角形。


- N18、N19 是行列式形式的獨立交叉核對，只對這組數字有效；本稿論證不依賴它們。
- 本稿只在 ℝ² 座標模型中工作；座標模型與綜合幾何公理系統之間的對應未在此處理。
- N20、N21 的長度平方只用於錯誤控制，屬於歐幾里得長度的 MKO，不屬於本稿論證。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 579b72812beece3e12baad63e611a795eb814972eceec9d3b1dd1abbe85ae559
- original source SHA-256: c4b2a9675620225c60a7ccfcc9072afda7b8e81861a9cd1a613e7b2b997c9dcc
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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