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

目標與範圍

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

逐步主鏈

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}

\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

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}

\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

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

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

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

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

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

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

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}

\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

F_3\text{ ring laws and inverse list}

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

局部子步與引理

本稿無局部子步。

逐步反向審查

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