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

目標與範圍

載體 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′。

逐步主鏈

(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

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

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

a,b\in G

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

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

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

3*b,\ a*3

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

e=3\ \text{is an identity}

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

a\in G

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

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

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

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

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

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

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

0^1=0

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

\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\}

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}

局部子步與引理

(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

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

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

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

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

e=e*e'=e'

逐步反向審查

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