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

目標與範圍

（一）在已通過有限含一環資格的 ℤ₆={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 且無零因子的交換環；域是每個非零元都有乘法逆元的交換環。

逐步主鏈

\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

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

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

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

a\otimes a=a\otimes a

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}

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)

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

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

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

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

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}

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

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

\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

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}

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)

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}

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}

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

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

局部子步與引理

本稿無局部子步。

逐步反向審查

• 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、反控制與修訂記錄）