反函數：交換有限雙射表並求非零斜率仿射函數的反函數

目標與範圍

（一）A={1,2,3}、B={4,5,6}，p(1)=5、p(2)=6、p(3)=4。先確認 p 是雙射，再交換有序對得到候選 q，驗證 q 是總函數 B→A，並逐側檢查 q(p(x))=x 與 p(q(y))=y。（二）f:ℝ→ℝ，f(x)=−4x+6（m=−4≠0）：求反函數 g(y)=uy+v，u、v 以最簡、正分母的有理數表示，並對所有實數驗證兩側恆等式。（三）說明 h(1)=4、h(2)=4、h(3)=6 的交換表不是 B→A 的函數，以及 f^{-1} 不是 1/f。

依 MKO 假設：有限表先確認是宣告 A→B 的雙射（a1）；候選先驗為總函數再查兩側恆等式（a2）；仿射例子為 f:ℝ→ℝ、m≠0，係數以最簡正分母有理數表示（a3）。仿射部分以代數恆等式對所有實數證明，不是抽樣。不處理一般單側反函數理論、反函數唯一性或機器證明；不改動 canonical MKO 或英文 edition。

已知條件與符號

• function_def
• injective_surjective_def
• composition_def
• frac_rules
• distributive
• numeric_evaluation

• G1 — A={1,2,3}、B={4,5,6}；p:A→B，p(1)=5、p(2)=6、p(3)=4。
• G2 — f:ℝ→ℝ，f(x)=−4x+6，即 m=−4、b=6。
• G3 — h:A→B，h(1)=4、h(2)=4、h(3)=6。
• G4 — 驗收標準（MKO a2）：候選 g 是雙射 f:A→B 的反函數，當且僅當 g 是總函數 B→A，且對每個 x∈A 有 g(f(x))=x、對每個 y∈B 有 f(g(y))=y。

• p,q — 有限雙射表與交換後的表
• f,g — 仿射函數 f(x)=−4x+6 與其反函數
• h — 非雙射的有限表
• R^{\mathsf T} — 交換關係 {(b,a) ∣ (a,b)∈R}
• \mathrm{id}_A — A 上的恆等函數

規則與來源

• function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
• injective_surjective_def · prerequisite — 單射：f(a)=f(a′) ⇒ a=a′。滿射：每個 b∈B 都有 a∈A 使 f(a)=b。雙射：既單又滿，此時有唯一反函數 f⁻¹ 使 f⁻¹∘f=id_A、f∘f⁻¹=id_B。
• composition_def · prerequisite — 合成：對 f:A→B 與 g:B→C，g∘f:A→C 定義為 (g∘f)(a)=g(f(a))。
• frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
• cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• 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 不定義。
• 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。
• iff_intro · prerequisite — 雙條件：P⇒Q 與 Q⇒P 都成立時，P⇔Q 成立；反之亦然。
• neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• mko_inverse_def · cited — 若 f:A→B 是雙射，反函數 g:B→A 由每個 b 的唯一原像定義，滿足 g(f(x))=x（x∈A）及 f(g(y))=y（y∈B）。有限表可以交換有序對後建立 g；若 f 非雙射，交換表不能自動成為這個 B→A 的反函數。 · mko-inverse-function
• mko_bijective_fiber · cited — 總函數 f:A→B 為雙射，當且僅當它同時單射與滿射；等價地，每個 b∈B 的纖維恰有一個元素。 · mko-bijective
• swap_table · prerequisite — 交換表：關係 R⊆A×B 的交換為 R^T={(b,a) ∣ (a,b)∈R}⊆B×A。b 在 R^T 中作為第一坐標出現的次數，等於 b 在 R 中作為第二坐標出現的次數。
• L_solve_affine · lemma — 對實數 m≠0、b、x、y：y=mx+b ⇔ x=(y−b)/m。

逐步主鏈

p(1)=5,\ p(2)=6,\ p(3)=4

p^{-1}(\{4\})=\{3\},\ p^{-1}(\{5\})=\{1\},\ p^{-1}(\{6\})=\{2\}\ \Rightarrow\ p\ \text{bijective}

p=\{(1,5),(2,6),(3,4)\}

q=p^{\mathsf T}=\{(5,1),(6,2),(4,3)\}

q=\{(4,3),(5,1),(6,2)\}

q:B\to A\ \text{total};\ q(4)=3,\ q(5)=1,\ q(6)=2

x\in A=\{1,2,3\}

q(p(x))=x\ \ \forall x\in A

y\in B=\{4,5,6\}

p(q(y))=y\ \ \forall y\in B

q:B\to A\ \text{total},\ q\circ p=\mathrm{id}_A,\ p\circ q=\mathrm{id}_B

q=p^{-1}

y=-4x+6

x=\frac{y-6}{-4}

\forall y\in\mathbb{R}:\ \bigl(f(x)=y\iff x=\tfrac{y-6}{-4}\bigr)

f^{-1}(\{y\})=\{\tfrac{y-6}{-4}\}\ \Rightarrow\ f\ \text{bijective}

y\in\mathbb{R}

g(y)=\frac{y-6}{-4}

\frac{y-6}{-4}

-\frac{1}{4}y+\frac{3}{2}

x\in\mathbb{R}\ \text{arbitrary}

g(f(x))=-\tfrac{1}{4}(-4x+6)+\tfrac{3}{2}=x

y\in\mathbb{R}\ \text{arbitrary}

f(g(y))=-4\bigl(-\tfrac{1}{4}y+\tfrac{3}{2}\bigr)+6=y

g\ \text{total},\ g\circ f=\mathrm{id}_{\mathbb{R}},\ f\circ g=\mathrm{id}_{\mathbb{R}}

f^{-1}(y)=-\tfrac{1}{4}y+\tfrac{3}{2}

f^{-1}(2)=1,\ \frac{1}{f(2)}=-\frac{1}{2}

f^{-1}\neq\frac{1}{f}

h^{\mathsf T}=\{(4,1),(4,2),(6,3)\}

h^{\mathsf T}\ \text{not a function}\ B\to A

\text{S06, S13, S14, S15}

q=p^{-1};\ f^{-1}(y)=-\tfrac{1}{4}y+\tfrac{3}{2};\ h^{\mathsf T}\ \text{rejected};\ f^{-1}\neq 1/f

局部子步與引理

y=mx+b

y-b=mx

y-b=mx

x=\frac{y-b}{m}

\frac{y-6}{-4}

\frac{y}{-4}-\frac{6}{-4}

\frac{y}{-4}-\frac{6}{-4}

-\frac{1}{4}y+\frac{3}{2}

逐步反向審查

• S16 · sufficient_goal_reduction · S06, S13, S14, S15, and_intro_elim — 目標 G 是 goal 的三部分。足夠條件 H 為 S06、S13、S14、S15 的合取，各自已從已知正向證成；H⇒G 只用合取引入。
• S15 · premise_audit · function_def, swap_table, G3 — 任一個要求失敗就足以否定「是函數」；這裡兩個都失敗。結論只關於 h，不影響 p、f。
• S14 · premise_audit · function_def, numeric_evaluation, S13 — 否定兩函數相等只需一個取值不同的輸入；本步不宣稱它們在每一點都不同。
• S13 · premise_audit · S09, S11, S12, mko_inverse_def — 三個驗收條件都已逐一成立；具體例只是示意，不是證明的一部分。
• S12 · premise_audit · composition_def, distributive, neg_mul, forall_intro — 與 S11 對稱；此側不能由 S11 推出，所以單獨證明。
• S11 · premise_audit · composition_def, distributive, neg_mul, forall_intro — 需要 f(x)∈ℝ 位於 g 的定義域，合成才有定義；推廣到所有 x 只因 x 是任意取的。
• S10.2 · inverse_equivalence · frac_rules, neg_mul — 分子分母同乘 −1 與約分都是等值改寫，可逆。
• S10.1 · inverse_equivalence · frac_rules — 分式加法規則雙向成立，前提只有分母不為零。
• S10 · inverse_equivalence · frac_rules, neg_mul — S10.1、S10.2 兩個子步都是對所有 y 成立的恆等改寫，所以兩個式子定義同一個函數。
• S09 · premise_audit · S08, mko_inverse_def, function_def — 只是依唯一原像命名函數；兩側恆等式仍在 S11、S12 另行驗證。
• S08 · premise_audit · S07, mko_bijective_fiber, iff_intro — 兩個方向都要用：只有 ⇐ 只給滿射，只有 ⇒ 只給單射。
• S07.2 · inverse_equivalence · mul_inverse_nonzero, eq_congruence — 乘 1/m 與乘 m 互為反運算，前提 m≠0，正是 MKO a3 的條件。
• S07.1 · inverse_equivalence · eq_congruence, add_inverse — 減 b 與加 b 互為反運算，對任何實數 b 都可做。
• S07 · inverse_equivalence · L_solve_affine — 引理兩個方向都在子步中證明，條件 −4≠0 成立。
• S06 · premise_audit · S03, S04, S05, mko_inverse_def — 需要三個條件同時成立；只有其中一側恆等式不夠（見錯誤控制）。
• S05 · premise_audit · case_analysis, composition_def, S03 — q 的值都在 A，p∘q 有定義；三個情形窮盡 B。
• S04 · premise_audit · case_analysis, composition_def, S03 — 合成有定義，因為 p 的值都在 B，也就是 q 的定義域；三個情形窮盡 A。這只是一側的恆等式，另一側在 S05。
• S03 · premise_audit · S01, swap_table, function_def — 總性需要每個纖維至少一個元素（p 滿射），單值性需要至多一個元素（p 單射），兩者都由 S01 提供。若 p 不是雙射，這一步就會失敗（見 S15）。
• S02 · premise_audit · swap_table, cartesian_product_def — 只是構造一個集合並命名，不宣稱 q 是函數。
• S01 · premise_audit · G1, mko_bijective_fiber, set_builder — 需要掃描全部三個輸入並檢查宣告陪域的全部三個目標；只用纖維刻畫的 ⇐ 方向。

錯誤控制與反例

反函數不是倒數

MKO 的誤解之一是把 f^{-1} 當成 1/f。上標 −1 表示對合成的反：f^{-1}(2)=1，但 1/f(2)=−1/2（S14）。而且 1/f 在 x=3/2 沒有定義（f(3/2)=0），f^{-1} 卻對每個實數都有定義。

非雙射的交換表不是反函數

另一個誤解是不管是否雙射都交換表。h 的纖維概況是 (2,0,1)，交換後 4 對應兩個值、5 沒有值，不是 B→A 的函數（S15）。MKO 要求先確認雙射（a1），再交換。

兩側恆等式都要查

只有一側成立時不是反函數。例：p′:{1,2}→{4,5,6}，p′(1)=4、p′(2)=5；候選 r:{4,5,6}→{1,2}，r(4)=1、r(5)=2、r(6)=1 是總函數，且對每個 x∈{1,2} 都有 r(p′(x))=x，但 p′(r(6))=p′(1)=4≠6。r 只是左反函數。本稿對 q 與 g 都分別驗證兩側（S04、S05、S11、S12）。

• g(y)=1/(−4y+6) 是 f 的反函數 → reject — 這是 1/f，不是反函數：f(0)=6，而 1/(−4·6+6)=−1/18≠0，所以 g(f(0))≠0。
• h 的交換表 {(4,1),(4,2),(6,3)} 是 h 的反函數 → reject — 它不是 B→A 的函數：4 有兩個值，5 沒有值；h 不是雙射。
• r(4)=1、r(5)=2、r(6)=1 滿足 r(p′(x))=x，所以 r 是 p′ 的反函數 → reject — 另一側不成立：p′(r(6))=p′(1)=4≠6。
• f(x)=−4x+6 的反函數是 g(y)=(y+6)/(−4) → reject — 符號錯：f(0)=6，而 (6+6)/(−4)=−3≠0；正確的是 (y−6)/(−4)。

結論與限制

p 的纖維概況為 (1,1,1)，是雙射；交換表 q 是總函數 B→A，q(4)=3、q(5)=1、q(6)=2，且 q∘p=id_A、p∘q=id_B，所以 q=p^{-1}。f(x)=−4x+6 是雙射，反函數為 f^{-1}(y)=(y−6)/(−4)=−(1/4)y+3/2，即 u=−1/4、v=3/2，兩側恆等式對所有實數成立。h 的交換表不是 B→A 的函數（4 有兩個值、5 沒有值）；f^{-1}(2)=1 而 1/f(2)=−1/2，所以 f^{-1}≠1/f。

• 本稿不另證反函數的唯一性；只驗證構造出的 q 與 g 符合 MKO 的兩側定義。
• N3 至 N5 是一次多項式在格點上的恆等式核對，與 S10 至 S12 的代數推導互相獨立。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: a9ff58a9eb164d3ba3885c3f347bc130c608c3b605ef14409ff4d974ddfcb2e6
• original source SHA-256: a9ff58a9eb164d3ba3885c3f347bc130c608c3b605ef14409ff4d974ddfcb2e6
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）