# 有限阿貝爾群：由完整 Cayley 表先核群資格、再核交換性

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

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

derivation-mko-finite-abelian-group-01 · production-20261019-adopted-96



## 目標與範圍

載體 G={0,1,2,3} 上給出完整的 4×4 Cayley 表（行 a、列 b 的格子是 a*b）：第 0 行 (1,2,3,0)，第 1 行 (2,3,0,1)，第 2 行 (3,0,1,2)，第 3 行 (0,1,2,3)。依序核對封閉、結合、唯一單位元與逆元，再對所有 a、b 核對 a*b=b*a，判定 (G,*) 是否為有限阿貝爾群；求元素 0 與 1 的階與它們生成的循環子群；並以 {0,1,2} 上的對稱表 a∘b=|a−b| 說明「表對稱」不能代替群資格。

停在 MKO 的切片內：載體標籤 0 到 n−1（此處 n=4）與完整的 n×n 表，只分類明示給出的有限表。用模 4 算術給出全稱證明，並把對整個載體的窮舉核對作為交叉核對。不涉及有限阿貝爾群的結構定理或其他群；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- group_axioms
- add_comm
- add_assoc
- forall_intro
- quantifier_negation
- abs_rules


- G1 — 載體 G={0,1,2,3}，標籤為 0 到 n−1，n=4。
- G2 — 完整的 Cayley 表（行 a、列 b 的格子是 a*b）：第 0 行 (1,2,3,0)；第 1 行 (2,3,0,1)；第 2 行 (3,0,1,2)；第 3 行 (0,1,2,3)。
- G3 — 對照表：載體 K={0,1,2}，a∘b=|a−b|，即第 0 行 (0,1,2)、第 1 行 (1,0,1)、第 2 行 (2,1,0)。


- G=\{0,1,2,3\} — 載體（標籤）
- a*b — 表中第 a 行第 b 列的格子
- x\bmod 4 — x 除以 4 的餘數，取值 0 到 3
- e — 單位元（此表中 e=3）
- a^k,\ \operatorname{ord}(a) — a 的 k 次方與 a 的階
- \langle a\rangle — a 生成的循環子群





## 規則與來源


- group_axioms · prerequisite — 群公理：集合 G 配二元運算，滿足結合律、有單位元 e（eg=ge=g）、每個元素 g 有反元素 g⁻¹（gg⁻¹=g⁻¹g=e）。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- abs_rules · prerequisite — 絕對值（實數）：|u|=u（u≥0）、|u|=−u（u<0）；|u|≥0；|uv|=|u||v|；三角不等式 |u+v|≤|u|+|v|；|u|<r ⇔ −r<u<r。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_fag · cited — 有限阿貝爾群先須以完整 Cayley 表通過封閉、結合、唯一單位元與逆元資格，再對所有 a、b 核 a*b=b*a。本輪只分類明示有限表；不由幾個樣本或生成元看似交換外推整群交換。 · mko-finite-abelian-group
- table_read · prerequisite — 讀表：a*b 是明示 Cayley 表第 a 行第 b 列的格子；表完整表示每一對 (a,b) 都有恰好一個格子。
- mod_arith · prerequisite — 模 n 算術（n≥1）：x mod n 是唯一滿足 0≤r≤n−1 且 n∣(x−r) 的整數 r。x≡y (mod n) 表示 n∣(x−y)；它是等價關係且與加法相容；x mod n≡x；兩個都在 0 到 n−1 之間且模 n 同餘的整數相等。
- power_def · prerequisite — 群中的冪與階：a¹=a，a^(k+1)=a^k*a；a 的階是使 a^k=e 的最小正整數 k；⟨a⟩ 是 a 的所有冪組成的集合。
- L_id_unique · lemma — 若 e 與 e′ 都是運算 * 的雙邊單位元，則 e=e′。





## 逐步主鏈

S01 · definition操作前

(G,*)\ \text{finite abelian group}

操作後

\text{closure}\land\text{assoc}\land\text{unique } e\land\text{inverses},\ \text{then}\ \forall a,b:\ a*b=b*a

條件：無

規則：mko_fag · 依賴：mko_fag, group_axioms

葉節點依據：mko_fag + def_unfold

依 MKO，分類分兩階段：先用完整表核群資格（封閉、結合、唯一單位元、逆元），全部通過後才核交換性 a*b=b*a 對所有 a、b。順序不能顛倒：交換性只對已是群的結構才構成「阿貝爾群」。



S02 · equivalent操作前

a*b\ \text{read from the table}

操作後

a*b=(a+b+1)\bmod 4\ \text{for all 16 pairs}

條件：無

規則：table_read · 依賴：G1, G2, table_read, mod_arith

葉節點依據：table_read + mod_arith + numeric_evaluation

逐格比較：第 a 行依 b=0,1,2,3 列出 a+1、a+2、a+3、a+4 除以 4 的餘數。例如第 0 行 1,2,3,4 mod 4=0，得 (1,2,3,0)；第 2 行 3,4,5,6 的餘數為 (3,0,1,2)。四行共 16 格全部與 (a+b+1) mod 4 相符。這是對完整表的窮舉比較，不是抽樣；之後可用模算術對所有元素同時論證。



S03 · implies操作前

a,b\in G

操作後

a*b=(a+b+1)\bmod 4\in\{0,1,2,3\}=G

條件：無

規則：mod_arith · 依賴：S02, mod_arith

葉節點依據：mod_arith + forall_intro

封閉：除以 4 的餘數一定在 0 到 3 之間，所以每個 a*b 都在 G 中。直接看表也一樣：16 個格子都是 0、1、2、3 之一。



S04 · implies操作前

(a*b)*c,\ a*(b*c)

操作後

(a*b)*c=a*(b*c)\ \text{for all } a,b,c\in G

條件：無

規則：mod_arith · 依賴：S02, S03, mod_arith

葉節點依據：mod_arith + add_assoc + add_comm + forall_intro

結合律對 64 組 (a,b,c) 都要成立。不逐一列舉，而用模算術一次證明：兩邊都與 a+b+c+2 模 4 同餘（S04.1、S04.2），而且都在 0 到 3 之間，所以相等（S04.3）。N3 再對全部 64 組做窮舉交叉核對。



S05 · implies操作前

3*b,\ a*3

操作後

3*b=(b+4)\bmod 4=b,\ a*3=(a+4)\bmod 4=a

條件：無

規則：mod_arith · 依賴：S02, mod_arith

葉節點依據：mod_arith + forall_intro

取 e=3：3*b=(3+b+1) mod 4=(b+4) mod 4=b，因為 b 在 0 到 3 之間且 b+4≡b；同樣 a*3=a。表中第 3 行 (0,1,2,3) 與第 3 列都重現標籤，與此一致。注意單位元是 3，不是標籤 0：0*0=1≠0。



S06 · implies操作前

e=3\ \text{is an identity}

操作後

e=3\ \text{is the unique identity}

條件：無

規則：L_id_unique · 依賴：S05, L_id_unique

葉節點依據：L_id_unique

MKO 要求單位元唯一。依引理 L_id_unique（S06.1 證明），任何另一個雙邊單位元 e′ 都等於 3。



S07 · implies操作前

a\in G

操作後

a^{-1}=(2-a)\bmod 4:\ 0\leftrightarrow 2,\ 1\leftrightarrow 1,\ 3\leftrightarrow 3

條件：無

規則：mod_arith · 依賴：S02, S05, mod_arith

葉節點依據：mod_arith + forall_intro

對 b=(2−a) mod 4：a*b≡a+(2−a)+1=3 (mod 4)，而 a*b 在 0 到 3 之間，所以 a*b=3=e；同樣 b*a=3。具體：0*2=3、1*1=3、2*0=3、3*3=3，與表相符。每個元素都有逆元。



S08 · implies操作前

\text{closure, associativity, unique } e,\ \text{inverses}

操作後

(G,*)\ \text{is a group}

條件：無

規則：group_axioms · 依賴：S03, S04, S06, S07, group_axioms

葉節點依據：group_axioms + and_intro_elim

群資格的四項都已證明（S03、S04、S06、S07），依群公理 (G,*) 是群。到這裡才進入第二階段。



S09 · implies操作前

a*b=(a+b+1)\bmod 4

操作後

a*b=(b+a+1)\bmod 4=b*a\ \text{for all } a,b\in G

條件：無

規則：add_comm · 依賴：S02, S08, add_comm

葉節點依據：add_comm + forall_intro

整數加法可交換，a+b+1=b+a+1，所以 a*b=b*a；a、b 任意，涵蓋全部 16 對（包括 6 個非對角的無序對），而非只看幾個樣本。等價地說，在行與列用同一順序排行時，表對主對角線對稱；但這個對稱只有在 S08 的群資格之後才代表阿貝爾群。



S10 · implies操作前

(G,*)\ \text{group},\ \forall a,b:\ a*b=b*a

操作後

(G,*)\ \text{is a finite abelian group of order } 4

條件：無

規則：mko_fag · 依賴：S08, S09, mko_fag

葉節點依據：mko_fag + and_intro_elim

兩階段都通過：(G,*) 是群（S08），且所有元素兩兩交換（S09）。依 MKO，(G,*) 是有限阿貝爾群，階數 |G|=4。



S11 · implies操作前

0^1=0

操作後

0^2=0*0=1,\ 0^3=1*0=2,\ 0^4=2*0=3=e;\ \operatorname{ord}(0)=4

條件：無

規則：power_def · 依賴：S02, S05, power_def

葉節點依據：power_def + table_read

依冪的定義用同一個群運算計算：0²=0*0=1，0³=0²*0=1*0=2，0⁴=0³*0=2*0=3=e。0¹、0²、0³ 都不等於 e=3，所以 0 的階是 4。階必須相對於單位元 3 計算，而不是標籤 0（MKO para1）。



S12 · implies操作前

\langle 0\rangle,\ 1^2=1*1

操作後

\langle 0\rangle=\{0,1,2,3\}=G;\ 1^2=3=e,\ \operatorname{ord}(1)=2,\ \langle 1\rangle=\{1,3\}

條件：無

規則：power_def · 依賴：S11, S02, S05, power_def

葉節點依據：power_def + table_read

0 的冪是 0、1、2、3 後又循環回來，所以 ⟨0⟩=G，這張表定義的群是循環群。另一方面 1¹=1≠e，1²=1*1=3=e，所以 1 的階是 2，⟨1⟩={1,3}。標籤 1 並不是生成元；這些子群只屬於這個指定的有限群（MKO para2）。



S13 · implies操作前

a\circ b=|a-b|\ \text{on}\ K=\{0,1,2\}

操作後

(1\circ 1)\circ 2=2\neq 0=1\circ(1\circ 2);\ (K,\circ)\ \text{is not a group}

條件：無

規則：quantifier_negation · 依賴：G3, abs_rules, quantifier_negation

葉節點依據：quantifier_negation + abs_rules + numeric_evaluation

對照表：|a−b|=|b−a|，所以表對角線對稱；0 是單位元（|0−b|=b）；每個元素是自己的逆（a∘a=0）。但 (1∘1)∘2=0∘2=2，而 1∘(1∘2)=1∘1=0，結合律失敗。一組反例就否定「對所有三元組結合」，所以 (K,∘) 不是群，自然也不是阿貝爾群。表對稱不能代替群資格。







## 局部子步與引理

S04.1 · implies操作前

(a*b)*c=\big((a*b)+c+1\big)\bmod 4

操作後

(a*b)*c\equiv(a+b+1)+c+1=a+b+c+2\pmod 4

條件：無

規則：mod_arith · 依賴：S02, mod_arith, add_assoc

葉節點依據：mod_arith + add_assoc + add_comm

依公式 (a*b)*c=((a*b)+c+1) mod 4，它與 (a*b)+c+1 同餘；又 a*b≡a+b+1，同餘與加法相容，所以 (a*b)*c≡a+b+1+c+1=a+b+c+2 (mod 4)。



S04.2 · implies操作前

a*(b*c)=\big(a+(b*c)+1\big)\bmod 4

操作後

a*(b*c)\equiv a+(b+c+1)+1=a+b+c+2\pmod 4

條件：無

規則：mod_arith · 依賴：S02, mod_arith, add_assoc

葉節點依據：mod_arith + add_assoc

同理，a*(b*c)≡a+(b*c)+1≡a+(b+c+1)+1=a+b+c+2 (mod 4)。



S04.3 · implies操作前

(a*b)*c\equiv a*(b*c)\pmod 4,\ \text{both in}\ \{0,1,2,3\}

操作後

(a*b)*c=a*(b*c)

條件：無

規則：mod_arith · 依賴：S04.1, S04.2, S03, mod_arith

葉節點依據：mod_arith

同餘的傳遞性給出 (a*b)*c≡a*(b*c)；依 S03 兩者都在 0 到 3 之間，兩個在此範圍內且同餘的整數相等。



S06.1 · implies操作前

e,\ e'\ \text{two-sided identities}

操作後

e=e*e'=e'

條件：無

規則：eq_refl_symm_trans · 依賴：eq_refl_symm_trans

葉節點依據：eq_refl_symm_trans + def_unfold

因 e′ 是單位元，e*e′=e；因 e 是單位元，e*e′=e′。依等號的對稱與傳遞，e=e′。這證明了引理 L_id_unique，對任何二元運算都成立，不需要結合律。







## 逐步反向審查


- S13 · premise_audit · G3, abs_rules, quantifier_negation — 否證只需一組三元組；不宣稱其他三元組也失敗。
- S12 · premise_audit · S11, power_def, table_read — 需要表的值與 e=3；不宣稱任何關於其他群的結論。
- S11 · premise_audit · S02, S05, power_def — 需要表的值與 e=3；最小性由逐一核對 k=1、2、3 得到。
- S10 · premise_audit · S08, S09, mko_fag — 只合取兩階段的結論；分類只關於這一張明示表。
- S09 · premise_audit · S02, S08, add_comm, forall_intro — 需要對所有 a、b 成立的公式；只檢查例如 0*1=1*0 與 0*2=2*0 兩個樣本不夠。
- S08 · premise_audit · S03, S04, S06, S07, group_axioms, and_intro_elim — 四項缺一不可；交換性尚未使用。
- S07 · premise_audit · S02, S05, mod_arith — 逆元以 S05 的 e=3 為準；若誤用標籤 0 當單位元，會找錯逆元。
- S06.1 · premise_audit · eq_refl_symm_trans — 只用兩個單位元的定義與等號性質；不使用 L_id_unique 本身。
- S06 · premise_audit · S05, L_id_unique — 需要 S05 的存在性與引理的唯一性。
- S05 · premise_audit · S02, mod_arith, forall_intro — 雙邊都要核（左乘與右乘）；本步兩邊都核了。
- S04.3 · premise_audit · S04.1, S04.2, S03, mod_arith — 關鍵是兩邊都已化成餘數；只有同餘而不在 0 到 3 之間的數不一定相等。
- S04.2 · premise_audit · mod_arith, add_assoc — 與 S04.1 對稱。
- S04.1 · premise_audit · mod_arith, add_assoc — 只用同餘的性質與加法結合律。
- S04 · premise_audit · S02, S03, mod_arith, forall_intro — 需要 S02 的公式；a、b、c 任意，所以是全稱結論。
- S03 · premise_audit · S02, mod_arith — 需要 S02 的公式與餘數的範圍；不宣稱反向。
- S02 · inverse_equivalence · table_read, mod_arith, G2 — 公式在 16 對上產生的值恰好就是表；由公式重算表或由表讀回公式值，兩者一致。
- S01 · premise_audit · mko_fag, group_axioms — 此步只列出義務，不推出新事實。





## 錯誤控制與反例

表對稱不足以判定阿貝爾群MKO 指出的誤解是因表對角線對稱就宣稱阿貝爾群。|a−b| 的表對稱、有單位元 0、每個元素自逆，但 (1∘1)∘2=2≠0=1∘(1∘2)，不是群（S13）。必須先完成群資格（S03 至 S08），交換性才有分類意義。

幾個交換樣本不夠MKO 的另一個誤解是由幾個元素交換外推整群交換。S09 用對所有 a、b 成立的公式。反例模式：在 {1,2,3} 的置換群中，r=(1 2 3) 與 r² 交換、單位元與一切交換，但 s=(1 2) 與 r 不交換：(r∘s)(1)=r(2)=3，而 (s∘r)(1)=s(2)=1。

單位元不一定是標籤 0標籤 0 到 n−1 只是名字。此表的單位元是 3（0*0=1≠0）。若誤把 0 當單位元，會找錯逆元，也會算錯階：例如以 0 為單位元時 0 的階會被誤判為 1。


- {0,1,2} 上 |a−b| 的表對主對角線對稱，所以它是阿貝爾群 → reject — 結合律失敗：(1∘1)∘2=2，1∘(1∘2)=0。
- 由 0*1=1*0 與 0*2=2*0 兩個樣本即可推出 (G,*) 交換 → reject — 兩個樣本不涵蓋其餘四個非對角無序對；結論要靠 S09 對所有 a、b 的論證。
- 標籤 0 是這個群的單位元 → reject — 0*0=1≠0；單位元是 3。
- 元素 1 生成整個群 G → reject — 1*1=3=e，所以 ⟨1⟩={1,3}≠G。





## 結論與限制

給定的 4×4 表就是 a*b=(a+b+1) mod 4。它封閉、結合（兩邊都與 a+b+c+2 模 4 同餘）、有唯一單位元 e=3、每個 a 有逆元 (2−a) mod 4，且對所有 a、b 交換，所以 (G,*) 是 4 階有限阿貝爾群。元素 0 的階為 4，⟨0⟩=G；元素 1 的階為 2，⟨1⟩={1,3}。對照的對稱表 |a−b| 在 {0,1,2} 上不結合，不是群。


- N1 至 N9 是對載體 {0,1,2,3} 的每個元素（或每對、每組三元組）做的有限窮舉核對。因為載體恰有這四個元素，它們涵蓋這一張表的所有情形；它們是 S03 至 S09 模算術證明的交叉核對，對其他表不說明任何事。
- 錯誤控制中的置換群反例沒有寫成完整 6×6 表，只用置換合成計算一組不交換的元素。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 8364c2e3fd58e2b9251219c8186c64a27ff0c6e88d59156b8ccb03f562a4beda
- original source SHA-256: 8364c2e3fd58e2b9251219c8186c64a27ff0c6e88d59156b8ccb03f562a4beda
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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