# 仿射函數與一次函數：由兩點求 m、b，判定次數、零點與是否為線性映射 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-linear-function/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-linear-function-01 · production-20261019-adopted-96 ## 目標與範圍 仿射函數 f:ℝ→ℝ，f(x)=mx+b 的圖形通過 (1,4) 與 (3,0)。求 m、b；判定 f 是否為次數一的函數、求它的零點，並判定 f 是否為線性代數意義下的 ℝ 線性映射。再證明兩個仿射函數在 ℝ 上相等當且僅當斜率與截距都相同，據此說明 f(2)=k(2)（k(x)=x）不能推出 f=k；最後處理 m=0 的兩個退化例子 g(x)=5 與 h(x)=0。 在 MKO 的範圍內：定義域與陪域都是 ℝ，m、b 是實常數。兩點斜率只在 x_1≠x_2 時使用；單點比較只主張該點的輸出相同。不討論多變數仿射映射或其他域；不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - distributive - eq_congruence - mul_inverse_nonzero - function_def - numeric_evaluation - G1 — f:ℝ→ℝ，f(x)=mx+b，m、b 為實常數（MKO 假設 a1）。m≠0 時稱次數一，m=0 時為常數函數；線性代數中的 ℝ 線性映射另要求可加性與齊次性。 - G2 — f 的圖形通過 (1,4) 與 (3,0)，即 f(1)=4、f(3)=0。 - G3 — 比較用的函數：k(x)=x、g(x)=0·x+5、h(x)=0·x+0，皆為 ℝ→ℝ。 - f(x)=mx+b — 仿射函數，m 為斜率、b 為截距 - (x_1,y_1),\ (x_2,y_2) — 圖形上的兩點 - k(x)=x — 比較用的函數 - g(x)=5,\ h(x)=0 — m=0 的兩個退化例子 ## 規則與來源 - distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。 - 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 不定義。 - function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。 - add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。 - add_comm · prerequisite — 加法交換律：u+v=v+u。 - add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。 - forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。 - eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。 - two_nonzero · prerequisite — 實數中 0<1，故 0<1+1=2，所以 2≠0。 - contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。 - mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。 - mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。 - iff_intro · prerequisite — 雙條件：P⇒Q 與 Q⇒P 都成立時，P⇔Q 成立；反之亦然。 - forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。 - case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - mko_affine · cited — 對 m、b∈R，f:R→R 由 f(x)=mx+b 定義為仿射函數。當 m≠0 時多項式次數為一；m=0 時為常數函數。線性代數中的 R 線性映射另要求 b=0，不能與初等教材的 linear function 稱呼混同。 · mko-linear-function - linear_map_def · prerequisite — T:ℝ→ℝ 是 ℝ 線性映射，指對所有實數 u、v、c 都有 T(u+v)=T(u)+T(v) 與 T(cu)=cT(u)。 - L_diff · lemma — 對仿射 f(x)=mx+b 與所有實數 x_1、x_2：f(x_2)−f(x_1)=m(x_2−x_1)。 - L_lin_zero · lemma — 每個 ℝ 線性映射 T 都有 T(0)=0。 - L_affine_eq · lemma — 對實數 m、b、n、c：（對所有 x∈ℝ，mx+b=nx+c）當且僅當（m=n 且 b=c）。 ## 逐步主鏈 S01 · definition操作前 f:\mathbb{R}\to\mathbb{R} 操作後 f(x)=mx+b;\ m\neq0\Rightarrow\deg f=1;\ m=0\Rightarrow f\ \text{constant} 條件：m,b\in\mathbb{R} 規則：mko_affine · 依賴：G1 葉節點依據：mko_affine + def_intro 依 MKO，所有 mx+b 形式的函數都是仿射函數；其中只有 m≠0 的稱為次數一，m=0 的是常數函數。線性代數的「線性映射」是另一個概念，要求可加性與齊次性（linear_map_def），MKO 指出它另需 b=0。三個名稱不可混用。 S02 · equivalent操作前 f(x_2)-f(x_1) 操作後 m(x_2-x_1) 條件：無 規則：L_diff · 依賴：S01 葉節點依據：distributive + add_inverse + add_comm 依引理 L_diff，仿射函數的輸出差等於斜率乘輸入差；截距 b 在相減時消去。證明在 S02.1。 S03 · theorem_application操作前 f(3)-f(1)=m(3-1) 操作後 0-4=2m,\ \text{i.e.}\ -4=2m 條件：x_1=1\neq 3=x_2 規則：forall_elim · 依賴：G2, S02 葉節點依據：forall_elim + eq_replace + numeric_evaluation 在 L_diff 中取 x_1=1、x_2=3，代入 f(1)=4、f(3)=0：0−4=m(3−1)，即 −4=2m。兩點的橫坐標不同（1≠3），所以 3−1=2≠0，下一步可以除。 S04 · equivalent操作前 -4=2m 操作後 m=\frac{-4}{2}=-2 條件：2\neq 0 規則：mul_inverse_nonzero · 依賴：S03, mul_inverse_nonzero 葉節點依據：mul_inverse_nonzero + eq_congruence + two_nonzero + numeric_evaluation 因 2≠0，兩邊同乘 1/2 得 m=−4/2=−2。這就是兩點斜率公式 m=(y_2−y_1)/(x_2−x_1)=(0−4)/(3−1)。 S05 · equivalent操作前 f(1)=4:\ -2\cdot 1+b=4 操作後 b=4+2=6 條件：無 規則：eq_congruence · 依賴：G2, S04 葉節點依據：eq_congruence + add_inverse + numeric_evaluation 把 m=−2 與 f(1)=4 代入 f(x)=mx+b：−2·1+b=4。兩邊同加 2 得 b=6。 S06 · implies操作前 m=-2,\ b=6 操作後 f(x)=-2x+6,\quad f(3)=-6+6=0 條件：無 規則：eq_replace · 依賴：S04, S05, G2 葉節點依據：eq_replace + numeric_evaluation 所以 f(x)=−2x+6。核對第二個點：f(3)=−2·3+6=0，與 G2 一致；f(1)=−2+6=4 也一致。S03 到 S05 每一步都是等價或由已知直接推出，所以通過這兩點的仿射函數只有這一個。 S07 · implies操作前 f(x)=-2x+6 操作後 b=f(0)=6,\quad f(x+1)-f(x)=m=-2 條件：無 規則：forall_elim · 依賴：S06, S02 葉節點依據：forall_elim + numeric_evaluation 依 MKO para0 的解讀：b=f(0)=−2·0+6=6；在 L_diff 中取 x_2=x_1+1，得 f(x+1)−f(x)=m·1=−2，即輸入每增加一單位，輸出減少 2。 S08 · implies操作前 m=-2 操作後 m\neq 0\Rightarrow f\ \text{has degree one} 條件：m\neq 0 規則：mko_affine · 依賴：S01, S04 葉節點依據：mko_affine + numeric_evaluation m=−2≠0，依 MKO，f 作為多項式的次數是一，是一次函數。若 m 為 0，即使寫成 mx+b 的形式也不是一次函數（見 S13）。 S09 · equivalent操作前 f(x)=0:\ -2x+6=0 操作後 x=\frac{-6}{-2}=3=-\frac{b}{m} 條件：m=-2\neq 0 規則：mul_inverse_nonzero · 依賴：S06, mul_inverse_nonzero 葉節點依據：mul_inverse_nonzero + eq_congruence + numeric_evaluation −2x+6=0 兩邊同減 6 得 −2x=−6；因 −2≠0，兩邊同乘 −1/2 得 x=3。每一步都是等價，所以零點唯一，就是 −b/m=−6/(−2)=3，與 G2 的點 (3,0) 一致。 S10 · implies操作前 f(0)=6 操作後 f\ \text{is not}\ \mathbb{R}\text{-linear} 條件：b=6\neq 0 規則：contrapositive · 依賴：S06, linear_map_def 葉節點依據：L_lin_zero + contrapositive + numeric_evaluation 依引理 L_lin_zero，每個 ℝ 線性映射都把 0 送到 0（證明在 S10.1）。f(0)=6≠0，依逆否命題，f 不是 ℝ 線性映射。直接也可看出可加性失敗：f(1+1)=f(2)=2，但 f(1)+f(1)=4+4=8。所以帶非零截距的仿射函數不是線性代數的線性映射。 S11 · equivalent操作前 \forall x\in\mathbb{R}:\ mx+b=nx+c 操作後 m=n\ \land\ b=c 條件：無 規則：L_affine_eq · 依賴：S01 葉節點依據：forall_elim + eq_congruence + iff_intro 依引理 L_affine_eq，兩個仿射函數在整個 ℝ 上相等，當且僅當斜率與截距都相同（MKO para2）。兩個方向分別在 S11.1、S11.2 證明。 S12 · implies操作前 f(2)=-4+6=2=k(2) 操作後 f\neq k\quad((-2,6)\neq(1,0)) 條件：無 規則：L_affine_eq · 依賴：S06, S11, G3 葉節點依據：L_affine_eq + contrapositive + numeric_evaluation f(2)=−2·2+6=2，k(2)=2，在輸入 2 的輸出相同，這只是單點事實（MKO 假設 a2）。f 的 (m,b)=(−2,6)，k 的 (m,b)=(1,0)，斜率不同，依 S11，f 與 k 在 ℝ 上不相等；例如 f(0)=6≠0=k(0)。 S13 · case_split操作前 g(x)=0x+5,\ h(x)=0x+0 操作後 g\ \text{has no zero};\ \text{every real is a zero of}\ h;\ \text{neither has degree one} 條件：m=0 規則：case_analysis · 依賴：G3, S01, linear_map_def 葉節點依據：case_analysis + mul_zero + linear_map_def m=0 時零點分兩種情形。g：對所有 x，g(x)=0·x+5=5≠0，沒有零點。h：對所有 x，h(x)=0，每個實數都是零點。兩者都是仿射（常數）函數，但 m=0，所以都不是次數一的函數。h 還滿足 h(u+v)=0=h(u)+h(v)、h(cu)=0=c·h(u)，是 ℝ 線性映射；g 因 g(0)=5≠0 不是。 S14 · implies操作前 f,\ k,\ g,\ h 操作後 f(x)=-2x+6:\ \deg 1,\ \text{zero}\ 3,\ \text{not linear};\ f\neq k;\ g,h\ \text{constant} 條件：無 規則：and_intro_elim · 依賴：S06, S08, S09, S10, S12, S13 葉節點依據：and_intro_elim 彙整：f(x)=−2x+6 是次數一的仿射函數，唯一零點 3，但不是 ℝ 線性映射；f 與 k 只在輸入 2 吻合，並不相等；g、h 是常數函數，g 無零點，h 處處為零。 ## 局部子步與引理 S02.1 · equivalent操作前 (mx_2+b)-(mx_1+b) 操作後 mx_2-mx_1=m(x_2-x_1) 條件：無 規則：distributive · 依賴：distributive, add_inverse 葉節點依據：distributive + add_inverse + add_comm + add_assoc 展開減法：(mx_2+b)−(mx_1+b)=mx_2+b−mx_1−b；b−b=0，剩下 mx_2−mx_1，依分配律提出 m 得 m(x_2−x_1)。這證得引理 L_diff。 S10.1 · implies操作前 T\ \mathbb{R}\text{-linear} 操作後 T(0)=T(0\cdot 0)=0\cdot T(0)=0 條件：無 規則：linear_map_def · 依賴：linear_map_def, mul_zero 葉節點依據：linear_map_def + mul_zero + mul_comm 0=0·0，依齊次性（c=0、u=0）T(0)=T(0·0)=0·T(0)，再依 u·0=0 得 0。這證得引理 L_lin_zero。 S11.1 · implies操作前 \forall x:\ mx+b=nx+c 操作後 b=c\ (x=0),\quad m+b=n+c\ (x=1)\ \Rightarrow\ m=n 條件：無 規則：forall_elim · 依賴：forall_elim, eq_congruence 葉節點依據：forall_elim + eq_congruence + add_inverse 等式對所有 x 成立，取 x=0 得 b=c；取 x=1 得 m+b=n+c，兩邊同減 b（=c）得 m=n。這是 ⇒ 方向。注意需要兩個不同的輸入；只知道一個點的等式不夠。 S11.2 · implies操作前 m=n\ \land\ b=c 操作後 \forall x:\ mx+b=nx+c 條件：無 規則：eq_replace · 依賴：eq_replace 葉節點依據：eq_replace + forall_intro 若 m=n 且 b=c，對任意 x 把 m 換成 n、b 換成 c，得 mx+b=nx+c；x 是任意的，依 forall_intro 對所有 x 成立。這是 ⇐ 方向。S11.1 與 S11.2 合起來證得引理 L_affine_eq。 ## 逐步反向審查 - S14 · sufficient_goal_reduction · S06, S08, S09, S10, S12, S13, and_intro_elim — 目標 G：各項結論。足夠條件 H：S06 至 S13 的各別結論；H⇒G 只是合取。H 由給定資料正向證成，沒有把 G 當作前提。 - S13 · premise_audit · S01, case_analysis, linear_map_def, mul_zero — m=0 的情形依 b 是否為零分成兩支，涵蓋全部可能；結論與 MKO para1 一致。 - S12 · premise_audit · S11, S06, numeric_evaluation — 用到 S11 中 ⇒ 方向的逆否：係數不同推出函數不同；單點的吻合（N9）不能推出全域相等。 - S11.2 · premise_audit · eq_replace, forall_intro — 等值代換對每個 x 都可做，沒有附加條件。 - S11.1 · premise_audit · forall_elim, eq_congruence — 前提是對所有 x 成立；若只在 x=2 成立，S12 顯示結論可以失敗。 - S11 · inverse_equivalence · L_affine_eq — 引理兩個方向都在子步證明，所以可作為等價使用。 - S10.1 · premise_audit · linear_map_def, mul_zero — 只用齊次性與乘以零；不需要可加性。 - S10 · premise_audit · L_lin_zero, contrapositive, linear_map_def — 只用到「線性 ⇒ T(0)=0」的逆否；不宣稱反向「T(0)=0 ⇒ 線性」對一般函數成立。 - S09 · inverse_equivalence · mul_inverse_nonzero, eq_congruence — 同減 6 與同乘 −1/2 都可逆，前提是 m≠0；代回 −2·3+6=0（N8）。 - S08 · premise_audit · S04, mko_affine — 判準只看 m 是否為零；截距 b 不影響次數。 - S07 · premise_audit · S02, S06, forall_elim — 兩個解讀都是已證式子的特例，不另加前提（N7）。 - S06 · premise_audit · S04, S05, G2, numeric_evaluation — 核對兩點只是確認計算無誤（N5、N6）；唯一性來自 S03 至 S05 的推導，不是來自這兩次代入。 - S05 · inverse_equivalence · eq_congruence, add_inverse — 同加 2 與同減 2 互為反運算；代回 −2+6=4。 - S04 · inverse_equivalence · mul_inverse_nonzero, eq_congruence, two_nonzero — 乘 1/2 與乘 2 互為反運算，前提 2≠0；代回 2·(−2)=−4。 - S03 · premise_audit · G2, S02, forall_elim — 需要兩點都在圖形上（G2）；若 x_1=x_2，等式變成 0=0，不能決定 m（MKO 假設 a2）。 - S02.1 · inverse_equivalence · distributive, add_inverse, add_comm — 每一步都是實數恆等式，雙向成立。 - S02 · inverse_equivalence · L_diff — 兩邊是同一個實數的兩種寫法，對所有 x_1、x_2 都成立（N1）。 - S01 · premise_audit · G1, mko_affine, linear_map_def — 此步只寫出定義與分類，不推出新事實。 ## 錯誤控制與反例 不是每個 mx+b 都是一次函數MKO 指出的第一個誤解是把所有 mx+b 都叫一次函數。只有 m≠0 時次數為一（S08）；g(x)=0·x+5 雖然寫成 mx+b 的形式，卻是常數函數，沒有零點（S13）。 仿射不等於線性映射MKO 指出的第二個誤解是把帶非零截距的仿射函數當成線性代數的線性映射。線性映射必有 T(0)=0（S10.1），而 f(0)=6；可加性也失敗：f(2)=2≠8=f(1)+f(1)（S10）。初等教材的 linear function 與線性代數的 linear map 是不同概念。 兩點斜率要 x_1≠x_2；單點相等不是全域相等S03、S04 能除以 x_2−x_1 是因為 1≠3。若兩點橫坐標相同，例如 (2,1) 與 (2,5)，(5−1)/(2−2) 無定義，而且沒有函數 ℝ→ℝ 能在 2 同時取 1 與 5。另一方面，f(2)=k(2) 只說明輸入 2 的輸出相同；全域相等要求斜率與截距都相同（S11、S12）。 - g(x)=5 是一次函數，因為它可以寫成 0·x+5 → reject — m=0，g 是常數函數，屬於仿射族但次數不是一。 - f(x)=−2x+6 是 ℝ 線性映射 → reject — f(0)=6≠0；而且 f(1+1)=2≠8=f(1)+f(1)。 - 通過 (2,1) 與 (2,5) 的仿射函數斜率是 (5−1)/(2−2) → reject — x_1=x_2 時斜率公式除以零；也沒有函數 ℝ→ℝ 在 2 同時取 1 與 5。 - f(2)=k(2)=2，所以 f=k → reject — 單點相等不推出全域相等：f(0)=6≠0=k(0)，斜率 −2≠1。 ## 結論與限制 由 (1,4)、(3,0) 得 m=(0−4)/(3−1)=−2、b=6，f(x)=−2x+6。因 m≠0，f 次數為一，唯一零點是 −b/m=3；但 f(0)=6≠0，f 不是 ℝ 線性映射。兩個仿射函數在 ℝ 上相等當且僅當斜率與截距都相同，所以 f(2)=k(2)=2 並不推出 f=k。m=0 時，g(x)=5 無零點，h(x)=0 處處為零，兩者都不是次數一的函數。 - 本稿只處理 ℝ→ℝ 的仿射函數；多變數仿射映射與一般向量空間上的線性映射不在範圍內。 - N1 是 degree 型格點核對（各變數次數至多一），作為 L_diff 代數恆等式的輔助；引理的證明是 S02.1。 ## 驗證及來源綁定 15 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: fb722ebaf4dc7b60839292d104faf6dc837ca15a0a3ed5015f7c9c626d96a85a - original source SHA-256: fb722ebaf4dc7b60839292d104faf6dc837ca15a0a3ed5015f7c9c626d96a85a - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-linear-function-01.json)