有限交換環上的多項式環：在 (ℤ/4ℤ)[x] 中做加法、卷積與次數核對

目標與範圍

在 R=ℤ/4ℤ 上取 f=1+2x、g=2x。依係數序列定義計算 f+g、f·g、f·f、g·g 並正規化；證明首項係數公式 (fg)_{m+n}=f_m g_n，說明為何此處 deg(fg)=deg f+deg g 失敗；最後證明 R[x] 不是有限環。

只在 MKO 範圍內工作：係數環 ℤ/4ℤ 以完整加法表與乘法表給出（取模 4），多項式為尾端零已正規化的有限支撐係數序列（假設 a1）；不假設係數環是域、整環、UFD 或 Euclidean domain，有零因子時不使用次數相加公式（假設 a2）。不處理多項式理想、商環或有限域；不改動 canonical MKO 或英文 edition。

已知條件與符號

• finite_sum_rules
• finite_counting_basics
• mul_zero
• power_laws
• function_def

• G1 — R=ℤ/4ℤ={0,1,2,3}，加法與乘法為整數運算後取除以 4 的餘數；完整的兩張表由此確定，R 是有限交換含一環，但不是整環（2·2=0）。
• G2 — R[x] 的元素是 R 中只有有限多項非零的係數序列 (a_k)_{k≥0}；寫成列表時去掉尾端的零（正規化）。兩多項式相等當且僅當每個係數相等。
• G3 — f=1+2x，即 f_0=1、f_1=2、其餘為 0；g=2x，即 g_0=0、g_1=2、其餘為 0。

• R=\mathbb{Z}/4\mathbb{Z} — 係數環，元素 0、1、2、3
• R[x] — R 上的多項式環
• f_k — f 的索引 k 的係數（x^k 的係數）
• \deg f — 非零多項式中最大的 k 使 f_k≠0
• e_n — x^n 的係數序列：索引 n 的係數為 1，其餘為 0

規則與來源

• finite_sum_rules · prerequisite — 有限和：Σ_{i=1}^{0} a_i=0、Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}；Σ(a_i+b_i)=Σa_i+Σb_i；Σ c·a_i=c·Σa_i。
• finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
• mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
• power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
• function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• de_morgan_logic · prerequisite — 邏輯的德摩根律：¬(P∧Q) ⇔ ¬P∨¬Q；¬(P∨Q) ⇔ ¬P∧¬Q。
• add_zero · prerequisite — 加法單位元：u+0=u。
• 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。
• contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_polyring_def · cited — R 為有限交換含一環時，R[x] 的每個元素是有限支撐係數序列；加法逐係數，乘法為有限卷積。若 1 不等於 0，單項式 1、x、x 平方等依 degree 互異，因此普通 R[x] 不稱有限環。 · mko-polynomial-ring-over-finite-commutative-ring
• mod_reduce · prerequisite — 在 ℤ/nℤ 中，整數 m 代表它除以 n 的餘數 r（0≤r<n）；兩個整數代表同一元素當且僅當 n 整除兩者之差；和與積是整數和、整數積的餘數。
• poly_ops · prerequisite — 多項式運算：(f+g)_k=f_k+g_k；(fg)_k=Σ_{i+j=k} f_i g_j（有限和，在 R 中計算）。
• deg_def · prerequisite — 非零多項式 f 的次數 deg f 是使 f_k≠0 的最大 k；零多項式沒有次數。
• L_top_coeff · lemma — 在任何交換環上，若 deg f=m、deg g=n，則 k>m+n 時 (fg)_k=0，且 (fg)_{m+n}=f_m g_n。因此 deg(fg)=m+n 當且僅當 f_m g_n≠0；否則 fg=0 或 deg(fg)<m+n。

逐步主鏈

\mathbb{Z}/4\mathbb{Z}\ \text{tables}

2+2=0,\ 2\cdot2=0,\ 1\cdot2=2,\ 1\cdot1=1,\ 1\neq0

f=1+2x,\ g=2x

f=(1,2),\ g=(0,2),\ \deg f=\deg g=1

f+g

(1+0,\ 2+2)=(1,0)

f+g=(1,0)

f+g=(1)=1,\ \deg(f+g)=0

(fg)_k=\sum_{i+j=k}f_ig_j

fg=(0,2,0)

fg=(0,2,0)

fg=(0,2)=2x,\ \deg(fg)=1\neq 1+1

f\cdot f

(1\cdot1,\ 1\cdot2+2\cdot1,\ 2\cdot2)=(1,0,0)=1

g\cdot g

(0\cdot0,\ 0\cdot2+2\cdot0,\ 2\cdot2)=(0,0,0)=0

\deg f=m,\ \deg g=n

(fg)_k=0\ (k>m+n),\ (fg)_{m+n}=f_mg_n

h=1+x=(1,1),\ g=(0,2)

hg=(0,2,2)=2x+2x^2,\ \deg(hg)=2

x^n=e_n,\ m\neq n

e_m\neq e_n

n\mapsto x^n\ \text{injective}

R[x]\ \text{is not finite}

x^2,\ x^4\in R[x]

x^2\neq x^4,\ \text{but}\ t^2=t^4\ \text{for every}\ t\in R

\text{S04, S06 to S09, S12}

f+g=1,\ fg=2x,\ f^2=1,\ g^2=0;\ R[x]\ \text{infinite}

局部子步與引理

(fg)_0=f_0g_0

1\cdot0=0

(fg)_1=f_0g_1+f_1g_0

1\cdot2+2\cdot0=2

(fg)_2=f_0g_2+f_1g_1+f_2g_0

0+2\cdot2+0=0

k>m+n,\ i+j=k

f_ig_j=0,\ \text{so}\ (fg)_k=0

(fg)_{m+n}=\sum_{i+j=m+n}f_ig_j

(fg)_{m+n}=f_mg_n

逐步反向審查

• S14 · sufficient_goal_reduction · S04, S06, S07, S08, S09, S12 — 目標 G：本稿目標中的計算、次數說明與無限性。足夠條件 H：S04、S06 到 S09、S12；H⇒G 由合取。H 由 G1 到 G3 正向證成，沒有把 G 當作前提，也沒有使用次數相加公式。
• S13 · premise_audit · G2, function_def, mod_reduce — 函數相同只靠對 R 的全部 4 點核對（對有限定義域這是完整核對）；多項式不同靠係數比較。兩個結論不衝突，因為相等的標準不同。
• S12 · premise_audit · S11, finite_counting_basics, contradiction — 需要對每個 N 都有 N+1 個互異元素，這由 S11 的一般論證提供，不是由檢查有限多個 N 得到。
• S11 · premise_audit · S01, G2, mko_polyring_def — 關鍵前提是 1≠0：在零環中 1=0，所有 x^n 都等於 0，R[x] 只有一個元素。
• S10 · premise_audit · S09, L_top_coeff — 結論依賴 h_1 g_1=2≠0 這個具體核對，不是由「通常次數相加」推得。
• S09.2 · inverse_equivalence · poly_ops, mul_zero, add_zero — 去掉的項全為 0，加上或去掉 0 不改變和，所以兩式相等，雙向成立。
• S09.1 · premise_audit · deg_def, mul_zero, de_morgan_logic — 只用到次數定義與乘零；不宣稱 k≤m+n 的係數非零。
• S09 · premise_audit · S02, L_top_coeff — 引理只需要 R 交換，不需要整環；它說的是「何時」次數相加，而不是總是相加。
• S08 · inverse_equivalence · poly_ops, mod_reduce, mul_zero — 每個係數都可重算為 0；零多項式與 (0,0,0) 是同一序列。
• S07 · inverse_equivalence · poly_ops, mod_reduce — 三個係數逐一可重算；f·f 與 1 逐項相同。
• S06 · inverse_equivalence · G2, deg_def — 正規化可逆（補回尾端零）；次數讀自正規化列表。
• S05.3 · inverse_equivalence · poly_ops, mod_reduce, mul_zero — 三項逐一可重算；在 ℤ 中 2·2=4≠0，但在 ℤ/4ℤ 中為 0。
• S05.2 · inverse_equivalence · poly_ops, mod_reduce — 兩項都列出，沒有遺漏或重複；結果可重算。
• S05.1 · inverse_equivalence · mul_zero — 恆等式 u·0=0，雙向成立。
• S05 · inverse_equivalence · poly_ops, mul_zero, finite_sum_rules — 每個係數都是同一卷積公式的求值，可逐項重算；左右兩邊是同一個多項式。
• S04 · inverse_equivalence · G2, deg_def — 補回尾端零得到同一序列，雙向成立；次數只對正規化的列表讀取。
• S03 · inverse_equivalence · poly_ops, mod_reduce — 反向：(1,0)−g=(1−0, 0−2)=(1,2)=f（在 ℤ/4ℤ 中 −2=2），還原了 f+g 的左邊。
• S02 · inverse_equivalence · G2, deg_def — 列表與多項式互相決定：由 (1,2) 讀回 1+2x，由 (0,2) 讀回 2x。
• S01 · premise_audit · G1, mod_reduce — 每項都可由取模重算（N1、N3）；本步只讀表，不推出表外的事實。

錯誤控制與反例

有限係數環不給有限多項式環

MKO 指出的誤解：把 R[x] 也叫有限載體。係數只有 4 種選擇，但次數沒有上界；S11、S12 證明 R[x] 含任意多個互異的單項式。對非負整數 d，所有指數≥d 的係數均為 0 的部分（含零多項式）有 4^d 個元素。d=0 時只有零多項式；d=1 時這是對乘法封閉的常數子環，兩種情況都對乘法封閉；d≥2 時則不封閉，因 x^{d−1} 與 x 均在其中，而乘積 x^d 不在其中。

有零因子時，次數相加未必成立

MKO 的第二個誤解是硬套 deg(fg)=deg f+deg g。在 ℤ/4ℤ 上，(2x)(2x)=0 沒有次數，(1+2x)(2x)=2x 次數為 1，(1+2x)^2=1 次數為 0。正確的說法是 L_top_coeff：次數相加當且僅當首項係數之積非零（S09、S10）。

先正規化再讀次數

逐係數加法可能產生尾端零：f+g 先得 (1,0)。(1,0) 與 (1) 是同一多項式，次數是 0 而不是 1（S04）。比較或讀次數前都要先去掉尾端零。

• R=ℤ/4ℤ 只有 4 個元素，所以 R[x] 是有限環 → reject — 1≠0 使 1、x、x² 等互異（S11），R[x] 含任意多個元素（S12）。
• deg((2x)(2x))=1+1=2 → reject — (2x)(2x)=4x²=0 是零多項式，沒有次數（S08）。
• x² 與 x⁴ 在 ℤ/4ℤ 的每個元素取值相同，所以在 R[x] 中 x²=x⁴ → reject — 多項式相等是逐係數相等；索引 2 的係數係數 1≠0（S13）。
• 1+2x 是 1 次多項式，所以不可能是 R[x] 的可逆元 → reject — 在 ℤ/4ℤ 中 (1+2x)²=1+4x+4x²=1（S07），所以 1+2x 確為 1 次可逆元。需要整環前提的是負例主張背後的「用次數相加排除正次數可逆元」論證，不是這個模 4 恆等式；此處係數環有零因子，不能套用那個次數論證。

結論與限制

在 (ℤ/4ℤ)[x] 中，f+g=1（正規化後次數 0），fg=2x（次數 1≠2），f·f=1（f=1+2x 是可逆元），g·g=0（兩個非零多項式之積為 0）。對任何交換環，(fg)_{m+n}=f_m g_n，所以次數相加恰在首項係數之積非零時成立。因 1≠0，單項式 1、x、x² 等互異，R[x] 不是有限環，雖然 R 只有 4 個元素。

• L_top_coeff 對任何交換環都已證明；S03 到 S08、S10 的計算只屬於 ℤ/4ℤ 與這幾個多項式。多項式理想、商環與有限域上的多項式（MKO 的下一步）不在本稿範圍。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 483fdc8d305e2bb342f7008783ce4641fe203322aebbac3fe3dbe5604f4c2e83
• original source SHA-256: 0bab65c7935d902ed18c55a3ac5fa3655cf979c044b1d2746c31e5cb7d687baf
• Lean: NOT_RUN · independent AI: NOT_MEASURED

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