有限整環：以完整乘法表判定 ℤ/5ℤ 與 ℤ/6ℤ，再由有限性推出可逆

目標與範圍

以完整乘法表判定 ℤ/5ℤ 是有限整環、ℤ/6ℤ 不是；再把「每個非零元可逆」作為定義之後的定理，對任何有限整環用有限性證明，並在 ℤ/5ℤ 中求出全部逆元，同時說明 ℤ/6ℤ 中 2 為何沒有逆元。

只在 MKO 範圍內工作：父結構已是完整有限交換含一環（ℤ/5ℤ 與 ℤ/6ℤ，加法與乘法表取模給出，假設 a1）；無零因子的條件對全部非零元素對量化（假設 a2）。可逆性定理對一般有限整環證明。不證明「ℤ/nℤ 是整環當且僅當 n 為質數」的一般判準，不建立有限域節點；不改動 canonical MKO 或英文 edition。

已知條件與符號

• divides_def
• division_algorithm
• distributive
• finite_counting_basics
• quantifier_negation
• injective_surjective_def
• case_analysis

• G1 — R5=ℤ/5ℤ={0,1,2,3,4}，加法與乘法是整數運算後取除以 5 的餘數；完整的加法表與乘法表由此確定，R5 已是有限交換含一環（MKO 假設 a1）。
• G2 — R6=ℤ/6ℤ={0,1,2,3,4,5}，運算同上但取模 6；R6 也已是有限交換含一環。
• G3 — 定義 D(R)：有限交換含一環 R 是有限整環，若 1≠0，且對所有 a,b∈R，a≠0、b≠0 ⇒ ab≠0（量化全部非零元素對，MKO 假設 a2）。定義中沒有「非零元可逆」。

• \mathbb{Z}/n\mathbb{Z} — 模 n 的剩餘類環，元素記為 0 到 n−1
• D(R) — R 是有限整環
• \lambda_a — 乘以 a 的映射 x↦ax
• a^{-1} — a 的乘法逆元
• R\setminus\{0\} — R 的非零元素

規則與來源

• divides_def · prerequisite — 整除：對整數 a、b，a∣b 表示存在整數 k 使 b=ak。
• division_algorithm · prerequisite — 帶餘除法：對整數 a 與正整數 b，存在唯一的整數 q、r 使 a=bq+r 且 0≤r<b。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• injective_surjective_def · prerequisite — 單射：f(a)=f(a′) ⇒ a=a′。滿射：每個 b∈B 都有 a∈A 使 f(a)=b。雙射：既單又滿，此時有唯一反函數 f⁻¹ 使 f⁻¹∘f=id_A、f∘f⁻¹=id_B。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
• forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• mul_one · prerequisite — 乘法單位元：1·u=u。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
• eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
• add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
• neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
• image_preimage_def · prerequisite — 像與原像：f(S)={f(a) ∣ a∈S}；f⁻¹(T)={a∈A ∣ f(a)∈T}。原像記號不預設 f 有反函數。
• subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
• set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。
• contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
• exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。
• mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
• zero_product · prerequisite — 零乘積性質：在 ℤ、ℚ、ℝ、ℂ（或任何整域）中，uv=0 ⇔ u=0 或 v=0。
• mko_fid_def · cited — 在同一完整有限交換含一環表上，若對所有非零 a,b 皆有 a 乘 b 不等於 0，則為有限整環。完整表可逐對核零因子；每個非零元可逆是利用有限性的後續定理步驟，不偷放入定義。 · mko-finite-integral-domain
• mod_reduce · prerequisite — 在 ℤ/nℤ 中，整數 m 代表它除以 n 的餘數 r（0≤r<n）；兩個整數代表同一元素當且僅當 n 整除兩者之差；兩元素的積是整數積的餘數。
• ring_axioms · prerequisite — 交換含一環：加法成交換群，乘法結合、交換、有單位元 1，且分配律成立；由此 a·0=0 且 a(x−y)=ax−ay。
• L_lambda_injective · lemma — 在整環 R 中，若 a≠0，則 λ_a(x)=ax 是單射：ax=ay ⇒ x=y。
• L_finite_inj_surj · lemma — 有限集 S 上的單射 f:S→S 必為滿射。

逐步主鏈

D(\mathbb{Z}/5\mathbb{Z})

\text{(i) ring (G1)}\ \land\ \text{(ii) }1\neq 0\ \land\ \text{(iii) }\forall a,b\in R_5\setminus\{0\}:\ ab\neq 0

1,0\in\mathbb{Z}/5\mathbb{Z}

1\neq 0

\forall (a,b)\in\{1,2,3,4\}^2:\ ab\neq 0

\forall a\le b\ \text{in}\ \{1,2,3,4\}:\ ab\neq 0

ab\ (1\le a\le b\le 4)\ \text{in}\ \mathbb{Z}/5\mathbb{Z}

1\cdot b=b;\ 2\cdot2=4,\ 2\cdot3=1,\ 2\cdot4=3,\ 3\cdot3=4,\ 3\cdot4=2,\ 4\cdot4=1

\text{the 10 products lie in }\{1,2,3,4\}

\forall a,b\in R_5\setminus\{0\}:\ ab\neq 0

\text{(i)},\ \text{(ii)},\ \text{(iii) for }R_5

D(\mathbb{Z}/5\mathbb{Z})

2,3\in R_6\setminus\{0\}

2\cdot 3=0\ \text{in}\ \mathbb{Z}/6\mathbb{Z},\ \text{hence}\ \neg D(\mathbb{Z}/6\mathbb{Z})

D(R),\ a\in R\setminus\{0\},\ \lambda_a(x)=ax

\lambda_a:R\to R\ \text{injective}

\lambda_a:R\to R\ \text{injective},\ R\ \text{finite}

\lambda_a(R)=R

1\in R=\lambda_a(R)

\exists b\in R:\ ab=ba=1

\lambda_2\ \text{on}\ \mathbb{Z}/5\mathbb{Z}

(0,1,2,3,4)\mapsto(0,2,4,1,3);\ 2^{-1}=3,\ 3^{-1}=2,\ 4^{-1}=4,\ 1^{-1}=1

\lambda_2\ \text{on}\ \mathbb{Z}/6\mathbb{Z}

(0,1,2,3,4,5)\mapsto(0,2,4,0,2,4);\ 1\notin\lambda_2(R_6)

2b=1,\ b\in\mathbb{Z}

\text{no solution: }2\ \text{is not invertible in}\ \mathbb{Z}

D(\mathbb{Z}/5\mathbb{Z}),\ \neg D(\mathbb{Z}/6\mathbb{Z}),\ \text{S08 to S10}

\mathbb{Z}/5\mathbb{Z}\ \text{finite integral domain};\ \mathbb{Z}/6\mathbb{Z}\ \text{not};\ D(R)\Rightarrow\text{every }a\neq0\ \text{invertible}

局部子步與引理

1\cdot b,\ b\in\{1,2,3,4\}

1\cdot b=b\neq 0

2\cdot2,\ 2\cdot3,\ 2\cdot4,\ 3\cdot3,\ 3\cdot4,\ 4\cdot4

4,\ 1,\ 3,\ 4,\ 2,\ 1

ax=ay

a(x-y)=0

a(x-y)=0,\ a\neq 0

x=y

\lambda_a\ \text{injective}

|\lambda_a(R)|=|R|

\lambda_a(R)\subseteq R,\ |\lambda_a(R)|=|R|

\lambda_a(R)=R

逐步反向審查

• S14 · sufficient_goal_reduction · S06, S07, S10, S11 — 目標 G：判定兩個環並證明可逆性定理。足夠條件 H：S06、S07、S10、S11；H⇒G 由合取。H 由 G1 到 G3 正向證成，沒有把 G 當作前提，也沒有把可逆性當作定義的一部分。
• S13 · premise_audit · divides_def, zero_product — ℤ 不屬於 D 的論域（D 只談有限環），這裡只作為對照，說明有限性的作用。
• S12 · premise_audit · S07, mod_reduce — 六個值逐一可重算；1 不在像中這一點對 6 個輸入是完整核對。
• S11 · premise_audit · S06, S10, S04.2, mod_reduce — 每個逆元都可直接乘回核對；這些計算是 S10 在一個例子上的實例，不取代 S10 的一般證明。
• S10 · premise_audit · S09, image_preimage_def, ring_axioms — 需要 S09 的滿射；不宣稱反向，即可逆性不能反過來當作 D(R) 的定義條款。
• S09.2 · premise_audit · S09.1, finite_counting_basics, contradiction — 加法公式 |A∪B|=|A|+|B| 只對有限集給出矛盾；無限集的真子集可以與全集等大。
• S09.1 · premise_audit · S08, finite_counting_basics, image_preimage_def — 需要單射；非單射的映射（如 ℤ/6ℤ 的 λ_2）其像較小。
• S09 · premise_audit · S08, L_finite_inj_surj — 需要單射與有限兩個前提；對無限集不成立：ℤ 中 x↦2x 是單射但不是滿射。
• S08.2 · premise_audit · S08.1, G3, contrapositive — 這裡用的是 (iii) 的逆否形式；沒有 (iii) 時，ℤ/6ℤ 的 2(3−0)=0 而 3−0≠0 正是反例。
• S08.1 · inverse_equivalence · distributive, eq_congruence, add_inverse — 加減 ay 互為反運算，分配律是恆等式，所以雙向成立。
• S08 · premise_audit · G3, L_lambda_injective — 需要 a≠0 與定義的 (iii)；在 ℤ/6ℤ 中 a=2 時結論失敗（S12）。
• S07 · premise_audit · G2, mod_reduce, quantifier_negation — 只需一個零因子對；本步不宣稱找出了全部零因子。
• S06 · premise_audit · S01, S02, S05, G1 — 三項都需要；此步沒有用到可逆性。
• S05 · premise_audit · S03, S04, case_analysis — 需要情況完整（S03 的化約與 S04 的完整列表）；只核其中幾個乘積不能推出全稱命題。
• S04.2 · inverse_equivalence · mod_reduce, division_algorithm — 反向核對：4−4、6−1、8−3、9−4、12−2、16−1 依序為 0、5、5、5、10、15，都是 5 的倍數；餘數由帶餘除法唯一決定。
• S04.1 · inverse_equivalence · mul_one — 1·b=b 是恆等式，兩邊互換即反向。
• S04 · inverse_equivalence · mod_reduce, numeric_evaluation — 每個結果都可反向核對：整數積減去所寫的餘數是 5 的倍數；兩邊表示同一元素。
• S03 · inverse_equivalence · mul_comm, forall_elim — 兩個方向都有理由：特例化給 ⇒，交換律給 ⇐。化約只減少計算量，不減少被覆蓋的情況。
• S02 · premise_audit · mod_reduce, divides_def — 只需要 5∤1。在 ℤ/1ℤ 中 1−0=1 是 1 的倍數，1=0，條件 (ii) 會失敗。
• S01 · premise_audit · G1, G3, mko_fid_def — 此步只展開定義，不推出新事實；三項之一不成立，D(R5) 就不成立。

錯誤控制與反例

抽查乘積不是證書

MKO 指出的誤解：抽查後宣稱無零因子。在 ℤ/6ℤ 中 1·5=5、5·5=25≡1、2·2=4、3·3=9≡3、4·4=16≡4、2·5=10≡4 都非零，但 2·3≡0、3·4≡0。本稿選用對全部非零元素對完整窮舉的證書（ℤ/6ℤ 有 5+C(5,2)=15 個無序對，N9），ℤ/5ℤ 的 S03 到 S05 就採此法；但它不是唯一可能的證法。例如可先直接核出每個非零元的逆元，再把 ab=0 乘以 a 的逆元推出 b=0。這個替代證書的逆元必須獨立核得，不能循環引用本稿稍後先假設整環才證得的可逆性定理。

可逆不放入定義

MKO 的第二個誤解是把「非零元可逆」直接塞進定義。本稿把它放在 S08 到 S10 作為定理，並指出唯一用到有限性的是 S09。ℤ 無零因子但 2 不可逆（S13），所以沒有有限性這個定理就不成立。

在 ℤ/nℤ 中計算，而不是在 ℤ 中

2·3=6 在 ℤ 中非零，但在 ℤ/6ℤ 中 6 的餘數是 0。每個乘積都要取模後再判斷是否為 0（S04.2、S07）。

• 在 ℤ/6ℤ 中抽查 1·5、5·5、2·2、3·3 都非零，所以 ℤ/6ℤ 是整環 → reject — 2·3=6≡0，2、3 都非零；抽樣不能證明全稱命題。
• 依定義，整環的每個非零元都可逆 → reject — 定義只要求無零因子；ℤ 中 2 不可逆。有限整環的可逆性是用有限性證出的定理。
• 乘法表中 0 的那一行全是 0，所以每個環都有零因子 → reject — 零因子要求兩個因子都非零；a·0=0 不算。ℤ/5ℤ 沒有零因子（S05）。
• 零環 {0} 沒有非零元素對，所以是有限整環 → reject — 定義要求 1≠0；零環中 1=0。

結論與限制

ℤ/5ℤ 是有限整環：1≠0，且完整窮舉 16 個非零有序對（化為 10 個乘積）沒有一個積為 0。ℤ/6ℤ 不是：2·3=0。對任何有限整環，乘以非零 a 的映射是單射，有限性使它成為滿射，所以 a 可逆；在 ℤ/5ℤ 中 2^{-1}=3、3^{-1}=2、4^{-1}=4、1^{-1}=1。可逆性是定義之後的定理，ℤ 顯示沒有有限性時它可以失敗。

• 本稿不證明一般判準「ℤ/nℤ 是整環當且僅當 n 為質數」，只對 n=5、6 用完整表判定。有限域節點（MKO 的下一步）另立；本稿只指出 S10 使 ℤ/5ℤ 的非零元可逆。

驗證及來源綁定

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

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

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