# 模7的Fermat證書與合數邊界 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-fermat-little-theorem/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-fermat-little-theorem-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 (−2)^6≡1 mod7；倍數7只可用a^7≡a版本；通過測試不證質數。 明示prime modulus7、完整乘法排列及exact平方乘法，另列合數341。 ## 已知條件與符號 - calc - G1 — p=7，a=−2，先正規化a≡5 mod7；定理形式為同餘而非整數等式。 - p — 已核prime modulus - U_7 — 全部非零mod7代表 ## 規則與來源 - calc · prerequisite — 假設精確整數算術、帶餘除法、整除與gcd的定義；同餘等式始終綁定明示模數。明示假設完整trial division至平方根的prime判準。 - mko_definition · cited — 模數p須明示為prime且p>=2。coprime版本僅在p不整除a時使用；p整除a仍可用all-integer版本但不得消去a。exact modular exponentiation正規化負底數，並以561等合數邊界展示Fermat test converse失敗。 · mko-fermat-little-theorem ## 逐步主鏈 S01 · implies操作前 p=7,\quad a=-2 操作後 7\text{ prime},\quad a\equiv5\pmod7,\quad7\nmid a 條件：無 規則：calc · 依賴：G1 葉節點依據：calc 若7合數有不超√7的質因數，唯一候選2不整除7；故prime，且base是unit。 S02 · implies操作前 U_7=\{1,2,3,4,5,6\} 操作後 5U_7\pmod7=(5,3,1,6,4,2) 條件：無 規則：calc · 依賴：G1, S01 葉節點依據：calc 全部非零代表乘5後各出現一次，所以形成完整排列。 S03 · implies操作前 \prod_{u\in U_7}(5u)\equiv\prod_{u\in U_7}u\pmod7 操作後 5^6\cdot720\equiv720\pmod7,\quad720\equiv6\pmod7 條件：無 規則：calc · 依賴：G1, S02 葉節點依據：calc 排列使乘積不變，抽出六個5後得到可消去的乘積。 S04 · implies操作前 5^6\cdot6\equiv6\pmod7 操作後 5^6\equiv1\pmod7\Rightarrow(-2)^6\equiv1\pmod7 條件：無 規則：calc · 依賴：G1, S01, S03 葉節點依據：calc 兩側乘6消去unit，回到原負base的同餘。 S05 · implies操作前 5^2\pmod7 操作後 5^2\equiv4,\quad5^4\equiv2,\quad5^6\equiv2\cdot4\equiv1\pmod7 條件：無 規則：calc · 依賴：G1, S04 葉節點依據：calc 獨立exact平方乘法再核同一結果，無浮點冪。 S06 · implies操作前 a=7b,\quad b\in\mathbb Z 操作後 a^7\equiv0\equiv a\pmod7,\quad a^6\equiv0\not\equiv1\pmod7 條件：無 規則：calc · 依賴：G1, S01 葉節點依據：calc 若7整除a，全整數形式仍成立；互質形式不適用，不能消去a。 S07 · implies操作前 n=341=11\cdot31,\quad2^{10}=1024 操作後 1024=3\cdot341+1\Rightarrow2^{340}=(2^{10})^{34}\equiv1\pmod{341} 條件：無 規則：calc · 依賴：G1 葉節點依據：calc 合數341也通過base2 Fermat congruence，直接否證測試的prime converse。 S08 · implies操作前 p=7:\quad(-2)^6\equiv1,\quad a=7b:\ a^7\equiv a 操作後 \text{coprime and all-integer forms have different domains} 條件：無 規則：mko_definition · 依賴：G1, S04, S05, S06, S07 葉節點依據：mko_definition 將兩形式與合數反例分層，所有等式均保留模數範圍。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S08 · premise_audit · G1, S04, S05, S06, S07 — 沒有把a^p=a當Z中恆等式；例如2⁷=128不等2。 - S07 · premise_audit · G1 — 11與31都大於1，合數性由因數而非猜測；這不違反prime方向。 - S06 · premise_audit · G1, S01 — 0^6有正指數且等0，不是除零或0^0問題。 - S05 · premise_audit · G1, S04 — 每次積後都取mod7，巨大整數展開並非必要。 - S04 · premise_audit · G1, S01, S03 — 消去依乘積可逆，不允許在0上照做。 - S03 · premise_audit · G1, S02 — 720的餘數6非零，且6·6≡1 mod7，故可逆。 - S02 · premise_audit · G1, S01 — 六個輸入輸出均列，未只核少數pairs。 - S01 · premise_audit · G1 — prime檢查與base非零先完成，不由Fermat通過反證prime。 ## 錯誤控制與反例 消去unita被p整除時不可消去a來取得互質形式。 測試方向先認證prime再套定理；通過同餘不反證prime。 - 7^6≡1 mod7。 → reject — base為0類，正冪仍0。 - 2^340≡1 mod341證341質數。 → reject — 341=11·31合數。 - a^7=a是整數等式。 → reject — a=2時128≠2，僅差126可被7整除。 ## 結論與限制 (−2)^6≡1 mod7；倍數7只可用a^7≡a版本；通過測試不證質數。 ## 驗證及來源綁定 3 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 902aa6dadc0e15cc6307c24fbfeae81e06264151bfb3a4a53cd657582a78760a - original source SHA-256: df79da016f65691101971d594a3f3b8b5f4afcdf8a7607582a5050bee1841e02 - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-fermat-little-theorem-01.json)