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

目標與範圍

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

逐步主鏈

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

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

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

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

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

C\in L(A,B)

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

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

C\notin L(A,B)

A,B,C\ \text{collinear}

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

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

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

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

A,B,C\ \text{noncollinear}

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

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

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

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

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

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

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

A\notin[B,C]

G\in\triangle ABC

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

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

G\notin\triangle ABC

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

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

\text{S09, S10, S14, S15}

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

局部子步與引理

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

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

X+t(Y-X)

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

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)

P+t(Q-P)

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

0\le t\le 1

[P,Q]=[Q,P]

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

G\notin[A,B]

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

G\notin[B,C]

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

G\notin[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、反控制與修訂記錄）