完整逆元配對與Wilson雙向證明

目標與範圍

n>1時(n−1)!≡−1 modn恰當n prime；模7完整逆元表核6!≡6。

一般雙向教學論證加上模7全表與p=2分支；有限測試不替代證明。

已知條件與符號

• calc

• G1 — n為整數且n>1；prime方向另記p；實例p=7。

• d — proper正因數
• p — prime modulus

規則與來源

本稿部分規則文字經本輪讀者釐清，屬於改述而非逐字引文；被引用的原始來源內容及雜湊沒有改動。

• calc · prerequisite — 假設精確整數算術、帶餘除法、整除與gcd的定義；同餘等式始終綁定明示模數。明示假設互質Bezout定理及prime的Euclid引理p|ab⇒p|a或p|b。
• mko_definition · cited — 先核n>1。prime direction完整枚舉nonzero residues的modular inverses；除self-inverse residues外成對相消，p>2時self-inverse恰1與p-1，p=2時兩者是同一residue。exact factorial table核(n-1)! mod n。Composite examples只證指定n，不取代converse proof；不得混同Fermat little theorem，有限testing不證所有n。 · mko-wilson-theorem

逐步主鏈

p\text{ prime},\quad1\le a<p

\gcd(a,p)=1\Rightarrow\exists a^{-1}\pmod p

a=a^{-1}\pmod p

a^2\equiv1\Rightarrow p\mid(a-1)(a+1)\Rightarrow a\equiv1\text{ or }-1\pmod p

p>2,\quad a\ne a^{-1}

\{a,a^{-1}\}\text{ disjoint inverse pairs},\quad aa^{-1}\equiv1\pmod p

\prod_{a=1}^{p-1}a\text{ paired as above}

(p-1)!\equiv1\cdot(-1)\cdot1\equiv-1\pmod p

p=2

(2-1)!=1\equiv-1\pmod2

p=7,\quad a=1,2,3,4,5,6

a^{-1}=1,4,5,2,3,6\text{ respectively}

j=1,2,3,4,5,6

j!\bmod7=1,2,6,3,1,6\text{ respectively};\quad6!=720\equiv6\pmod7

n>1\text{ composite},\quad1<d<n,\quad d\mid n

d\mid(n-1)!

(n-1)!\equiv-1\pmod n,\quad d\mid n,\quad d\mid(n-1)!

d\mid((n-1)!+1)\text{ and }d\mid(n-1)!\Rightarrow d\mid1\text{ impossible}

n>1,\quad\text{prime direction and composite contradiction}

n\text{ prime}\iff(n-1)!\equiv-1\pmod n

局部子步與引理

本稿無局部子步。

逐步反向審查

• S10 · premise_audit · G1, S04, S05, S07, S09 — n=1不在domain，不能以0!=1的偶然餘數擴張。
• S09 · premise_audit · G1, S08 — 這是一般反證，不是以幾個composite測試取代。
• S08 · premise_audit · G1 — 不需聲稱所有合數factorial都0 modn；n=4也由此證法涵蓋。
• S07 · premise_audit · G1, S04, S06 — Wilson使用factorial不是Fermat的base power。
• S06 · premise_audit · G1, S01, S02 — 2·4=8≡1、3·5=15≡1、6²=36≡1，全部覆核。
• S05 · premise_audit · G1, S01 — 不能把兩個相同self-inverse代表重複計入乘積。
• S04 · premise_audit · G1, S02, S03 — 這是對任意odd prime的論證，不是只用p=7表外推。
• S03 · premise_audit · G1, S01, S02 — a^{-1}的逆是a，因此不會漏類或把一類配兩次。
• S02 · premise_audit · G1, S01 — prime前提是零乘積推因子的關鍵，合數不保證。
• S01 · premise_audit · G1 — 逆元唯一到類，因若ab=ac=1則b=b(ac)=(ba)c=c。

錯誤控制與反例

全部配對

全部非零類都需配對或列為self-inverse。

雙向證明

prime配對與composite proper-divisor矛盾分開，不由finite test推全稱。

• 合數4也通過Wilson。 → reject — 3!=6≡2 mod4而−1≡3。
• p=2必有兩個不同self-inverse類。 → reject — 1≡−1 mod2，只有一類。
• Wilson就是a^{p−1}≡1。 → reject — Wilson是(p−1)!，Fermat才是固定base的power。

結論與限制

n>1時(n−1)!≡−1 modn恰當n prime；模7完整逆元表核6!≡6。

驗證及來源綁定

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

• source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
• adopted source SHA-256: 21bca817d48683970a4a4d8b31d62b9415855aa678ab3aa40682b18bfd6d1cdb
• original source SHA-256: a2d4d999d4312d01eaa71a10b634018e935b72665829e46b09f492efd7ebc702
• Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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