# 有限含一環：證明模 4 的加法表與乘法表構成含一環

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

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

derivation-mko-finite-unital-ring-01 · production-20261019-adopted-96



## 目標與範圍

在載體 X={0,1,2,3} 上給定完整的加法表 ⊕ 與乘法表 ⊙（即模 4 的加法與乘法）。對所有元素對與三元組證明：(X,⊕) 是阿貝爾群；⊙ 結合；⊙ 對 ⊕ 左右分配；存在唯一的雙側乘法單位元 1，且 1≠0。並指出 2⊙2=0 不妨礙它是含一環。

只在 MKO 的範圍內：載體標籤 0 到 3、兩個 4×4 運算表完整（假設 a1）；資格對全部元素對與三元組精確成立（假設 a2）。主證明先核對 32 個表格項等於模 4 公式，再以「模運算相容」引理對所有三元組一次證明公理；N4 到 N7 另對全部 64 個三元組作窮舉交叉核對。不要求乘法交換，不處理整環、域、理想或商環；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- division_algorithm
- group_axioms
- distributive
- finite_forall


- G1 — 加法表 ⊕（行 a、列 b）：第 0 行 0,1,2,3；第 1 行 1,2,3,0；第 2 行 2,3,0,1；第 3 行 3,0,1,2。
- G2 — 乘法表 ⊙（行 a、列 b）：第 0 行 0,0,0,0；第 1 行 0,1,2,3；第 2 行 0,2,0,2；第 3 行 0,3,2,1。
- G3 — r(m) 表示整數 m 除以 4 的餘數：依除法演算法 m=4q+r(m)、0≤r(m)<4，q、r(m) 唯一。


- X — 載體 {0,1,2,3}
- a\oplus b,\ a\odot b — 加法表與乘法表給出的運算
- r(m) — 整數 m 除以 4 的餘數，0≤r(m)<4
- 0,\ 1 — 加法單位元與乘法單位元
- \ominus a — a 的加法逆元





## 規則與來源


- division_algorithm · prerequisite — 帶餘除法：對整數 a 與正整數 b，存在唯一的整數 q、r 使 a=bq+r 且 0≤r<b。
- 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。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- mko_ring_def · cited — 在同一有限載體X上給完整加法表與乘法表。加法須為阿貝爾群；乘法須結合；乘法對加法左右分配；並存在唯一乘法單位元1且1不等於加法單位元0。本輪不要求乘法交換。 · mko-finite-unital-ring
- finite_forall · prerequisite — 有限全稱：對有限集合 D，「對所有 t∈D，Φ(t)」等價於把 D 的每個元素逐一代入所得命題的合取；列表必須完整。
- L_mod_compat · lemma — 對所有整數 m、k：r(m+k)=r(r(m)+r(k))，且 r(mk)=r(r(m)r(k))。
- L_unique_identity · lemma — 若 e 與 e′ 都是 ⊙ 的雙側單位元，則 e=e′。





## 逐步主鏈

S01 · definition操作前

(X,\oplus,\odot)\ \text{finite unital ring}

操作後

(X,\oplus)\ \text{abelian group};\ \odot\ \text{associative};\ \text{left and right distributive};\ \exists!\,1,\ 1\neq 0

條件：無

規則：mko_ring_def · 依賴：G1, G2

葉節點依據：mko_ring_def + def_unfold

依 MKO 列出全部責任：加法是阿貝爾群（封閉、結合、單位元 0、逆元、交換）；乘法結合；乘法對加法左分配與右分配分開核；存在唯一的雙側乘法單位元 1，且 1≠0。乘法交換不是責任之一。



S02 · implies操作前

\text{the 32 entries of the two tables}

操作後

a\oplus b=r(a+b),\ a\odot b=r(ab)\ \text{for all}\ a,b\in X

條件：無

規則：finite_forall · 依賴：G1, G2, G3, finite_forall

葉節點依據：finite_forall + division_algorithm + numeric_evaluation

逐格比對 16+16 個表格項與公式。例如乘法第 3 行：3·0=0、3·1=3、3·2=6 餘 2、3·3=9 餘 1，與表中 0,3,2,1 相同；第 2 行：0、2、4 餘 0、6 餘 2；加法第 3 行：3、4 餘 0、5 餘 1、6 餘 2。全部 32 格都相符，所以兩個表格運算恰是模 4 的加法與乘法。



S03 · theorem_application操作前

m,\ k\in\mathbb{Z}

操作後

r(m+k)=r(r(m)+r(k)),\ r(mk)=r(r(m)r(k))

條件：無

規則：L_mod_compat · 依賴：G3

葉節點依據：L_mod_compat

引理 L_mod_compat（S03.1 到 S03.3 證明）說明：先取餘再運算再取餘，與直接運算後取餘相同。之後每條公理都化成整數的對應恆等式。



S04 · implies操作前

a,b\in X

操作後

a\oplus b\in X,\ a\odot b\in X,\ r(a)=a

條件：無

規則：division_algorithm · 依賴：S02, G3

葉節點依據：division_algorithm

餘數滿足 0≤r<4，所以每個運算結果都在 X 中：兩個運算是 X 上的封閉二元運算。另外，a∈X 時 a=4·0+a 且 0≤a<4，依唯一性 r(a)=a；之後用它把 c 換成 r(c)。



S05 · equivalent操作前

(a\oplus b)\oplus c=r(r(a+b)+c)

操作後

r(a+b+c)=a\oplus(b\oplus c),\quad a\oplus b=b\oplus a

條件：a,b,c\in X

規則：L_mod_compat · 依賴：S02, S03, S04

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

因 c=r(c)，r(r(a+b)+c)=r(r(a+b)+r(c))=r((a+b)+c)（引理）。同理 a⊕(b⊕c)=r(a+r(b+c))=r(a+(b+c))。整數加法結合，所以兩者相等：⊕ 結合。又 r(a+b)=r(b+a)，⊕ 交換。a、b、c 是 X 的任意元素，所以涵蓋全部 64 個三元組。



S06 · implies操作前

a\oplus 0,\ a\oplus(\ominus a)

操作後

a\oplus 0=a;\ \ominus0=0,\ \ominus1=3,\ \ominus2=2,\ \ominus3=1

條件：無

規則：group_axioms · 依賴：S02, S04, G1

葉節點依據：group_axioms + finite_forall + numeric_evaluation

a⊕0=r(a)=a，0⊕a=a，所以 0 是加法單位元（加法表第 0 行與第 0 列都是 0,1,2,3）。逆元：1⊕3=r(4)=0，2⊕2=r(4)=0，3⊕1=0，0⊕0=0；加法表每一行都恰含一個 0。所以每個元素都有加法逆元。



S07 · implies操作前

\text{closure, associativity, identity 0, inverses, commutativity}

操作後

(X,\oplus)\ \text{abelian group}

條件：無

規則：group_axioms · 依賴：S04, S05, S06

葉節點依據：group_axioms + and_intro_elim

合併 S04（封閉）、S05（結合、交換）、S06（單位元、逆元），(X,⊕) 是阿貝爾群，0 是加法單位元。



S08 · equivalent操作前

(a\odot b)\odot c=r(r(ab)\,c)

操作後

r(abc)=a\odot(b\odot c)

條件：a,b,c\in X

規則：L_mod_compat · 依賴：S02, S03, S04

葉節點依據：L_mod_compat + mul_assoc + forall_intro

因 c=r(c)，r(r(ab)c)=r(r(ab)r(c))=r((ab)c)（引理）；a⊙(b⊙c)=r(a·r(bc))=r(r(a)r(bc))=r(a(bc))。整數乘法結合，所以 ⊙ 結合，對全部三元組成立。



S09 · equivalent操作前

a\odot(b\oplus c)=r(a\,r(b+c))

操作後

r(ab+ac)=(a\odot b)\oplus(a\odot c)

條件：a,b,c\in X

規則：L_mod_compat · 依賴：S02, S03, S04

葉節點依據：L_mod_compat + distributive + forall_intro

左分配：r(a·r(b+c))=r(r(a)r(b+c))=r(a(b+c))=r(ab+ac)=r(r(ab)+r(ac))=(a⊙b)⊕(a⊙c)。第二個等號與最後一步用引理的乘法與加法部分，中間用整數分配律。



S10 · equivalent操作前

(a\oplus b)\odot c=r(r(a+b)\,c)

操作後

r(ac+bc)=(a\odot c)\oplus(b\odot c)

條件：a,b,c\in X

規則：L_mod_compat · 依賴：S02, S03, S04

葉節點依據：L_mod_compat + distributive + forall_intro

右分配要分開證：r(r(a+b)c)=r(r(a+b)r(c))=r((a+b)c)=r(ac+bc)=r(r(ac)+r(bc))=(a⊙c)⊕(b⊙c)。這裡用的是整數右分配 (a+b)c=ac+bc，沒有借用 ⊙ 的交換性。



S11 · implies操作前

1\odot a,\ a\odot 1

操作後

1\odot a=a=a\odot 1\ \text{for all}\ a\in X

條件：無

規則：mul_one · 依賴：S02, S04, G2

葉節點依據：mul_one + finite_forall

1⊙a=r(a)=a，a⊙1=r(a)=a；乘法表第 1 行與第 1 列都是 0,1,2,3。所以 1 是雙側乘法單位元（MKO 要求雙側作用）。



S12 · theorem_application操作前

e\ \text{a two-sided identity for}\ \odot

操作後

e=1

條件：無

規則：L_unique_identity · 依賴：S11

葉節點依據：L_unique_identity

依引理 L_unique_identity（S12.1 證明），任何雙側單位元 e 都等於 1，所以乘法單位元唯一。也可對照表：只有第 1 行等於 0,1,2,3。



S13 · implies操作前

0\ \text{additive identity},\ 1\ \text{multiplicative identity}

操作後

1\neq 0

條件：無

規則：numeric_evaluation · 依賴：S06, S11

葉節點依據：numeric_evaluation + mul_one

1 與 0 是 X 中不同的元素；而且它們作用不同：1⊙1=1，而 0⊙1=0。MKO 要求 1≠0，排除只有一個元素的零環。



S14 · implies操作前

\text{all obligations of S01}

操作後

(X,\oplus,\odot)\ \text{is a finite unital ring};\ 2\odot2=0

條件：無

規則：mko_ring_def · 依賴：S01, S07, S08, S09, S10, S11, S12, S13

葉節點依據：mko_ring_def + and_intro_elim

S01 的全部責任都已證成：S07（加法阿貝爾群）、S08（乘法結合）、S09 與 S10（左右分配）、S11 到 S13（唯一雙側單位元且 1≠0）。所以它是有限含一環。另外 2⊙2=r(4)=0 而 2≠0，2 是零因子：它不是整環或域，但 MKO 不要求這些（它們另立節點）。







## 局部子步與引理

S03.1 · implies操作前

m-m'=4t,\ m'=4s+r(m')

操作後

r(m)=r(m')

條件：0\le r(m')<4

規則：division_algorithm · 依賴：G3, division_algorithm

葉節點依據：division_algorithm + distributive + add_assoc

先證輔助事實：若 m−m′ 是 4 的倍數，則兩者餘數相同。由 m′=4s+r(m′) 得 m=m′+4t=4(s+t)+r(m′)，且 0≤r(m′)<4。除法演算法的唯一性說明 m 的餘數只能是 r(m′)。



S03.2 · implies操作前

m=4q+r(m),\ k=4p+r(k)

操作後

(m+k)-(r(m)+r(k))=4(q+p)\Rightarrow r(m+k)=r(r(m)+r(k))

條件：無

規則：distributive · 依賴：S03.1, G3

葉節點依據：distributive + add_assoc + add_comm

相加得 m+k=4(q+p)+(r(m)+r(k))，所以 m+k 與 r(m)+r(k) 相差 4 的倍數；依 S03.1 兩者餘數相同。N3 核對所用的代數恆等式。



S03.3 · implies操作前

m=4q+r(m),\ k=4p+r(k)

操作後

mk-r(m)r(k)=4(4qp+q\,r(k)+p\,r(m))\Rightarrow r(mk)=r(r(m)r(k))

條件：無

規則：distributive · 依賴：S03.1, G3

葉節點依據：distributive + mul_comm + mul_assoc + add_assoc

展開 mk=(4q+r(m))(4p+r(k))=16qp+4q·r(k)+4p·r(m)+r(m)r(k)，所以 mk 與 r(m)r(k) 相差 4(4qp+q·r(k)+p·r(m))，是 4 的倍數；依 S03.1 餘數相同。S03.1 到 S03.3 合起來證得引理 L_mod_compat。N2 核對展開式。



S12.1 · implies操作前

e\odot x=x=x\odot e,\ e'\odot x=x=x\odot e'\ \forall x

操作後

e=e\odot e'=e'

條件：無

規則：eq_refl_symm_trans · 依賴：eq_refl_symm_trans

葉節點依據：eq_refl_symm_trans + eq_replace

e′ 是右單位元，所以 e⊙e′=e；e 是左單位元，所以 e⊙e′=e′。依等號的對稱與傳遞得 e=e′。這證得引理 L_unique_identity。







## 逐步反向審查


- S14 · sufficient_goal_reduction · S01, S07, S08, S09, S10, S11, S12, S13 — 目標 G：含一環。足夠條件 H：S01 的全部責任；H⇒G 由定義。H 由 S02 到 S13 正向證成，沒有把 G 當作前提。
- S13 · premise_audit · S06, S11 — 只需比較兩個元素；不涉及其他公理。
- S12.1 · premise_audit · eq_refl_symm_trans — 用到一個是左單位元、另一個是右單位元；此子步不使用 L_unique_identity。
- S12 · premise_audit · S11, L_unique_identity — 需要 1 本身是雙側單位元（S11）；唯一性不依賴表的大小。
- S11 · premise_audit · S04, G2, mul_one — 行與列都核過，所以是雙側；只有一側不夠。
- S10 · inverse_equivalence · L_mod_compat, distributive — 等式鏈可倒推；本稿分別直接證明左右分配，不借用乘法交換性；不由非交換矩陣例子推論兩條公理的獨立性。
- S09 · inverse_equivalence · L_mod_compat, distributive — 等式鏈可倒推；只證左分配，右分配另在 S10 證明。
- S08 · inverse_equivalence · L_mod_compat, S04, mul_assoc — 等式鏈的每一環都是等值改寫，可倒推。
- S07 · sufficient_goal_reduction · S04, S05, S06, group_axioms — 目標：加法是阿貝爾群。足夠條件：群公理加交換律，全部由前面的步驟正向證成。
- S06 · premise_audit · S04, G1, group_axioms — 四個元素的逆元逐一列出；因 ⊕ 交換，單側即雙側。
- S05 · inverse_equivalence · L_mod_compat, S04, add_assoc — 每個等號都是等值改寫（引理是等式），可以倒著讀，雙向成立。
- S04 · premise_audit · S02, division_algorithm — 封閉性只需值域在 X；r(a)=a 只對 X 中的 a 宣稱。
- S03.3 · premise_audit · S03.1, distributive — 只用整數的分配律、交換律與 S03.1；此子步不使用 L_mod_compat。
- S03.2 · premise_audit · S03.1, distributive — 只用整數的分配律與 S03.1；此子步不使用 L_mod_compat。
- S03.1 · premise_audit · division_algorithm — 關鍵是唯一性：找到一個符合 0≤r<4 的表示式就確定了餘數。此子步不使用 L_mod_compat。
- S03 · premise_audit · G3, L_mod_compat — 只依賴除法演算法的存在與唯一性；對所有整數成立，不是有限樣本。
- S02 · premise_audit · G1, G2, G3, finite_forall — 32 格全部比對，所以這是對全部元素對的完整核對，不是抽樣；之後的公理證明都建立在這個識別上。
- S01 · premise_audit · mko_ring_def — 此步只展開定義，不推出新事實。





## 錯誤控制與反例

有乘法單位元不等於是環MKO 指出的誤解之一是把只有乘法單位元的有限表當作含一環。在同一個 ⊕ 上，取 ⊙′ 為依次序 0<2<3<1 的最小值：1 是 ⊙′ 的單位元，⊙′ 結合且交換，但 2⊙′(1⊕1)=2⊙′2=2，而 (2⊙′1)⊕(2⊙′1)=2⊕2=0，分配律失敗。

分配律樣本不夠上面的 ⊙′ 在 a=0 或 a=1 的全部 32 個左分配三元組都通過（a=0 時兩邊都是 0，a=1 時 1 是單位元），卻在 (2,1,1) 失敗。所以必須對全部三元組成立；本稿用引理一次證明全部 64 個三元組，N4 到 N7 再窮舉核對。

左右分配分開核，不要求交換MKO 不要求乘法交換。例如 ℤ/2 上的 2×2 矩陣有 16 個元素，E11·E12=E12 而 E12·E11=0，說明乘法可不交換；這個矩陣環同時滿足左右分配，所以不是「一側成立、另一側失敗」的反例。本稿把左右分配列為分開的證明責任，S09 與 S10 分別直接驗證，S10 沒有借用交換性；此處不宣稱已證明分配公理的邏輯獨立性。


- 單點載體 {0}（0⊕0=0、0⊙0=0）是本 MKO 意義下的含一環 → reject — 唯一可能的乘法單位元是 0，但 MKO 要求 1≠0。
- 模 4 的表不是含一環，因為 2⊙2=0 → reject — 含一環不要求沒有零因子；S14 已證全部責任成立。
- 含一環的乘法必須交換 → reject — ℤ/2 上的 2×2 矩陣構成含一環，但 E11·E12=E12≠0=E12·E11。
- (X,⊕,⊙′)（⊙′ 為次序 0<2<3<1 下的最小值）有單位元 1，且 a=0、1 的分配樣本都通過，所以是含一環 → reject — 2⊙′(1⊕1)=2，而 (2⊙′1)⊕(2⊙′1)=0。





## 結論與限制

X={0,1,2,3} 上的兩個表恰是模 4 的加法與乘法；由模運算相容引理，(X,⊕) 是阿貝爾群，⊙ 結合且左右分配，1 是唯一的雙側乘法單位元且 1≠0。所以它是有限含一環；2⊙2=0 顯示它有零因子，但這不違反含一環的定義。


- N4 到 N7 以模 4 公式在 X 的全部 64 個三元組上求值，是只對這個載體有效的窮舉交叉核對；它們依賴 S02 對表格與公式的逐格識別。
- 錯誤控制中 2×2 矩陣環的環公理未在本稿證明，只用來說明交換性不是定義的一部分。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: a2a8f40dc0dbfde1670bf349418a4632b211fea6b33f6be1d6c49b9287d36163
- original source SHA-256: 30241d9011a9d59085c5ce9d60b57629112800e30ade745754d1fed586529cd4
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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