# 完整逆元配對與Wilson雙向證明 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-wilson-theorem/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-wilson-theorem-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 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 ## 逐步主鏈 S01 · implies操作前 p\text{ prime},\quad1\le a

2時1與−1不同。 S03 · implies操作前 p>2,\quad a\ne a^{-1} 操作後 \{a,a^{-1}\}\text{ disjoint inverse pairs},\quad aa^{-1}\equiv1\pmod p 條件：無 規則：calc · 依賴：G1, S01, S02 葉節點依據：calc 取逆是involution，所以除兩個self-inverse外的全部類正好配成不交雙元素對。 S04 · implies操作前 \prod_{a=1}^{p-1}a\text{ paired as above} 操作後 (p-1)!\equiv1\cdot(-1)\cdot1\equiv-1\pmod p 條件：無 規則：calc · 依賴：G1, S02, S03 葉節點依據：calc 完整所有非零類乘積中，普通逆對給1，自逆的1、−1留下−1。 S05 · implies操作前 p=2 操作後 (2-1)!=1\equiv-1\pmod2 條件：無 規則：calc · 依賴：G1, S01 葉節點依據：calc 偶prime2時1與−1同一類，只出現一次，公式直接成立。 S06 · implies操作前 p=7,\quad a=1,2,3,4,5,6 操作後 a^{-1}=1,4,5,2,3,6\text{ respectively} 條件：無 規則：calc · 依賴：G1, S01, S02 葉節點依據：calc 完整六格逆元表給配對{1}、{6}、{2,4}、{3,5}。 S07 · implies操作前 j=1,2,3,4,5,6 操作後 j!\bmod7=1,2,6,3,1,6\text{ respectively};\quad6!=720\equiv6\pmod7 條件：無 規則：calc · 依賴：G1, S04, S06 葉節點依據：calc 完整逐乘factorial表獨立核prime7方向，6代表−1。 S08 · implies操作前 n>1\text{ composite},\quad11整除1，矛盾，證converse。 S10 · implies操作前 n>1,\quad\text{prime direction and composite contradiction} 操作後 n\text{ prime}\iff(n-1)!\equiv-1\pmod n 條件：無 規則：mko_definition · 依賴：G1, S04, S05, S07, S09 葉節點依據：mko_definition 兩方向連同p=2完成雙向定理，模7表只是實例證書。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - 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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-wilson-theorem-01.json)