# 有限交換環：逐元素對核對 ℤ₆ 的交換律，並以上三角矩陣環為非交換反例

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-finite-commutative-ring/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-finite-commutative-ring-01 · production-20261019-adopted-96



## 目標與範圍

（一）在已通過有限含一環資格的 ℤ₆={0,1,2,3,4,5}（a⊕b=(a+b) mod 6、a⊗b=(ab) mod 6）上，核對全部 36 個有序元素對的 a⊗b=b⊗a，判定 ℤ₆ 是否為有限交換環。（二）說明 ℤ₆ 有非零零因子且 2 不可逆，所以不是整環或域。（三）在已通過資格的 ℱ₂ 上 2×2 上三角矩陣環 U 中，說明若干乘積可交換，但 U 不是交換環。

在 MKO 的範圍內工作：使用已通過有限含一環資格的同一組加法與乘法表（假設 a1），本稿不重新核對環公理；交換律量化所有有序元素對，不額外假設無零因子或非零元可逆（假設 a2）。整環與域只用來說明交換環不必具備這些性質。不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- mul_comm
- eq_refl_symm_trans
- matrix_product_def
- quantifier_negation
- numeric_evaluation


- G1 — ℤ₆ 的載體為 {0,1,2,3,4,5}，a⊕b=(a+b) mod 6，a⊗b=(ab) mod 6。乘法表各行：第 0 行 (0,0,0,0,0,0)；第 1 行 (0,1,2,3,4,5)；第 2 行 (0,2,4,0,2,4)；第 3 行 (0,3,0,3,0,3)；第 4 行 (0,4,2,0,4,2)；第 5 行 (0,5,4,3,2,1)；第 a 行、列索引 b 的項是 a⊗b。
- G2 — (ℤ₆,⊕,⊗) 已由父節點以這兩張完整表通過有限含一環資格，0 為加法單位元，1 為乘法單位元；本稿不重新核對。
- G3 — U 的載體是 8 個三元組 (a,b,c)∈{0,1}³，代表第一行 (a,b)、第二行 (0,c) 的矩陣；加法逐項 mod 2，乘法為矩陣乘積再 mod 2。U 已由父節點通過有限含一環資格，單位元為 I=(1,0,1)；本稿不重新核對。


- \mathbb{Z}_6=\{0,1,2,3,4,5\} — 模 6 剩餘的載體
- a\otimes b=(ab)\bmod 6 — ℤ₆ 的乘法表
- U — 𝔽₂ 上 2×2 上三角矩陣環，元素記為 (a,b,c)
- (a,b,c) — 代表矩陣，第一行 (a,b)、第二行 (0,c)
- E_{11},E_{12},E_{22},I — U 中的 (1,0,0)、(0,1,0)、(0,0,1)、(1,0,1)





## 規則與來源


- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- matrix_product_def · prerequisite — 矩陣乘法：若 A 為 m×n、B 為 n×p，則 (AB)_{ij}=Σ_{k=1}^{n} A_{ik}B_{kj}。矩陣乘法一般不可交換。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
- cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- add_zero · prerequisite — 加法單位元：u+0=u。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_comm_ring_def · cited — 在已通過完整有限含一環資格的同一加法與乘法表上，若每個 a,b 皆有 a 乘 b=b 乘 a，則為有限交換環。逐一核完整元素對，不由幾個樣本或表面對稱猜測。 · mko-finite-commutative-ring
- mko_unital_ring_def · cited — 在同一有限載體上給完整加法表與乘法表：加法為阿貝爾群；乘法結合且對加法左右分配；存在唯一乘法單位元 1 且 1≠0。不要求乘法交換。 · mko-finite-unital-ring
- mod_reduce · prerequisite — 對整數 m 與正整數 n，m mod n 是唯一滿足 0≤r<n 且 n 整除 m−r 的整數 r；相等的整數有相同的餘數。
- domain_field_def · prerequisite — 非零元 a、b 若 ab=0，稱為零因子。整環是 1≠0 且無零因子的交換環；域是每個非零元都有乘法逆元的交換環。





## 逐步主鏈

S01 · definition操作前

\mathbb{Z}_6\ \text{finite commutative ring}

操作後

\mathbb{Z}_6\ \text{qualified unital ring}\ \land\ \forall a,b\in\mathbb{Z}_6:\ a\otimes b=b\otimes a

條件：無

規則：mko_comm_ring_def · 依賴：G1, G2, mko_comm_ring_def, mko_unital_ring_def

葉節點依據：mko_comm_ring_def + def_unfold

依 MKO，有限交換環＝父環資格＋乘法交換律，兩者用同一組表。父環資格由 G2 提供（保留同一個 0、1 與全部環公理），所以剩下的責任只有：對每個有序對 (a,b) 核對 a⊗b=b⊗a。



S02 · equivalent操作前

\mathbb{Z}_6\times\mathbb{Z}_6

操作後

36=6\ \text{diagonal pairs}+30\ \text{off-diagonal pairs}

條件：無

規則：finite_counting_basics · 依賴：S01, G1, finite_counting_basics

葉節點依據：finite_counting_basics + cartesian_product_def + numeric_evaluation

有序對共 6·6=36 個，分成 a=b 的 6 個對角對與 a≠b 的 30 個非對角對；30 個非對角對又兩兩配成 (a,b) 與 (b,a)，共 15 組。這個分割不漏掉任何一對。



S03 · implies操作前

(a,a),\ a\in\mathbb{Z}_6

操作後

a\otimes a=a\otimes a

條件：無

規則：eq_refl_symm_trans · 依賴：S02

葉節點依據：eq_refl_symm_trans

對角對的交換條件是 a⊗a=a⊗a，由等號的自反性對 6 個對角對全部成立，不需查表。



S04 · equivalent操作前

a\otimes b=b\otimes a\ \ \text{and}\ \ b\otimes a=a\otimes b

操作後

\text{one equation per group}\ \{a,b\},\ a<b:\ 15\ \text{checks}

條件：無

規則：eq_refl_symm_trans · 依賴：S02

葉節點依據：eq_refl_symm_trans

有序對 (a,b) 的條件 a⊗b=b⊗a 與 (b,a) 的條件 b⊗a=a⊗b 依等號對稱性互相等價，所以每組只需核對一個等式；這不是省略，而是同一個等式同時涵蓋兩個有序對。



S05 · implies操作前

a\otimes b=(ab)\bmod 6

操作後

a\otimes b=(ab)\bmod 6=(ba)\bmod 6=b\otimes a\ \ (\forall a,b\in\mathbb{Z}_6)

條件：無

規則：mul_comm · 依賴：G1, mul_comm, mod_reduce

葉節點依據：mul_comm + mod_reduce + eq_replace

全稱證書：表由公式 (ab) mod 6 產生。整數乘法交換，ab=ba；相等的整數有相同的模 6 餘數，所以 (ab) mod 6=(ba) mod 6，即 a⊗b=b⊗a。這對每一對都成立，不依賴樣本。



S06 · implies操作前

\text{row}\ a\ \text{vs. column}\ a\ \text{of the listed table}

操作後

\text{the 15 entries above the diagonal equal the 15 below}

條件：無

規則：case_analysis · 依賴：G1, S04

葉節點依據：case_analysis + numeric_evaluation

在列出的表上逐組核對 15 個等式：含 0 的 5 組都是 0=0；{1,b} 的 4 組是 b=b（第 1 行是 (0,1,2,3,4,5)）；{2,3}:0=0，{2,4}:2=2，{2,5}:4=4；{3,4}:0=0，{3,5}:3=3；{4,5}:2=2。5+4+3+2+1=15 組全部相等。



S07 · implies操作前

\text{6 diagonal pairs (S03)},\ \text{30 off-diagonal pairs (S05, S06)}

操作後

\mathbb{Z}_6\ \text{is a finite commutative ring}

條件：無

規則：case_analysis · 依賴：S01, S03, S05, S06

葉節點依據：case_analysis + mko_comm_ring_def

36 個有序對分成對角與非對角兩類（S02），兩類都已核對，依分情形證明，所有對都滿足交換律；加上 G2 的父環資格，ℤ₆ 是有限交換環。



S08 · implies操作前

2\otimes 3=(6)\bmod 6

操作後

2\otimes 3=0,\ 2\neq 0,\ 3\neq 0\ \Rightarrow\ \mathbb{Z}_6\ \text{not an integral domain}

條件：無

規則：domain_field_def · 依賴：G1, S07, domain_field_def

葉節點依據：domain_field_def + quantifier_negation + numeric_evaluation

第 2 行、列索引 3 的項是 0：2⊗3=6 mod 6=0，而 2、3 都非零，所以 2 與 3 是零因子。ℤ₆ 雖然交換，卻不是整環。MKO 提醒：交換環仍可能有非零零因子。



S09 · implies操作前

\text{row 2}=(0,2,4,0,2,4)

操作後

\nexists x:\ 2\otimes x=1\ \Rightarrow\ \mathbb{Z}_6\ \text{not a field}

條件：無

規則：domain_field_def · 依賴：G1, domain_field_def

葉節點依據：domain_field_def + quantifier_negation + case_analysis

2 的逆元 x 必須使 2⊗x=1；第 2 行的六個值是 0、2、4、0、2、4，沒有 1。所以非零元 2 不可逆，ℤ₆ 不是域。這是在完整的一行上窮舉，不是抽樣。



S10 · equivalent操作前

\begin{pmatrix}a&b\\0&c\end{pmatrix}\begin{pmatrix}a'&b'\\0&c'\end{pmatrix}

操作後

(a,b,c)(a',b',c')=(aa',\ ab'+bc',\ cc')\bmod 2

條件：無

規則：matrix_product_def · 依賴：G3, matrix_product_def

葉節點依據：matrix_product_def + mul_zero + add_zero

依矩陣乘積：左上 aa'+b·0=aa'；右上 ab'+bc'；左下 0·a'+c·0=0；右下 0·b'+cc'=cc'。所以乘積仍是上三角，記為三元組 (aa', ab'+bc', cc')，各項再取 mod 2。這個公式產生 U 的完整 8×8 乘法表。



S11 · equivalent操作前

E_{11}E_{12}=(1,0,0)(0,1,0)

操作後

E_{11}E_{12}=(1\cdot0,\ 1\cdot1+0\cdot0,\ 0\cdot0)=(0,1,0)=E_{12}

條件：無

規則：numeric_evaluation · 依賴：S10

葉節點依據：numeric_evaluation + matrix_product_def

代入 S10 的公式，a=1、b=0、c=0，a'=0、b'=1、c'=0：第一項 0，第二項 1·1+0·0=1，第三項 0。



S12 · equivalent操作前

E_{12}E_{11}=(0,1,0)(1,0,0)

操作後

E_{12}E_{11}=(0\cdot1,\ 0\cdot0+1\cdot0,\ 0\cdot0)=(0,0,0)

條件：無

規則：numeric_evaluation · 依賴：S10

葉節點依據：numeric_evaluation + matrix_product_def

交換順序：a=0、b=1、c=0，a'=1、b'=0、c'=0。第二項 ab'+bc'=0·0+1·0=0，所以乘積是零矩陣。



S13 · implies操作前

E_{11}E_{12}=(0,1,0)\neq(0,0,0)=E_{12}E_{11}

操作後

\exists a,b\in U:\ ab\neq ba\ \Rightarrow\ U\ \text{not commutative}

條件：無

規則：quantifier_negation · 依賴：S11, S12, G3, mko_comm_ring_def

葉節點依據：quantifier_negation + mko_comm_ring_def

兩個三元組的第二項 1≠0，所以 E₁₁E₁₂≠E₁₂E₁₁。交換律是全稱命題，一組失敗的有序對就足以否定：U 是有限含一環，但不是有限交換環。



S14 · implies操作前

IX=XI,\ E_{11}E_{22}=(0,0,0)=E_{22}E_{11},\ E_{11}E_{11}=E_{11}

操作後

\text{some pairs commute, yet}\ U\ \text{is not commutative}

條件：無

規則：quantifier_negation · 依賴：S10, S13, G3

葉節點依據：quantifier_negation + numeric_evaluation

U 中有許多對可交換：單位元 I 與每個元素交換；E₁₁E₂₂=(0,1·0+0·1,0)=(0,0,0)，E₂₂E₁₁=(0,0·0+0·0,0)=(0,0,0)；每個元素與自己交換。若只抽這些樣本，會誤以為 U 交換，但 S13 已給出反例。這正是 MKO 所說的「看到若干乘積可交換就宣稱整個環交換」的誤解。



S15 · implies操作前

\text{S07},\ \text{S08},\ \text{S09},\ \text{S13}

操作後

\mathbb{Z}_6\ \text{commutative, not a domain, not a field};\ U\ \text{not commutative}

條件：無

規則：and_intro_elim · 依賴：S07, S08, S09, S13

葉節點依據：and_intro_elim

合併：ℤ₆ 經 36 個有序對全部核對，是有限交換環；它有零因子 2、3，2 不可逆，所以不是整環或域。U 有可交換的樣本，但 E₁₁E₁₂≠E₁₂E₁₁，不是交換環。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S15 · sufficient_goal_reduction · S07, S08, S09, S13, and_intro_elim — 目標 G 是三個任務的合取；H 由 S07、S08、S09、S13 正向證得，H⇒G 由合取引入，沒有把 G 當作前提。
- S14 · premise_audit · S10, S13, numeric_evaluation — 樣本可交換與 S13 的反例不矛盾：全稱命題被一個反例否定，不被尚未窮盡定義域的正例樣本證明（N8）；若定義域有限且全部有序對都通過，完整窮舉就能建立該有限全稱命題。
- S13 · premise_audit · S11, S12, quantifier_negation — 否定全稱只需一個見證；這不影響 U 的含一環資格（G3）。
- S12 · inverse_equivalence · S10, numeric_evaluation — 精確計算，兩邊同一元素（N7）。
- S11 · inverse_equivalence · S10, numeric_evaluation — 精確計算，兩邊同一元素（N6）。
- S10 · inverse_equivalence · matrix_product_def, mul_zero — 三元組與上三角矩陣一一對應，公式只是同一乘積的另一種寫法，雙向成立。
- S09 · premise_audit · G1, domain_field_def — 否定存在需要核對所有 x；第 2 行列出了全部六個 x 的值（N5 在整個載體上重算）。
- S08 · premise_audit · G1, domain_field_def, numeric_evaluation — 一組零因子足以否定整環資格（N4）；交換性本身沒有被否定。
- S07 · sufficient_goal_reduction · S01, S02, S03, S05, case_analysis — 目標 G：ℤ₆ 交換。足夠條件 H：父環資格且所有 36 對可交換；H⇒G 由 S01 的定義。H 由 G2、S03、S05 正向證得，沒有用到 G。
- S06 · premise_audit · G1, S04, case_analysis — 15 組涵蓋全部非對角有序對（S02、S04）；N3 在全部 36 對上以公式重算，因載體恰為這六個元素，這個有限核對窮盡了所有對。
- S05 · premise_audit · mul_comm, mod_reduce, G1 — 此公式證書使用 G1 明示的運算定義 (ab) mod 6。S06 另核列出表格的 15 組非對角對稱等式，只證表格對稱，不是 36 個表格值逐項等於公式的核對；若要從任意獨立表格移交公式證書，須另驗證該一致性。
- S04 · inverse_equivalence · eq_refl_symm_trans — 等號對稱性雙向成立，所以兩個條件同真同假。
- S03 · premise_audit · eq_refl_symm_trans — 只用自反性；這 6 對不需要任何環的性質。
- S02 · inverse_equivalence · finite_counting_basics, numeric_evaluation — 對角與非對角是不交且窮盡的分割，6+30=36，兩邊是同一個集合（N1、N2）。
- S01 · premise_audit · G2, mko_comm_ring_def, mko_unital_ring_def — 此步只展開定義；若父環資格不成立，即使乘法表對稱也不能稱為交換環。





## 錯誤控制與反例

可交換的樣本不證明交換環MKO 指出的誤解是看到若干乘積可交換就宣稱整個環交換。U 中單位元、E₁₁ 與 E₂₂、每個元素與自身都可交換，但 E₁₁E₁₂≠E₁₂E₁₁。交換律必須量化所有有序對：ℤ₆ 用公式證書加 15 個等式涵蓋全部 36 對。

交換環不等於整環或域MKO 的另一個誤解是把交換環直接當整環或域。ℤ₆ 交換，但 2⊗3=0（零因子），且 2 不可逆。交換律只說 ab=ba，不說 ab=0 推出 a=0 或 b=0，也不給逆元。

表面對稱要逐項核對憑眼睛看表「大致對稱」不夠，抄錯一個數字就會改變結論。本稿用兩條獨立路線：S05 的公式證書，以及 S06 對列出的表逐組核對 15 個等式；N3 再在全部 36 對上重算公式。


- U 中 I 與所有元素交換，E₁₁ 與 E₂₂ 也交換，所以 U 是交換環 → reject — E₁₁E₁₂=E₁₂，E₁₂E₁₁=0，兩者不同。
- ℤ₆ 是交換環，所以沒有零因子 → reject — 2⊗3=0，而 2、3 都非零。
- ℤ₆ 是有限交換環，所以每個非零元都可逆 → reject — 第 2 行 (0,2,4,0,2,4) 中沒有 1，2 不可逆。
- 若乘法表的某一行與對應的列相同，就足以判定環交換 → reject — U 中單位元 I 的行與列相同，但 U 不交換；必須所有行都與對應的列相同。





## 結論與限制

ℤ₆ 的乘法對全部 36 個有序對都交換（6 個對角對由自反性，30 個非對角對由 15 個等式與公式證書），所以 ℤ₆ 是有限交換環；但 2⊗3=0 且 2 沒有乘法逆元，所以它不是整環也不是域。𝔽₂ 上的上三角矩陣環 U 中 I、E₁₁、E₂₂ 等樣本可交換，但 E₁₁E₁₂=E₁₂≠0=E₁₂E₁₁，所以 U 不是交換環。


- ℤ₆ 與 U 的有限含一環資格取自父節點（G2、G3），本稿未重新核對環公理。
- U 的完整 8×8 乘法表由 S10 的公式產生，本稿未逐格印出，只計算了用到的乘積。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 71ebaf592c6af1889ee73c2b6cda7d5ccfdbf9107995322905339d85c5f7b990
- original source SHA-256: 2aae99393024c2da54cb50cf7b82689e6617f3ce5fb9975a73db4ae5405b5182
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-finite-commutative-ring-01.json)