仿射函數與一次函數：由兩點求 m、b，判定次數、零點與是否為線性映射

目標與範圍

仿射函數 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）。

逐步主鏈

f:\mathbb{R}\to\mathbb{R}

f(x)=mx+b;\ m\neq0\Rightarrow\deg f=1;\ m=0\Rightarrow f\ \text{constant}

f(x_2)-f(x_1)

m(x_2-x_1)

f(3)-f(1)=m(3-1)

0-4=2m,\ \text{i.e.}\ -4=2m

-4=2m

m=\frac{-4}{2}=-2

f(1)=4:\ -2\cdot 1+b=4

b=4+2=6

m=-2,\ b=6

f(x)=-2x+6,\quad f(3)=-6+6=0

f(x)=-2x+6

b=f(0)=6,\quad f(x+1)-f(x)=m=-2

m=-2

m\neq 0\Rightarrow f\ \text{has degree one}

f(x)=0:\ -2x+6=0

x=\frac{-6}{-2}=3=-\frac{b}{m}

f(0)=6

f\ \text{is not}\ \mathbb{R}\text{-linear}

\forall x\in\mathbb{R}:\ mx+b=nx+c

m=n\ \land\ b=c

f(2)=-4+6=2=k(2)

f\neq k\quad((-2,6)\neq(1,0))

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}

f,\ k,\ g,\ h

f(x)=-2x+6:\ \deg 1,\ \text{zero}\ 3,\ \text{not linear};\ f\neq k;\ g,h\ \text{constant}

局部子步與引理

(mx_2+b)-(mx_1+b)

mx_2-mx_1=m(x_2-x_1)

T\ \mathbb{R}\text{-linear}

T(0)=T(0\cdot 0)=0\cdot T(0)=0

\forall x:\ mx+b=nx+c

b=c\ (x=0),\quad m+b=n+c\ (x=1)\ \Rightarrow\ m=n

m=n\ \land\ b=c

\forall x:\ mx+b=nx+c

逐步反向審查

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