# 完整表認證 F₃ 與有限整環引理

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

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

derivation-mko-finite-field-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

F₃ 是域，2/2=1；有限整環的非零乘法映射給逆元。

完整 F₃ 雙表及有限整環引理；F₄ 僅作非質數階的明示邊界。





## 已知條件與符號


- calc


- G1 — F₃={0,1,2}，運算為整數加乘後模3。另令 D 為有限交換含一整環且1≠0。


- F_3 — 模3域
- D — 任意有限整環
- m_a — 乘a自映射





## 規則與來源


- calc · prerequisite — 假設整數與 F₂ 多項式的環運算法則、同餘運算及有限集合單射必滿射；整環指無零因子。
- mko_definition · cited — 以完整有限環雙表核1不等於0、乘法交換及每個非零元素的雙側逆元。除法只對非零除數定義。有限整環成域是利用有限乘法映射單射推出滿射的定理步驟；域階為質數冪，不必是質數。 · mko-finite-field





## 逐步主鏈

S01 · implies操作前

F_3=\{0,1,2\}

操作後

\begin{array}{c|ccc}+&0&1&2\\\hline 0&0&1&2\\1&1&2&0\\2&2&0&1\\\end{array}

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

九個和全部列出，結果均在載體。加法零是0，每列給唯一和。



S02 · implies操作前

\begin{array}{c|ccc}+&0&1&2\\\hline 0&0&1&2\\1&1&2&0\\2&2&0&1\\\end{array}

操作後

-0=0,\quad -1=2,\quad -2=1

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

由表讀得每個加法逆元；結合律與交換律由整數加法取餘保留。



S03 · implies操作前

a,b\in F_3

操作後

\begin{array}{c|ccc}*&0&1&2\\\hline 0&0&0&0\\1&0&1&2\\2&0&2&1\\\end{array}

條件：無

規則：calc · 依賴：G1, S02

葉節點依據：calc

九個積全部列出。整數乘法的結合律、分配律在取餘後仍成立，表沿對角對稱。



S04 · implies操作前

\begin{array}{c|ccc}*&0&1&2\\\hline 0&0&0&0\\1&0&1&2\\2&0&2&1\\\end{array}

操作後

1\ne0,\quad 1^{-1}=1,\quad2^{-1}=2

條件：無

規則：calc · 依賴：G1, S03

葉節點依據：calc

1列保持元素；全部非零元素1與2均有表中雙側逆元。



S05 · implies操作前

2/2:=2\cdot2^{-1}

操作後

2/2=2\cdot2=1\quad(\bmod 3)

條件：denominator 2 is nonzero in F3

規則：calc · 依賴：G1, S04

葉節點依據：calc

除數2非零，因此除法以乘逆元定義，結果為1。



S06 · implies操作前

a\in D\setminus\{0\},\quad m_a(x)=ax

操作後

m_a(x)=m_a(y)\Rightarrow a(x-y)=0\Rightarrow x=y

條件：a is nonzero; D has no zero divisors

規則：calc · 依賴：G1

葉節點依據：calc

在任意上述有限整環，無零因子與a非零證乘法自映射單射。



S07 · implies操作前

m_a:D\to D\text{ injective},\quad |D|<\infty

操作後

m_a\text{ surjective}\Rightarrow\exists b\in D:\ ab=1

條件：無

規則：calc · 依賴：G1, S06

葉節點依據：calc

有限自映射的單射即滿射，所以1有前像b。交換性再給ba=1。



S08 · implies操作前

t^2=t+1\text{ over }F_2

操作後

\begin{array}{c|cccc}+&0&1&t&t+1\\\hline 0&0&1&t&t+1\\1&1&0&t+1&t\\t&t&t+1&0&1\\t+1&t+1&t&1&0\\\end{array}\qquad\begin{array}{c|cccc}*&0&1&t&t+1\\\hline 0&0&0&0&0\\1&0&1&t&t+1\\t&0&t&t+1&1\\t+1&0&t+1&1&t\\\end{array}

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

四個餘式0、1、t、t+1以t²=t+1約化，列出完整雙表。若改代表差為t²+t+1的倍數，加乘仍保持這個性質。



S09 · implies操作前

\begin{array}{c|cccc}*&0&1&t&t+1\\\hline 0&0&0&0&0\\1&0&1&t&t+1\\t&0&t&t+1&1\\t+1&0&t+1&1&t\\\end{array}

操作後

1^{-1}=1,\quad t^{-1}=t+1,\quad(t+1)^{-1}=t,\quad |F_4|=4

條件：無

規則：calc · 依賴：G1, S08

葉節點依據：calc

F₄ 全部三個非零元素有雙側逆元，因此4這個非質數也可以是域階。



S10 · implies操作前

F_3\text{ ring laws and inverse list}

操作後

F_3\text{ is a field};\quad D\text{ finite domain}\Rightarrow D\text{ field}

條件：無

規則：mko_definition · 依賴：G1, S02, S04, S07

葉節點依據：mko_definition

完整F₃證書滿足域定義；有限整環引理由單射到滿射補足所有非零逆元。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S10 · premise_audit · G1, S02, S04, S07 — 域結論依全部非零元素，不是僅算2/2；未分類任意有限交換環。
- S09 · premise_audit · G1, S08 — t(t+1)=t²+t=1；4=2²是質數冪，並未否證質數冪限制。
- S08 · premise_audit · G1 — 因此多項式環法則下降至這四個餘式；表不是任意未認證的運算。
- S07 · premise_audit · G1, S06 — 滿射必對同一有限集合D使用；無限整環的單射未必滿射。
- S06 · premise_audit · G1 — 最後消去不是預設逆元，而是從無零因子推出x-y=0，避免循環。
- S05 · premise_audit · G1, S04 — 反乘2得到2；此反查只因2可逆，並不允許0/0。
- S04 · premise_audit · G1, S03 — 需核2·2=1及交換方向；不能把0加進逆元清單。
- S03 · premise_audit · G1, S02 — 若換整數代表相差3的倍數，加乘結果仍相差3的倍數，故法則能下降。
- S02 · premise_audit · G1, S01 — 加法逆元必使和為0；1+2=0是模3結論。
- S01 · premise_audit · G1 — 反查各列有三格，0列保持全部元素，不是抽樣表。





## 錯誤控制與反例

非零門檻每次寫a/b前先核b≠0；F₃中的2是合法除數。

有限性責任Z中的乘2映射單射但1無前像，故不可略去有限性。


- Z/4Z 也是域。 → reject — 2≠0但2·2=0，且2乘任何元素皆非1。
- 0/0 在 F₃ 定義為1。 → reject — 0乘任意元素均為0，沒有乘法逆元。
- 每個有限域的階都是質數。 → reject — 已列出的 F₄ 雙表與逆元給出階4反例；4是質數冪而非質數。





## 結論與限制

F₃ 是域，2/2=1；有限整環的非零乘法映射給逆元。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 9909c1c936322edb23fc5590d4a6015e7d0dd8e45001936c925a7207563a9e1b
- original source SHA-256: 9722a064eed5b1edabc2c54029af29ccbda3ac540e9a81c9fae3a4286df475eb
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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