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

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

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

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



## 目標與範圍

給兩個完整運算表。（甲）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。





## 逐步主鏈

S01 · definition操作前

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

條件：無

規則：mko_finite_group_def · 依賴：G1, mko_finite_group_def

葉節點依據：mko_finite_group_def + group_axioms

依 MKO，(G,*) 是有限群需要四件事：封閉、對所有三元組結合、存在雙側單位元、每個元素有雙側逆元。交換律不在其中；表是否對稱與群無關。



S02 · implies操作前

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

操作後

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

條件：無

規則：finite_exhaustion · 依賴：G1, mod_notation

葉節點依據：finite_exhaustion + mod_notation + numeric_evaluation

逐行（row）比對 16 格：第 a 行是 a+0、a+1、a+2、a+3 除以 4 的餘數。例如第 1 行 1,2,3,4 的餘數是 1,2,3,0；第 2 行 2,3,4,5 的餘數是 2,3,0,1；第 3 行 3,4,5,6 的餘數是 3,0,1,2；第 0 行不變。16 格全部相符，所以表 T 就是 a*b=(a+b) mod 4。



S03 · implies操作前

a,b\in G

操作後

a*b\in G

條件：無

規則：finite_exhaustion · 依賴：G1, S02

葉節點依據：finite_exhaustion + division_algorithm

封閉：表 T 的 16 格輸出都在 {0,1,2,3} 中。也可由 S02 看出：餘數 r 滿足 0≤r<4，必為 0、1、2、3 之一。



S04 · implies操作前

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

操作後

x\bmod m=y\bmod m

條件：m>0

規則：L_same_rem · 依賴：division_algorithm, mod_notation

葉節點依據：division_algorithm + mod_notation

結合律的論證需要一個關於餘數的引理 L_same_rem：相差 m 的整數倍的兩個整數，除以 m 的餘數相同。證明在子步 S04.1、S04.2，只用除法演算法的存在與唯一性。



S05 · equivalent操作前

(a*b)*c

操作後

(a+b+c)\bmod 4

條件：a,b,c\in G

規則：L_same_rem · 依賴：S02, S04, division_algorithm

葉節點依據：L_same_rem + division_algorithm + eq_replace

由 S02，(a*b)*c=((a+b) mod 4 + c) mod 4。設 a+b=4q+r，r=(a+b) mod 4；則 (r+c)−(a+b+c)=r−(a+b)=−4q 是 4 的整數倍，依引理 L_same_rem（m=4），(r+c) mod 4=(a+b+c) mod 4。a、b、c 是 G 中任意元素。



S06 · equivalent操作前

a*(b*c)

操作後

(a+b+c)\bmod 4

條件：a,b,c\in G

規則：L_same_rem · 依賴：S02, S04, division_algorithm

葉節點依據：L_same_rem + division_algorithm + eq_replace

同理，a*(b*c)=(a+(b+c) mod 4) mod 4。設 b+c=4p+s，s=(b+c) mod 4；則 (a+s)−(a+b+c)=−4p，依引理得 (a+s) mod 4=(a+b+c) mod 4。



S07 · implies操作前

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

操作後

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

條件：無

規則：eq_refl_symm_trans · 依賴：S05, S06, G3

葉節點依據：eq_refl_symm_trans + forall_intro

兩邊都等於 (a+b+c) mod 4，依等號的傳遞得 (a*b)*c=a*(b*c)。S05、S06 對 G 中任意 a、b、c 成立，所以這一次論證涵蓋全部 4³=64 個有序三元組，符合 G3 的要求。N4 另外把 64 個三元組逐一窮舉作交叉核對；兩者都是對這個有限模型的完整核對，不是抽樣。



S08 · implies操作前

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

操作後

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

條件：無

規則：finite_exhaustion · 依賴：G1

葉節點依據：finite_exhaustion

第 0 行（row）是 0,1,2,3，表示 0*a=a 對四個 a 都成立（左單位）；第 0 列（column，每行的第一個數）依序是 0,1,2,3，表示 a*0=a（右單位）。左右都成立，0 是雙側單位元。



S09 · implies操作前

a\in G

操作後

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

條件：無

規則：finite_exhaustion · 依賴：G1, S08

葉節點依據：finite_exhaustion + numeric_evaluation

在每一行（row）找出值為單位元 0 的位置：0*0=0；1*3=0 且 3*1=0；2*2=0；3*1=0 且 1*3=0。每一對都檢查左右兩個乘積，所以 0、3、2、1 分別是 0、1、2、3 的雙側逆元。



S10 · implies操作前

\text{closure, associativity, identity, inverses}

操作後

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

條件：無

規則：mko_finite_group_def · 依賴：S03, S07, S08, S09

葉節點依據：mko_finite_group_def + and_intro_elim

S03、S07、S08、S09 分別給出四個條件，依 MKO 的定義，(G,*) 是有限群。



S11 · implies操作前

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

操作後

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

條件：無

規則：finite_exhaustion · 依賴：G2

葉節點依據：finite_exhaustion

逐格查候選乙的 9 格：輸出都在 {0,1,2}（封閉）；1∘2=1=2∘1，其餘對稱位置也相等（表對稱）；第 0 行（row）與第 0 列（column）都是 0,1,2（0 是雙側單位元）；0∘0=0、1∘1=0、2∘2=0（每個元素是自己的雙側逆元）。



S12 · implies操作前

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

操作後

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

條件：無

規則：case_analysis · 依賴：S11

葉節點依據：case_analysis + finite_counting_basics + numeric_evaluation

若三元組含 0，依位置分情形，每種情形都用 0 是雙側單位元：a=0 時兩邊都是 b∘c；b=0 時兩邊都是 a∘c；c=0 時兩邊都是 a∘b。這樣的三元組有 3³−2³=27−8=19 個，全部通過。所以若只抽查含單位元的三元組，會誤以為 ∘ 結合。



S13 · implies操作前

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

操作後

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

條件：無

規則：def_unfold · 依賴：G2

葉節點依據：def_unfold + numeric_evaluation

查表：1∘1=0，所以 (1∘1)∘2=0∘2=2；1∘2=1，所以 1∘(1∘2)=1∘1=0。2≠0，三元組 (1,1,2) 違反結合律。



S14 · implies操作前

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

操作後

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

條件：無

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

葉節點依據：quantifier_negation + mko_finite_group_def

群需要對所有三元組結合；S13 給出反例，依量詞否定這個全稱命題為假，所以 (K,∘) 不是群。這發生在 S11 的對稱、單位元與逆元全部通過、S12 的 19 個三元組也全部通過之後：只看表的對稱或少數案例會誤判。







## 局部子步與引理

S04.1 · theorem_application操作前

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

操作後

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

條件：m>0

規則：division_algorithm · 依賴：division_algorithm, mod_notation

葉節點依據：division_algorithm + mod_notation

對 x 與正整數 m 使用除法演算法：存在整數 q 與 r，使 x=mq+r 且 0≤r<m；依記號，r=x mod m。



S04.2 · implies操作前

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

操作後

y\bmod m=r=x\bmod m

條件：q-k\in\mathbb{Z}

規則：division_algorithm · 依賴：S04.1, division_algorithm

葉節點依據：division_algorithm + distributive + eq_replace

由 x−y=mk 得 y=x−mk=mq+r−mk=m(q−k)+r。q−k 是整數且 0≤r<m，所以 (q−k, r) 正是 y 除以 m 的商與餘數；依除法演算法的唯一性，y mod m=r=x mod m。S04.1 與 S04.2 合起來證得引理 L_same_rem。







## 逐步反向審查


- 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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-finite-group-01.json)