# 有限交換環上的多項式環：在 (ℤ/4ℤ)[x] 中做加法、卷積與次數核對 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-polynomial-ring-over-finite-commutative-ring/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-polynomial-ring-over-finite-commutative-ring-01 · production-20261019-adopted-96 ## 目標與範圍 在 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≤rm+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),\ (fg)_{m+n}=f_mg_n 條件：f\neq0,\ g\neq0 規則：L_top_coeff · 依賴：S02, S06, S07, S08 葉節點依據：poly_ops + finite_sum_rules + mul_zero + deg_def 依引理 L_top_coeff（在 S09.1、S09.2 證明），索引大於 m+n 的積係數全為零，索引 m+n 的係數恰為首項係數之積；只有積非零時才把前者寫成次數至多 m+n，零多項式依本稿約定沒有次數。在本例 m=n=1，f_1=g_1=2，f_1 g_1=0，所以 f·g、f·f、g·g 的索引 2 的係數都是 0，與 S06 到 S08 一致：前兩者次數降到 1 與 0，後者成為零多項式。 S10 · implies操作前 h=1+x=(1,1),\ g=(0,2) 操作後 hg=(0,2,2)=2x+2x^2,\ \deg(hg)=2 條件：h_1g_1=2\neq0 規則：L_top_coeff · 依賴：S09, S01, poly_ops 葉節點依據：poly_ops + mod_reduce + deg_def 對照：h=1+x 的首項係數是 1。卷積：索引 0 的係數 1·0=0；索引 1 的係數 1·2+1·0=2（N5）；索引 2 的係數 1·2=2≠0（N6）。所以 deg(hg)=2=1+1。依 L_top_coeff，次數相加恰在首項係數之積非零時成立；只要首項係數有一個是 1，就不會被零因子消去。 S11 · implies操作前 x^n=e_n,\ m\neq n 操作後 e_m\neq e_n 條件：1\neq0\ \text{in}\ R 規則：mko_polyring_def · 依賴：S01, G2 葉節點依據：function_def + injective_surjective_def + def_unfold x^n 的係數序列 e_n 在索引 n 的係數為 1、其餘為 0。若 m≠n，比較索引 m 的係數：(e_m)_m=1，(e_n)_m=0；由 S01，1≠0，所以兩序列不同，e_m≠e_n。因此 n↦x^n 是 ℕ 到 R[x] 的單射。 S12 · implies操作前 n\mapsto x^n\ \text{injective} 操作後 R[x]\ \text{is not finite} 條件：無 規則：contradiction · 依賴：S11, finite_counting_basics 葉節點依據：contradiction + finite_counting_basics + injective_surjective_def 假設 R[x] 有限，恰有 N 個元素。由 S11，x^0、x^1 直到 x^N 是 R[x] 中 N+1 個互異元素，即 {0,1,直到 N} 到一個 N 元集合的單射；它的像是 N+1 個元素的子集，但有限集的子集元素不多於該集合，矛盾。所以 R[x] 不是有限環。每個固定次數上界的部分是有限的，例如次數小於 3 的多項式恰有 4^3=64 個（N7），但次數沒有上界。 S13 · implies操作前 x^2,\ x^4\in R[x] 操作後 x^2\neq x^4,\ \text{but}\ t^2=t^4\ \text{for every}\ t\in R 條件：無 規則：function_def · 依賴：S01, G2, function_def 葉節點依據：function_def + mod_reduce + numeric_evaluation 作為多項式，x^2 與 x^4 在索引 2 的係數係數為 1 與 0，所以不同（S11）。作為 R 上的函數，逐點代入全部 4 個元素：0^2=0^4=0，1^2=1^4=1，2^2=4≡0 與 2^4=16≡0，3^2=9≡1 與 3^4=81≡1，兩函數相同（N8 對 R 的全部 4 個元素逐一核對）。R 到 R 的函數只有 4^4=256 個（N9），是有限集；R[x] 不是函數集合，不能因為函數有限就說 R[x] 有限。 S14 · implies操作前 \text{S04, S06 to S09, S12} 操作後 f+g=1,\ fg=2x,\ f^2=1,\ g^2=0;\ R[x]\ \text{infinite} 條件：無 規則：and_intro_elim · 依賴：S04, S06, S07, S08, S09, S12 葉節點依據：and_intro_elim 彙整：f+g=1（需正規化），fg=2x（次數 1，不是 2），f·f=1（1 次多項式可逆），g·g=0（R[x] 有零因子）；首項係數公式說明次數何時相加；1≠0 使單項式互異，R[x] 不是有限環。 ## 局部子步與引理 S05.1 · equivalent操作前 (fg)_0=f_0g_0 操作後 1\cdot0=0 條件：無 規則：mul_zero · 依賴：S02, poly_ops 葉節點依據：mul_zero i+j=0 只有 (0,0)：f_0 g_0=1·0=0。 S05.2 · equivalent操作前 (fg)_1=f_0g_1+f_1g_0 操作後 1\cdot2+2\cdot0=2 條件：無 規則：poly_ops · 依賴：S02, S01, poly_ops 葉節點依據：poly_ops + mod_reduce + numeric_evaluation i+j=1 有 (0,1) 與 (1,0) 兩項：1·2+2·0=2+0=2（N2）。 S05.3 · equivalent操作前 (fg)_2=f_0g_2+f_1g_1+f_2g_0 操作後 0+2\cdot2+0=0 條件：無 規則：poly_ops · 依賴：S02, S01, poly_ops 葉節點依據：poly_ops + mod_reduce + mul_zero i+j=2 有三項；f_0 g_2=1·0=0、f_2 g_0=0·0=0，中間 f_1 g_1=2·2=4≡0（S01，N3）。所以 (fg)_2=0：首項係數的乘積被零因子消去。 S09.1 · implies操作前 k>m+n,\ i+j=k 操作後 f_ig_j=0,\ \text{so}\ (fg)_k=0 條件：無 規則：mul_zero · 依賴：poly_ops, deg_def, mul_zero 葉節點依據：mul_zero + deg_def + de_morgan_logic + finite_sum_rules 若 i≤m 且 j≤n，則 i+j≤m+nm 或 j>n。依次數定義 f_i=0 或 g_j=0，該項為 0（u·0=0、0·u=0）。卷積和的每項都是 0，所以 (fg)_k=0。 S09.2 · equivalent操作前 (fg)_{m+n}=\sum_{i+j=m+n}f_ig_j 操作後 (fg)_{m+n}=f_mg_n 條件：無 規則：poly_ops · 依賴：S09.1, poly_ops, deg_def 葉節點依據：poly_ops + mul_zero + add_zero + finite_sum_rules 在 i+j=m+n 的各項中：若 in，g_j=0；若 i>m 則 f_i=0。只剩 (i,j)=(m,n) 一項，所以 (fg)_{m+n}=f_m g_n。因此 deg(fg)=m+n 當且僅當 f_m g_n≠0。S09.1 與 S09.2 合起來證得引理 L_top_coeff。 ## 逐步反向審查 - 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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-polynomial-ring-over-finite-commutative-ring-01.json)