# 點、線、面：在座標模型中判定點是否在直線上

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

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

derivation-mko-point-line-plane-01 · production-20261019-adopted-96



## 目標與範圍

在座標平面模型 ℝ² 中，設 P=(1,2)、Q=(3,6)。判定 R=(4,8) 與 S=(2,5) 是否在通過 P、Q 的直線 L 上，並據此判定 P、Q、R 是否共線。

只在一個明示的模型（ℝ² 的座標模型，直線以參數式定義）中判定入射關係，示範 MKO「線與面的精確性質由所選模型決定」這一點。不處理一般公理化幾何、平面或高維情形；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- cartesian_product_def
- image_preimage_def
- eq_congruence
- mul_inverse_nonzero
- numeric_evaluation


- G1 — 模型：點是 ℝ² 中的有序實數對；加法、減法與實數倍數逐坐標進行。
- G2 — 本模型的直線定義：對相異點 P≠Q，通過 P、Q 的直線是 L(P,Q)={P+t(Q−P) ∣ t∈ℝ}。
- G3 — P=(1,2)、Q=(3,6)、R=(4,8)、S=(2,5)。


- \mathbb{R}^2 — 有序實數對的集合；本稿的點
- P,Q,R,S — 四個給定點
- L(P,Q) — 通過相異點 P、Q 的直線
- t — 直線的實數參數
- Q-P — 方向向量，逐坐標相減





## 規則與來源


- 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 有反函數。
- 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 不定義。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- two_nonzero · prerequisite — 實數中 0<1，故 0<1+1=2，所以 2≠0。
- 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)。
- add_zero · prerequisite — 加法單位元：u+0=u。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- logic_chain · prerequisite — 推論的傳遞：由 P⇒Q 與 Q⇒R 得 P⇒R；⇔ 同理。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- 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)。
- collinear_def · prerequisite — 共線：若存在一條直線同時包含若干點，這些點稱為共線。
- L_solve_linear · lemma — 對實數 a、c 與 b≠0：c=a+bt ⇔ t=(c−a)/b。





## 逐步主鏈

S01 · definition操作前

\text{points and lines of the chosen model}

操作後

\text{point}\in\mathbb{R}^2,\ L(P,Q)=\{P+t(Q-P)\mid t\in\mathbb{R}\}\ (P\neq Q)

條件：無

規則：mko_model_dependence · 依賴：G1, G2

葉節點依據：mko_model_dependence

MKO 指出線的精確性質由所選模型決定，所以先固定模型：點是 ℝ² 的有序對，直線由 G2 的參數式定義。之後每一步的「在線上」都是指這個模型中的集合歸屬，而不是示意圖上的外觀。



S02 · implies操作前

P=(1,2),\ Q=(3,6)

操作後

P\neq Q

條件：無

規則：cartesian_product_def · 依賴：G3, cartesian_product_def

葉節點依據：cartesian_product_def + numeric_evaluation

兩個有序對相等必須兩個坐標都相等；P 與 Q 的第一坐標 1≠3，所以 P≠Q。這是 G2 的直線定義所要求的前提，L(P,Q) 因此確實是一條直線。



S03 · equivalent操作前

Q-P

操作後

(2,4)

條件：無

規則：coord_ops · 依賴：G1, G3

葉節點依據：coord_ops + numeric_evaluation

逐坐標相減：Q−P=(3−1, 6−2)=(2,4)。左右兩邊是同一個有序對，這是等值代換。



S04 · equivalent操作前

L(P,Q)=\{P+t(Q-P)\mid t\in\mathbb{R}\}

操作後

L=\{(1+2t,\,2+4t)\mid t\in\mathbb{R}\}

條件：P\neq Q

規則：coord_ops · 依賴：S01, S02, S03, G3

葉節點依據：coord_ops + eq_replace

代入 P=(1,2) 與 Q−P=(2,4)：P+t(Q−P)=(1,2)+(2t,4t)=(1+2t, 2+4t)。對每個 t，兩種寫法是同一點，所以兩個集合相同。條件 P≠Q 已在 S02 確認。



S05 · equivalent操作前

R\in L

操作後

\exists t\in\mathbb{R}:\ (4,8)=(1+2t,\,2+4t)

條件：無

規則：image_preimage_def · 依賴：S04, G3

葉節點依據：image_preimage_def + def_unfold

L 是參數 t 走遍 ℝ 時得到的點的集合（函數 t↦(1+2t,2+4t) 的像）。所以 R 屬於 L，恰好表示有某個實數 t 使 R 等於 (1+2t, 2+4t)。



S06 · equivalent操作前

(4,8)=(1+2t,\,2+4t)

操作後

4=1+2t\ \land\ 8=2+4t

條件：無

規則：cartesian_product_def · 依賴：S05, cartesian_product_def

葉節點依據：cartesian_product_def

有序對相等當且僅當兩個坐標分別相等，所以一個點的方程拆成兩個實數方程，而且兩個方程用的是同一個 t。



S07 · equivalent操作前

4=1+2t

操作後

t=\tfrac{3}{2}

條件：2\neq 0

規則：L_solve_linear · 依賴：S06

葉節點依據：eq_congruence + mul_inverse_nonzero + two_nonzero

依引理 L_solve_linear（a=1、b=2、c=4）：4=1+2t ⇔ t=(4−1)/2=3/2。除以 2 需要 2≠0。



S08 · equivalent操作前

8=2+4t

操作後

t=\tfrac{3}{2}

條件：4\neq 0

規則：L_solve_linear · 依賴：S06

葉節點依據：eq_congruence + mul_inverse_nonzero + numeric_evaluation

同一引理（a=2、b=4、c=8）：8=2+4t ⇔ t=(8−2)/4=6/4=3/2；這裡 4≠0。



S09 · implies操作前

4=1+2t\ \land\ 8=2+4t

操作後

R\in L

條件：無

規則：exists_intro · 依賴：S05, S06, S07, S08

葉節點依據：exists_intro + and_intro_elim + logic_chain

兩個方程都恰好由 t=3/2 滿足，所以同一個 t=3/2 同時滿足兩者。依 S05、S06 的等價，R∈L，而且 R=P+(3/2)(Q−P)。



S10 · equivalent操作前

S\in L

操作後

\exists t\in\mathbb{R}:\ 2=1+2t\ \land\ 5=2+4t

條件：無

規則：image_preimage_def · 依賴：S04, G3

葉節點依據：image_preimage_def + cartesian_product_def

對 S 重複 S05、S06 的兩個展開：S∈L 當且僅當有某個 t 同時滿足兩個坐標方程 2=1+2t 與 5=2+4t。



S11 · equivalent操作前

2=1+2t\ \land\ 5=2+4t

操作後

t=\tfrac{1}{2}\ \land\ t=\tfrac{3}{4}

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

規則：L_solve_linear · 依賴：S10

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

分別解兩個方程：2=1+2t ⇔ t=1/2；5=2+4t ⇔ t=3/4。每個方程各自等價變形，所以合取前後同真同假。



S12 · implies操作前

\exists t:\ t=\tfrac{1}{2}\ \land\ t=\tfrac{3}{4}

操作後

S\notin L

條件：無

規則：contradiction · 依賴：S10, S11

葉節點依據：contradiction + eq_refl_symm_trans + numeric_evaluation

若有 t 同時等於 1/2 與 3/4，依等號的對稱與傳遞得 1/2=3/4，但 1/2≠3/4。所以不存在這樣的 t；依 S10 的等價，S∉L。



S13 · implies操作前

t=0,\ t=1

操作後

P\in L,\ Q\in L

條件：無

規則：image_preimage_def · 依賴：S04, G3

葉節點依據：image_preimage_def + coord_ops + numeric_evaluation

取 t=0 得 (1+0, 2+0)=(1,2)=P；取 t=1 得 (1+2, 2+4)=(3,6)=Q。所以 L 確實通過兩個給定點。



S14 · implies操作前

P,Q,R\in L,\ S\notin L

操作後

P,Q,R\ \text{collinear};\ S\notin L(P,Q)

條件：無

規則：collinear_def · 依賴：S09, S12, S13

葉節點依據：collinear_def + and_intro_elim

L 同時包含 P、Q、R，依共線定義三點共線；S 不在 L 上。兩個結論都只在本模型中成立。







## 局部子步與引理

S07.1 · equivalent操作前

c=a+bt

操作後

c-a=bt

條件：無

規則：eq_congruence · 依賴：eq_congruence

葉節點依據：eq_congruence + add_assoc + add_comm + add_inverse + add_zero

兩邊同減 a：(a+bt)−a=bt（加法結合律、交換律與反元素）。反向是兩邊同加 a。



S07.2 · equivalent操作前

c-a=bt

操作後

t=\frac{c-a}{b}

條件：b\neq 0

規則：mul_inverse_nonzero · 依賴：S07.1, mul_inverse_nonzero

葉節點依據：eq_congruence + mul_inverse_nonzero + mul_assoc + mul_comm + mul_one

因 b≠0，1/b 存在；兩邊同乘 1/b 得 (c−a)/b=t。反向是兩邊同乘 b。若 b=0，1/b 不存在，這一步不能做。S07.1 與 S07.2 合起來證得引理 L_solve_linear。







## 逐步反向審查


- S14 · sufficient_goal_reduction · S09, S12, S13, collinear_def — 目標 G：P、Q、R 共線且 S∉L(P,Q)。足夠條件 H 是兩件事的合取：L 同時含 P、Q、R，且 S∉L。前一項由 S09、S13 得到，後一項由 S12 得到；共線定義加合取引入給出 H⇒G。沒有把 G 當作前提。
- S13 · premise_audit · S04, image_preimage_def — 每個點只需找到一個參數值；這一步不宣稱參數值唯一。
- S12 · premise_audit · S10, S11, contradiction — 矛盾來自「同一個 t 要同時滿足兩個方程」；每個方程單獨都有解，所以不能只看其中一個坐標。
- S11 · inverse_equivalence · L_solve_linear — 代回 1+2·(1/2)=2、2+4·(3/4)=5；兩個等價各自雙向。
- S10 · inverse_equivalence · image_preimage_def, cartesian_product_def — 與 S05、S06 同理，兩個展開都是雙向的。
- S09 · premise_audit · S05, S07, S08, exists_intro — 需要的是「同一個 t」：S07 與 S08 給出相同的值，存在性才成立。只有一個方程有解並不夠。
- S08 · inverse_equivalence · L_solve_linear — 代回 2+4·(3/2)=8；兩個方向都由引理保證。
- S07.2 · inverse_equivalence · mul_inverse_nonzero, eq_congruence — 乘 1/b 與乘 b 互為反運算，前提 b≠0；這正是引理的條件。
- S07.1 · inverse_equivalence · eq_congruence, add_inverse — 減 a 與加 a 互為反運算，對任何實數 a 都可做，沒有附加條件。
- S07 · inverse_equivalence · L_solve_linear — 代回 1+2·(3/2)=4；兩個方向都由引理保證。
- S06 · inverse_equivalence · cartesian_product_def — 有序對的相等條件本身是雙向的；拆開後兩個方程不能各自使用不同的 t。
- S05 · inverse_equivalence · image_preimage_def — 這是像集合的展開：找到這樣的 t 就推出 R∈L，R∈L 也必有這樣的 t，雙向成立。
- S04 · inverse_equivalence · S02, S03, coord_ops — 每個 t 在兩種寫法中給出同一點，集合逐元素相同，雙向成立。
- S03 · inverse_equivalence · coord_ops, numeric_evaluation — 反向：P+(2,4)=(1+2, 2+4)=(3,6)=Q，還原了 Q−P=(2,4)；兩式表示同一個點。
- S02 · premise_audit · G3, cartesian_product_def — 一個坐標不同就足以推出兩點不等；反向（兩點不等推出某個指定坐標不等）並未宣稱。
- S01 · premise_audit · G1, G2, mko_model_dependence — 此步只選定並寫出模型，不推出新事實；之後所有結論只在這個模型中成立。





## 錯誤控制與反例

看起來在線上不等於在線上在示意圖上 S=(2,5) 很靠近 L：x=2 時 L 上的點是 (2,4)，只差 1。MKO 提醒不要把圖的外觀當成定義。本稿的判定完全由模型中的方程決定：S 的兩個坐標方程沒有共同解，所以 S∉L，不論圖上看起來多接近。

只核一個坐標不夠S 的第一個坐標方程 2=1+2t 有解 t=1/2，單看它會誤以為 S 在線上。但 t=1/2 代入第二坐標得 2+4·(1/2)=4≠5。入射需要同一個 t 同時滿足兩個坐標方程（S06 與 S12）。

為什麼先確認 P≠Q若 P=Q，Q−P=(0,0)，集合 {P+t·(0,0) ∣ t∈ℝ} 只有一個點 P，不是直線。G2 的定義只對相異兩點給出直線，所以 S02 必須先確認 P≠Q，S04 才能把 L 當作直線使用。


- S 在圖上看起來很接近直線，所以 S 在 L 上 → reject — 入射由方程決定；S 的兩個坐標方程要求 t=1/2 與 t=3/4，沒有共同解。
- 由 2=1+2t 得 t=1/2，所以 S∈L → reject — 第二坐標不成立：2+4·(1/2)=4≠5。
- 任意兩點 P、Q（包括 P=Q）都決定一條直線 {P+t(Q−P)} → reject — P=Q 時這個集合只有一點 P。
- 在任何幾何模型中，三點是否共線都可用這組座標方程判定 → reject — 這組方程屬於 ℝ² 的座標模型；MKO 指出線的性質由所選模型決定，換了模型（例如球面幾何）直線的定義也不同。





## 結論與限制

在 ℝ² 座標模型中，R=(4,8) 在通過 P、Q 的直線上（t=3/2），所以 P、Q、R 共線；S=(2,5) 不在這條直線上，因為兩個坐標方程要求 t=1/2 與 t=3/4，互相矛盾。


- 本稿不證明「通過兩相異點的直線唯一」，所以只宣稱 S∉L(P,Q)，不宣稱 P、Q、S 不在任何一條直線上。
- N8、N9 是以行列式形式做的獨立交叉核對，只對這組數字有效，本稿的論證不依賴它們。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: acf8e1534a6a5a0b508ab339ff6a480eccfed9de9c617ae4b40a60230ec65bfc
- original source SHA-256: fe3365f185ad4359da5ff93616296d2ba284d6ea11f6bb9927b953ceefeb6905
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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