# 完整模7平方表 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-quadratic-residue/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-quadratic-residue-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 模7非零平方剩餘為{1,2,4}；−5≡2有根3、4，3無根。 bounded odd prime7，完整非零平方表；不用Euler或Legendre。 ## 已知條件與符號 - calc - G1 — p=7，候選a=−5與3；非零根代表恰為1、2、3、4、5、6。 - Q_7,N_7 — 非零平方與非平方類 - p — 已核odd prime ## 規則與來源 - calc · prerequisite — 假設精確整數算術、帶餘除法、整除與gcd的定義；同餘等式始終綁定明示模數。假設完整trial division到平方根可判質數。 - mko_definition · cited — 奇質數p下，先正規化a；完整枚舉全部非零平方決定非零平方剩餘，零、p=2與合數模數分開。此處不用Euler判準或Legendre符號。 · mko-quadratic-residue ## 逐步主鏈 S01 · implies操作前 p=7 操作後 7>2,\quad2\nmid7,\quad\sqrt7<3\Rightarrow7\text{ odd prime} 條件：無 規則：calc · 依賴：G1 葉節點依據：calc 平方根以下唯一prime候選2不整除7，認證domain。 S02 · implies操作前 a=-5 操作後 a\equiv2\pmod7,\quad0<2<7 條件：無 規則：calc · 依賴：G1, S01 葉節點依據：calc 先正規化負數，候選是非零類2。 S03 · implies操作前 x=1,2,3 操作後 1^2\equiv1,\quad2^2\equiv4,\quad3^2\equiv2\pmod7 條件：無 規則：calc · 依賴：G1, S01 葉節點依據：calc 平方表前半完整計算為1、4、2。 S04 · implies操作前 x=4,5,6 操作後 \begin{array}{c|rrrrrr}x&1&2&3&4&5&6\\\hline x^2\bmod7&1&4&2&2&4&1\end{array} 條件：無 規則：calc · 依賴：G1, S03 葉節點依據：calc 後半16、25、36餘數為2、4、1，合成完整六項表。 S05 · implies操作前 \begin{array}{c|rrrrrr}x&1&2&3&4&5&6\\\hline x^2\bmod7&1&4&2&2&4&1\end{array} 操作後 Q_7=\{1,2,4\},\quad N_7=\{3,5,6\} 條件：無 規則：calc · 依賴：G1, S04 葉節點依據：calc 去除重複平方值得到全部residues，剩餘非零類便是nonresidues。 S06 · implies操作前 a\equiv2\pmod7 操作後 \operatorname{roots}(2)=\{3,4\},\quad\operatorname{roots}(1)=\{1,6\},\quad\operatorname{roots}(4)=\{2,5\} 條件：無 規則：calc · 依賴：G1, S02, S05 葉節點依據：calc 完整表給每個平方類全部兩根，成x與−x配對。 S07 · implies操作前 a=3,\quad3\notin\{1,2,4\} 操作後 x^2\not\equiv3\pmod7\text{ for every }x\in\mathbb Z 條件：無 規則：mko_definition · 依賴：G1, S04, S05 葉節點依據：mko_definition 全部非零根類已列，零平方亦為0非3，所以全整數均無根。 S08 · implies操作前 p=2\text{ or }m=8 操作後 \operatorname{roots}_{2}(1)=\{1\};\quad\operatorname{roots}_{8}(1)=\{1,3,5,7\} 條件：無 規則：calc · 依賴：G1, S01, S06 葉節點依據：calc 偶prime只有一根；合數8有四根，明示odd-prime兩根責任不能偷換。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S08 · premise_audit · G1, S01, S06 — 模8四奇數的平方均1，無其他類；此表不定義Legendre或Euler。 - S07 · premise_audit · G1, S04, S05 — 無根由完整residue表而非有界整數搜尋推得。 - S06 · premise_audit · G1, S02, S05 — 每對不同，因非零x且奇prime7不允許2x=0。 - S05 · premise_audit · G1, S04 — Q₇不含0，N₇也不含0；兩者只partition非零載體。 - S04 · premise_audit · G1, S03 — 未列x=0是因目前分類非零平方；零另分支。 - S03 · premise_audit · G1, S01 — 3²=9的餘數是2，不是整數9。 - S02 · premise_audit · G1, S01 — −5不是無效輸入；同餘只改代表不改類。 - S01 · premise_audit · G1 — 不得在合數模數沿用後面的兩根結論。 ## 錯誤控制與反例 零類候選先normalize，0獨立於非零residue/nonresidue。 完整根表x=1至6全部列出才可證absence。 - 0是本節非零平方剩餘。 → reject — 0類另列，不在非零集合Q₇。 - 模7的3有根因3²=9。 → reject — 9≡2，不是3；完整表無3。 - 模8的1也恰兩根。 → reject — 1、3、5、7四根皆成立。 ## 結論與限制 模7非零平方剩餘為{1,2,4}；−5≡2有根3、4，3無根。 ## 驗證及來源綁定 2 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 384acd699a63eb402427b8835c9873f84548e160871fa06b63517b0138ea17d3 - original source SHA-256: d000894426cdf201a44c3ff9da8d4a815803ac12c4d484007b9cbefb594772c4 - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-quadratic-residue-01.json)