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

目標與範圍

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

逐步主鏈

(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

\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

m,\ k\in\mathbb{Z}

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

a,b\in X

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

(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\oplus 0,\ a\oplus(\ominus a)

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

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

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

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

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

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

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

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

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

1\odot a,\ a\odot 1

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

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

e=1

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

1\neq 0

\text{all obligations of S01}

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

局部子步與引理

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

r(m)=r(m')

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))

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))

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

e=e\odot e'=e'

逐步反向審查

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