數學表徵：判定文字、符號、表格與序對是否表示同一個函數

目標與範圍

固定對象 f:D→ℤ，D={0,1,2,3}，f(x)=2x−1。判定：文字「輸入加倍後減 1」對應 2x−1；表格 T1={(0,−1),(1,1),(2,3),(3,5)} 表示 f；序對集合是 f 的圖形；由兩列 (1,1)、(3,5) 唯一恢復仿射規則；表格 T2 把 (3,5) 換成 (3,6) 後不表示 f，也不表示任何仿射規則；含重複輸入的 T3 不是函數表；定義在 ℤ 上的 g(x)=2x−1 與 f 不是同一個函數；以及表格不提供未列點的值。

具體練習使用整係數仿射規則與完整明示的有限表格／序對（MKO 假設 a1）；輔助的兩點仿射引理則在實數係數與實數座標下敘述；所有核對只在列出的定義域上進行，未列點與圖形外觀不提供數值（假設 a2）。不處理一般圖形的語義或更完整的 typed semantic bridge；不改動 canonical MKO 或英文 edition。

已知條件與符號

• function_def
• cartesian_product_def
• set_extensionality
• mul_inverse_nonzero
• quantifier_negation

• G1 — 對象：f:D→ℤ，D={0,1,2,3}，f(x)=2x−1。
• G2 — 解讀規則：表格的一列 (x,y) 表示「輸入 x 的輸出是 y」。一個表格表示 f，當且僅當它的輸入恰為 D 的元素、每個各出現一次，且每一列都滿足 y=f(x)。
• G3 — 文字表徵 W：「把輸入加倍，然後減 1」。
• G4 — T1={(0,−1),(1,1),(2,3),(3,5)}；T2={(0,−1),(1,1),(2,3),(3,6)}；T3=(0,−1),(1,1),(1,2),(2,3),(3,5)（輸入 1 出現兩次）。
• G5 — g:ℤ→ℤ，g(x)=2x−1。

• D=\{0,1,2,3\} — f 的定義域
• f(x)=2x-1 — 符號表徵
• T_1,\ T_2,\ T_3 — 三個待檢查的表格／序對列表
• \Gamma_f — f 的圖形 {(x,f(x)) ∣ x∈D}
• g — 定義在 ℤ 上的同一公式

規則與來源

• function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
• cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
• set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
• mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
• set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
• eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_repr · cited — 同一數學對象可以用文字、符號、表格、序對或圖形表示。兩個表示是否對應，必須先固定對象、定義域、標度與解讀規則；不能只依外觀宣稱等價。 · mko-mathematical-representation
• mko_repr_notes · cited — 表格列出指定輸入與輸出，符號式則給計算規則；二者只有在共同域及每列數值相符時形成明示語義橋。兩點可決定非垂直仿射規則，但必須先確認橫坐標不同；重複輸入若對應不同輸出，就不是函數表。圖像可以支援理解，但像素位置、視覺直線感或未標示刻度不能替代明示資料。 · mko-mathematical-representation
• L_two_point · lemma — 對實數座標，若 x₁≠x₂，則恰有一個實係數仿射規則 y=ax+b 通過 (x₁,y₁) 與 (x₂,y₂)，即 a=(y₂−y₁)/(x₂−x₁)，b=y₁−a·x₁。

逐步主鏈

\text{several representations}

\text{object }f:D\to\mathbb{Z},\ D=\{0,1,2,3\},\ \text{row }(x,y)\ \text{means}\ f(x)=y

W:\ \text{double the input, then subtract 1}

x\mapsto 2x-1

f(0),f(1),f(2),f(3)

-1,\ 1,\ 3,\ 5

\text{inputs of }T_1:\ 0,1,2,3

\text{each }x\in D\ \text{appears exactly once in }T_1

h_1(x)\ \text{vs}\ f(x)\ \text{for }x\in D

h_1=f\ \text{(}T_1\ \text{represents }f\text{)}

\Gamma_f=\{(x,f(x))\mid x\in D\}

\Gamma_f=\{(0,-1),(1,1),(2,3),(3,5)\}=T_1

(x_1,y_1),(x_2,y_2),\ x_1\neq x_2

a=\frac{y_2-y_1}{x_2-x_1},\ b=y_1-a\,x_1\ \text{(unique)}

(1,1),(3,5)\in T_1,\ 1\neq 3

a=\tfrac{5-1}{3-1}=2,\ b=1-2=-1;\ \text{rows }(0,-1),(2,3)\ \text{also satisfy }y=2x-1

T_2\ \text{row }(3,6),\ f(3)=5

T_2\ \text{does not represent }f\ \text{nor any affine rule}

T_3\ni(1,1),(1,2)

T_3\ \text{is not a function table}

g:\mathbb{Z}\to\mathbb{Z},\ f:D\to\mathbb{Z}

g\neq f,\ \ g|_D=f

x=4,\ x=\tfrac{1}{2}

\text{no value supplied: }4,\tfrac{1}{2}\notin D

\text{decisions}

W,\ 2x-1,\ T_1,\ \Gamma_f\ \text{represent }f;\ T_2,\ T_3,\ g\ \text{do not}

局部子步與引理

a x_1+b=y_1,\ a x_2+b=y_2

a(x_2-x_1)=y_2-y_1\ \Rightarrow\ a=\frac{y_2-y_1}{x_2-x_1},\ b=y_1-a\,x_1

a=\frac{y_2-y_1}{x_2-x_1},\ b=y_1-a\,x_1

a x_1+b=y_1,\ a x_2+b=y_2

逐步反向審查

• S13 · sufficient_goal_reduction · S02, S05, S06, S08, S09, S10, S11, S12, and_intro_elim — 目標 G：本稿目標的各項判定。足夠條件 H：所列各步已證（H⇒G 由合取引入）。H 由給定條件正向推出，沒有把 G 當作前提。
• S12 · premise_audit · mko_repr_notes, function_def — 只需要這些點不在定義域中；結論是「沒有資料」，不是「值為某數」。
• S11 · premise_audit · function_def, set_extensionality — 定義域不同就足以使函數不等；公式相同不能補救。
• S10 · premise_audit · function_def, mko_repr_notes — 只需要一個輸入對應兩個不同輸出；若重複的列輸出相同，那只是重複列，另行處理。
• S09 · premise_audit · S03, L_two_point, quantifier_negation — 否定全稱只需一個反例；「沒有仿射規則」用到引理的唯一性。
• S08 · premise_audit · L_two_point, numeric_evaluation — 需要 x₁≠x₂；核對其餘各列是必要的，因為仿射規則只由兩點決定，其他列可能不在其上（S09）。
• S07.2 · premise_audit · eq_replace, distributive, mul_inverse_nonzero — 需要 a(x₂−x₁)=y₂−y₁，這由 a 的定義與 x₂−x₁≠0 得到。
• S07.1 · premise_audit · mul_inverse_nonzero, eq_congruence, distributive — 這一步只證明「若存在則唯一」；存在性在 S07.2 另外核對。
• S07 · premise_audit · L_two_point — 依賴該引理，前提 x₁≠x₂ 不可省略。
• S06 · inverse_equivalence · set_builder, set_extensionality, cartesian_product_def — 兩邊有相同的元素，集合相等雙向成立。
• S05 · premise_audit · S03, S04, function_def, mko_repr_notes — 需要四列全部相符；只檢查部分列不足以推出函數相等（見 S09 的 T2）。
• S04 · premise_audit · function_def, G4 — 需要「涵蓋 D」與「不重複」兩件事；只檢查其一不足以得到函數。
• S03 · inverse_equivalence · numeric_evaluation — 精確整數計算，雙向相同。
• S02 · inverse_equivalence · def_unfold — 把 2x−1 讀回文字：先乘 2，再減 1，正是 W；兩個方向描述同一個計算程序。
• S01 · premise_audit · G1, G2, mko_repr — 此步只固定設定，不推出新事實。

錯誤控制與反例

看起來相同不等於等價

MKO 指出的誤解之一：把 T2 畫出來，(3,6) 只比直線高一格，四點看起來近乎在一條線上。但對應由逐列數值決定：f(3)=5≠6（S09）。像素位置與視覺直線感不能代替明示資料。

定義域與重複輸入不可忽略

MKO 指出的另一個誤解：g(x)=2x−1 在 ℤ 上與 f 公式相同，但定義域不同，所以不是同一個函數（S11）；T3 的輸入 1 對應兩個輸出，不是函數表（S10）。判定前必須先核對定義域與每個輸入只出現一次。

兩點決定候選，其餘各列仍要核對

由兩列恢復仿射規則需要橫坐標不同（S07.1 要除以 x₂−x₁）。恢復出的規則只是候選：T1 的其他列核對後相符（S08），T2 的第四列則不符（S09）。

• T2 表示 f，因為四列中有三列相符，而且畫出來幾乎是一條直線 → reject — 表示要求每一列都相符；f(3)=5≠6（S09）。
• g:ℤ→ℤ，g(x)=2x−1 與 f 是同一個函數 → reject — 定義域不同；例如 g(4)=7 有定義，4∉D（S11）。
• T3 的每一列都是序對，所以 T3 是一個函數表 → reject — 輸入 1 對應 1 與 2 兩個輸出（S10）。
• 由 T1 可知 f(1/2)=0，因為這些點在一條直線上 → reject — 1/2∉D，未列點與圖形外觀不提供數值（S12）。
• 文字「把輸入加倍，然後減 1」描述的是 2(x−1) → reject — 2(x−1) 是先減後乘；在 x=0 得 −2，而 W 給 −1（S02）。

結論與限制

固定 f:D→ℤ（D={0,1,2,3}，f(x)=2x−1）與「列 (x,y) 表示 f(x)=y」的解讀規則後：文字「輸入加倍後減 1」、公式 2x−1、表格 T1 與序對集合 {(0,−1),(1,1),(2,3),(3,5)} 都表示 f；由 (1,1)、(3,5)（1≠3）唯一恢復 y=2x−1，其餘列另外核對相符。T2 在 x=3 的值 6≠5，不表示 f，且依兩點唯一性不表示任何仿射規則；T3 中輸入 1 對應兩個輸出，不是函數表；g:ℤ→ℤ 與 f 定義域不同而不相等；表格不提供 x=4 或 x=1/2 的值。

• 圖形表徵只在錯誤控制與 S12 中討論，沒有建立座標刻度與像素的正式對應；更完整的 typed semantic bridge 屬於 MKO 的 formal next。

驗證及來源綁定

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

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

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