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

目標與範圍

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

逐步主鏈

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

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

P\neq Q

Q-P

(2,4)

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

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

R\in L

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

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

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

4=1+2t

t=\tfrac{3}{2}

8=2+4t

t=\tfrac{3}{2}

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

R\in L

S\in L

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

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

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

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

S\notin L

t=0,\ t=1

P\in L,\ Q\in L

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

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

局部子步與引理

c=a+bt

c-a=bt

c-a=bt

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

逐步反向審查

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