模7的Fermat證書與合數邊界

目標與範圍

(−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

逐步主鏈

p=7,\quad a=-2

7\text{ prime},\quad a\equiv5\pmod7,\quad7\nmid a

U_7=\{1,2,3,4,5,6\}

5U_7\pmod7=(5,3,1,6,4,2)

\prod_{u\in U_7}(5u)\equiv\prod_{u\in U_7}u\pmod7

5^6\cdot720\equiv720\pmod7,\quad720\equiv6\pmod7

5^6\cdot6\equiv6\pmod7

5^6\equiv1\pmod7\Rightarrow(-2)^6\equiv1\pmod7

5^2\pmod7

5^2\equiv4,\quad5^4\equiv2,\quad5^6\equiv2\cdot4\equiv1\pmod7

a=7b,\quad b\in\mathbb Z

a^7\equiv0\equiv a\pmod7,\quad a^6\equiv0\not\equiv1\pmod7

n=341=11\cdot31,\quad2^{10}=1024

1024=3\cdot341+1\Rightarrow2^{340}=(2^{10})^{34}\equiv1\pmod{341}

p=7:\quad(-2)^6\equiv1,\quad a=7b:\ a^7\equiv a

\text{coprime and all-integer forms have different domains}

局部子步與引理

本稿無局部子步。

逐步反向審查

• 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。

錯誤控制與反例

消去unit

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