有限群：以完整 Cayley 表核對群公理

目標與範圍

給兩個完整運算表。（甲）G={0,1,2,3} 配上表 T，證明 (G,*) 是有限群：封閉、全部 4³=64 個三元組的結合律、雙側單位元、雙側逆元。（乙）K={0,1,2} 配上表 ∘：它對稱、有雙側單位元、每個元素都有雙側逆元，卻在三元組 (1,1,2) 違反結合律，因此不是群；同時說明含 0 的 19 個三元組全部通過，抽樣會誤判。

只處理題目給定的有限模型：元素標為 0 到 n−1、運算由完整 n×n 表給出（MKO 假設 a1）。結合律以涵蓋全部三元組的論證完成，並以窮舉全部 n³ 個三元組作獨立交叉核對（MKO 假設 a2）。不處理子群、同態或無限群；不改動 canonical MKO 或英文 edition。

已知條件與符號

• division_algorithm
• eq_refl_symm_trans
• case_analysis
• numeric_evaluation

• G1 — 候選甲：G={0,1,2,3}，運算表 T 的第 a 行（row）依序列出 a*0、a*1、a*2、a*3：第 0 行 0,1,2,3；第 1 行 1,2,3,0；第 2 行 2,3,0,1；第 3 行 3,0,1,2。
• G2 — 候選乙：K={0,1,2}，運算表的第 a 行（row）依序列出 a∘0、a∘1、a∘2：第 0 行 0,1,2；第 1 行 1,0,1；第 2 行 2,1,0。
• G3 — 抽樣行（row）或少數三元組不證群；結合律必須對全部 n³ 個有序三元組成立（MKO 假設 a2）。

• G=\{0,1,2,3\} — 候選甲的載體
• a*b — 表 T 中第 a 行（row）第 b 列（column）的值
• K=\{0,1,2\} — 候選乙的載體
• a\circ b — 表 ∘ 中第 a 行（row）第 b 列（column）的值
• x\bmod m — x 除以正整數 m 的餘數，0≤r<m

規則與來源

• division_algorithm · prerequisite — 帶餘除法：對整數 a 與正整數 b，存在唯一的整數 q、r 使 a=bq+r 且 0≤r<b。
• eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• group_axioms · prerequisite — 群公理：集合 G 配二元運算，滿足結合律、有單位元 e（eg=ge=g）、每個元素 g 有反元素 g⁻¹（gg⁻¹=g⁻¹g=e）。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• mko_finite_group_def · cited — 有限集合 G 配備二元運算 *。若運算對 G 封閉、對所有三元組結合、存在雙側單位元且每元素有雙側逆元，則 (G,*) 為有限群。完整 Cayley 表可窮舉核對指定有限模型。 · mko-finite-group
• mod_notation · prerequisite — 對整數 x 與正整數 m，x mod m 表示除法演算法中的餘數 r：即唯一滿足 0≤r<m 且 x=mq+r（q 為整數）的 r。
• finite_exhaustion · prerequisite — 在有限集合上，對全部元素（或全部有序對、三元組）的命題成立，當且僅當它在列出的每一個情形都成立；逐一核完每個情形是該有限模型的完整證明，但不推及其他集合。
• L_same_rem · lemma — 設 m 為正整數、x、y 為整數。若 x−y=mk（k 為整數），則 x mod m=y mod m。

逐步主鏈

(G,*)\ \text{given by table } T

\text{closure},\ \forall a,b,c:\ (a*b)*c=a*(b*c),\ \exists e\ \text{two-sided identity},\ \forall a\ \exists a'\ \text{two-sided inverse}

T(a,b)\ \text{for all } a,b\in G

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

a,b\in G

a*b\in G

x-y=mk,\ k\in\mathbb{Z}

x\bmod m=y\bmod m

(a*b)*c

(a+b+c)\bmod 4

a*(b*c)

(a+b+c)\bmod 4

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

\forall a,b,c\in G:\ (a*b)*c=a*(b*c)

\text{row } 0 \text{ and column } 0 \text{ of } T

\forall a\in G:\ 0*a=a\ \land\ a*0=a

a\in G

0'=0,\ 1'=3,\ 2'=2,\ 3'=1;\ a*a'=a'*a=0

\text{closure, associativity, identity, inverses}

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

(K,\circ)\ \text{given by its table}

\text{closed},\ a\circ b=b\circ a,\ 0\ \text{two-sided identity},\ a\circ a=0

(a,b,c)\in K^3,\ 0\in\{a,b,c\}

(a\circ b)\circ c=a\circ(b\circ c)

(1\circ 1)\circ 2\ \text{vs}\ 1\circ(1\circ 2)

0\circ 2=2\neq 0=1\circ 1

\exists (a,b,c):\ (a\circ b)\circ c\neq a\circ(b\circ c)

(K,\circ)\ \text{is not a group}

局部子步與引理

x\in\mathbb{Z},\ m>0

x=mq+r,\ 0\le r<m,\ r=x\bmod m

y=x-mk=m(q-k)+r,\ 0\le r<m

y\bmod m=r=x\bmod m

逐步反向審查

• S14 · sufficient_goal_reduction · S13, quantifier_negation, mko_finite_group_def — 目標 G：(K,∘) 不是群。足夠條件 H：某個三元組違反結合律（H⇒G 由定義）。H 由 S13 直接查表得到，沒有把 G 當作前提。
• S13 · premise_audit · G2, def_unfold, numeric_evaluation — 四次查表都可在 G2 直接核對；一個反例就足以否定全稱的結合律。
• S12 · premise_audit · S11, case_analysis — 三種情形可能重疊（例如兩個 0），但都涵蓋到；此步只宣稱含 0 的三元組，不涉及其餘 8 個。
• S11 · premise_audit · G2, finite_exhaustion — 這些性質都由逐格檢查得到；它們都不涉及三元組，所以對結合律沒有任何保證。
• S10 · sufficient_goal_reduction · S03, S07, S08, S09, mko_finite_group_def — 目標 G：(G,*) 是群。足夠條件 H：四個條件同時成立；H⇒G 由定義。H 的每一部分都由表 T 正向證成，沒有把 G 當作前提。
• S09 · premise_audit · G1, S08, finite_exhaustion — 逆元的定義依賴 S08 的單位元，且必須左右乘都得到同一個單位元；四個元素逐一核完。
• S08 · premise_audit · G1, finite_exhaustion — 必須同時查對應的行（row）與列（column）；只查一邊只能得到單側單位元（見錯誤控制三）。
• S07 · premise_audit · S05, S06, eq_refl_symm_trans, forall_intro — ∀ 引入要求 a、b、c 沒有被特別取值；S05、S06 確實沒有。結合律與交換律不同，此步沒有用到 a*b=b*a。
• S06 · inverse_equivalence · S02, L_same_rem, eq_replace — 與 S05 相同，是相等式子的互換，雙向成立。
• S05 · inverse_equivalence · S02, L_same_rem, eq_replace — 兩邊是同一個整數的兩種寫法；把相等的式子互換，兩個方向都成立。
• S04.2 · premise_audit · S04.1, division_algorithm, distributive — 關鍵是唯一性：若沒有唯一性，y 可能有另一種寫法給出不同的餘數。0≤r<m 的界由 S04.1 帶入。
• S04.1 · premise_audit · division_algorithm, mod_notation — 除法演算法要求除數為正整數，條件 m>0 正是為此。
• S04 · premise_audit · L_same_rem — 引理需要 m>0 與 k 為整數；此處只宣稱這個方向，反向（餘數相同推出差為 m 的倍數）雖然也成立，但本稿不需要也不使用。
• S03 · premise_audit · G1, finite_exhaustion, division_algorithm — 封閉只要求每格輸出仍屬於 G；它本身不推出結合律或單位元。
• S02 · premise_audit · G1, finite_exhaustion, mod_notation — 公式只是表的另一種寫法，靠的是 16 格逐一相符；這只對表 T 成立，不宣稱任何表都能寫成這種公式。
• S01 · premise_audit · G1, mko_finite_group_def — 此步只列出要核的條件，不推出新事實。四個條件缺一不可，之後逐一核對。

錯誤控制與反例

對稱的表不等於群

MKO 指出的誤解是只看表的對稱性就宣稱是群。對稱只表示交換律，而交換律不是群公理，也不推出結合律。候選乙的表完全對稱、有單位元與逆元，仍在 (1,1,2) 違反結合律。

抽樣三元組不夠

候選乙的 27 個三元組中，含 0 的 19 個全部通過（S12）。抽查幾個三元組很可能全部落在這 19 個之中而誤判。結合律必須涵蓋全部 n³ 個三元組：本稿以對任意 a、b、c 成立的論證（S05 到 S07）涵蓋候選甲，並以 N4 窮舉 64 個三元組交叉核對。

單側單位元或逆元

MKO 也提醒不要把單側單位元或逆元當雙側。例：在 {0,1,2} 上令 a•b=(a−b) mod 3。對每個 a，a•0=a，所以 0 是右單位元；但 0•1=2≠1，0 不是左單位元，因此沒有雙側單位元。S08 必須同時查第 0 行（row）與第 0 列（column），S09 必須同時查 a*a' 與 a'*a。

• 候選乙的表對稱，且有單位元與逆元，所以 (K,∘) 是群 → reject — 結合律在 (1,1,2) 失敗：(1∘1)∘2=2，1∘(1∘2)=0。
• 已核 (0,1,2)、(1,0,2)、(2,1,0)、(1,2,0) 四個三元組都結合，所以 ∘ 結合 → reject — 這四個三元組都含 0，必然通過；不含 0 的 (1,1,2) 失敗。若要肯定結合律，論證必須涵蓋全部 27 個三元組。
• 在 {0,1,2} 上 a•b=(a−b) mod 3，因為 a•0=a 對所有 a 成立，所以 0 是單位元 → reject — 0 只是右單位元：0•1=2≠1。
• 只要每行（row）每列（column）都是集合的一個排列（拉丁方），運算表就定義一個群 → reject — (a−b) mod 3 的表是拉丁方，但 (0•1)•1=2•1=1，而 0•(1•1)=0•0=0。

結論與限制

候選甲 (G,*) 的表就是 a*b=(a+b) mod 4；它封閉，全部 64 個三元組結合，0 是雙側單位元，0、1、2、3 的雙側逆元分別是 0、3、2、1，所以是有限群。候選乙 (K,∘) 封閉、對稱、以 0 為雙側單位元且每個元素自逆，含 0 的 19 個三元組也都結合，但 (1∘1)∘2=2≠0=1∘(1∘2)，所以不是群。

• 結論只屬於兩個指定的有限模型（MKO 假設 a2）；本稿不處理子群、同態、陪集等（MKO 的 formal next）。
• N4 是對候選甲全部 64 個三元組的有限窮舉，對這個模型是完整的，但它依賴 S02 的公式重現表 T；S05 到 S07 的論證不依賴 N4。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: df045187fbff83ea6ba906772f9d4bccd3acd1bc60dcb87c4028857733f76d42
• original source SHA-256: df045187fbff83ea6ba906772f9d4bccd3acd1bc60dcb87c4028857733f76d42
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）