# 自然數模同餘：餘數定義、見證形式、運算保持與取消的限制 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-modular-congruence/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-modular-congruence-01 · production-20261019-adopted-96 ## 目標與範圍 依 MKO 定義（n>0，a≡b (mod n) ⇔ a mod n=b mod n）：(1) 判定 100≡23 (mod 7)；(2) 證明它等價於見證形式「存在自然數 k、l 使 a+nk=b+nl」，並給出 100 與 23 的見證；(3) 說明同餘是等價關係；(4) 證明加法與乘法保持同餘，並由 15≡1 (mod 7) 得 115≡24、1500≡23 (mod 7)；(5) 以 2·3≡2·0 (mod 6) 說明不能無條件取消公因子；(6) 說明不同模數不能串接，並說明模數 0 被排除。 只處理自然數 a、b 與正模數 n（MKO 假設 a1、a2）；餘數由帶餘除法定義。證明兩種定義等價、同餘是等價關係、加法與乘法保持同餘。取消律在 gcd(c,n)=1 時成立這一正面結果不在本稿證明。不處理負整數或模數 0；不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - division_algorithm - distributive - eq_refl_symm_trans - numeric_evaluation - G1 — a、b 是自然數，模數 n 是正自然數（MKO 假設 a1）；本條目排除 n=0（MKO 假設 a2）。 - G2 — a mod n 是帶餘除法的餘數：唯一的 r 使 a=nq+r 且 0≤r0 與自然數 x、m：(x+n·m) mod n=x mod n。 - L_witness · lemma — 對 n>0 與自然數 a、b：a mod n=b mod n ⇔ 存在自然數 k、l 使 a+nk=b+nl。 - L_add_mul · lemma — 若 a≡b (mod n) 且 c≡d (mod n)，則 a+c≡b+d (mod n) 且 ac≡bd (mod n)。 ## 逐步主鏈 S01 · definition操作前 a\equiv b\pmod n 操作後 a\bmod n=b\bmod n\quad(n>0) 條件：n>0 規則：mko_cong_def · 依賴：G1, G2, mko_cong_def 葉節點依據：mko_cong_def + def_unfold 依 MKO 的定義，同餘是在固定的同一個正模數下比較兩個餘數。它不是數值相等：兩數可以不同而同餘。 S02 · implies操作前 100 操作後 100=7\cdot 14+2,\ 0\le 2<7,\ 100\bmod 7=2 條件：7>0 規則：division_algorithm · 依賴：G2, G3, division_algorithm 葉節點依據：division_algorithm + numeric_evaluation 7·14=98，100−98=2，且 0≤2<7（N1、N2）。依帶餘除法的唯一性，100 mod 7=2。 S03 · implies操作前 23 操作後 23=7\cdot 3+2,\ 23\bmod 7=2 條件：7>0 規則：division_algorithm · 依賴：G2, G3, division_algorithm 葉節點依據：division_algorithm + numeric_evaluation 7·3=21，23−21=2，0≤2<7（N3、N4），所以 23 mod 7=2。 S04 · equivalent操作前 100\bmod 7=2=23\bmod 7 操作後 100\equiv 23\pmod 7 條件：無 規則：mko_cong_def · 依賴：S01, S02, S03 葉節點依據：mko_cong_def + eq_refl_symm_trans 兩個餘數都是 2，依定義 100≡23 (mod 7)，雖然 100≠23。 S05 · equivalent操作前 (x+nm)\bmod n 操作後 x\bmod n 條件：n>0 規則：L_shift · 依賴：G2, L_shift 葉節點依據：division_algorithm + distributive 加上 n 的自然數倍不改變餘數：依引理 L_shift（S05.1、S05.2 證明）。後面的等價與運算保持都靠它。 S06 · equivalent操作前 a\bmod n=b\bmod n 操作後 \exists k,l\in\mathbb{N}:\ a+nk=b+nl 條件：n>0 規則：L_witness · 依賴：S01, L_witness 葉節點依據：division_algorithm + distributive + eq_refl_symm_trans 依引理 L_witness（S06.1、S06.2 證明），餘數定義與 MKO 的見證形式等價。見證形式的好處是全在自然數中，不必做減法。 S07 · implies操作前 100=7\cdot 14+2,\ 23=7\cdot 3+2 操作後 100+7\cdot 3=23+7\cdot 14=121;\quad 100+7\cdot 0=23+7\cdot 11 條件：無 規則：exists_intro · 依賴：S02, S03, S06 葉節點依據：exists_intro + numeric_evaluation 依 S06.1 的構造，k=3、l=14：100+21=121=23+98（N5）。另一組見證 k=0、l=11：100=23+77（N6）。見證不唯一。 S08 · implies操作前 \equiv\pmod n\ \text{for one fixed}\ n 操作後 \text{reflexive, symmetric, transitive} 條件：n\ \text{fixed} 規則：eq_refl_symm_trans · 依賴：S01, eq_refl_symm_trans 葉節點依據：eq_refl_symm_trans + def_unfold 在固定的 n 下，a≡b 就是 a mod n=b mod n，是餘數之間的等式。等號的自反、對稱、遞移直接給出 a≡a；a≡b ⇒ b≡a；a≡b 且 b≡c ⇒ a≡c。所以同餘在 ℕ 上是等價關係（MKO 段落 0）。 S09 · implies操作前 15=7\cdot 2+1,\ 1=7\cdot 0+1 操作後 15\equiv 1\pmod 7 條件：無 規則：mko_cong_def · 依賴：G3, division_algorithm 葉節點依據：division_algorithm + numeric_evaluation 15 mod 7=1（N7），1 mod 7=1，所以 15≡1 (mod 7)。 S10 · implies操作前 a\equiv b,\ c\equiv d\pmod n 操作後 a+c\equiv b+d,\ ac\equiv bd\pmod n 條件：n>0 規則：L_add_mul · 依賴：S05, L_add_mul 葉節點依據：distributive + division_algorithm + eq_refl_symm_trans 依引理 L_add_mul（S10.1、S10.2 證明），加法與乘法保持同一模數下的同餘。 S11 · implies操作前 100\equiv 23,\ 15\equiv 1\pmod 7 操作後 115\equiv 24,\quad 1500\equiv 23\pmod 7 條件：無 規則：forall_elim · 依賴：S04, S09, S10 葉節點依據：forall_elim + numeric_evaluation 套用 S10：100+15=115≡23+1=24，100·15=1500≡23·1=23 (mod 7)。逐項重算核對（MKO 段落 1）：115=7·16+3、24=7·3+3，餘數都是 3；1500=7·214+2、23 mod 7=2，餘數都是 2（N8 到 N11）。 S12 · implies操作前 2\cdot 3\equiv 2\cdot 0\pmod 6 操作後 3\not\equiv 0\pmod 6 條件：無 規則：numeric_evaluation · 依賴：S01, G3 葉節點依據：numeric_evaluation + mko_cong_def 2·3=6，6 mod 6=0；2·0=0，0 mod 6=0，所以 2·3≡2·0 (mod 6)。但 3 mod 6=3≠0=0 mod 6，所以 3≢0 (mod 6)（N12、N13）。因此從 c·a≡c·b 直接取消 c 不合法；這裡 gcd(2,6)=2≠1（N14），正是 MKO 段落 2 所說要考慮 c 與 n 的最大公因數。 S13 · implies操作前 100\equiv 23\pmod 7,\ 23\equiv 5\pmod 3 操作後 100\not\equiv 5\pmod 7,\ 100\not\equiv 5\pmod 3 條件：無 規則：numeric_evaluation · 依賴：S04, S08, G3 葉節點依據：numeric_evaluation + mko_cong_def 23=3·7+2、5=3·1+2，所以 23≡5 (mod 3)（N15）。若誤把兩個不同模數的同餘串接，會得到 100≡5。但 100 mod 7=2≠5=5 mod 7（N17），100 mod 3=1≠2=5 mod 3（N16），兩個模數下都不成立。S08 的遞移性只對同一個 n 成立。 ## 局部子步與引理 S05.1 · implies操作前 x=nq+r,\ 0\le r0 規則：division_algorithm · 依賴：S05.1, division_algorithm 葉節點依據：division_algorithm x+nm 已寫成 n·(自然數)+r 且 0≤r0 規則：L_shift · 依賴：S05 葉節點依據：eq_congruence + eq_refl_symm_trans + division_algorithm （⇐ 方向）依 L_shift，a mod n=(a+nk) mod n；兩個相等的數有相同餘數；再依 L_shift，(b+nl) mod n=b mod n。S06.1 與 S06.2 合起來證得引理 L_witness。 S10.1 · implies操作前 a=nq_1+r,\ b=nq_2+r,\ c=nq_3+s,\ d=nq_4+s 操作後 (a+c)\bmod n=(r+s)\bmod n=(b+d)\bmod n 條件：無 規則：L_shift · 依賴：S05, G2, distributive 葉節點依據：distributive + add_comm + add_assoc + division_algorithm 設 a、b 的共同餘數為 r，c、d 的共同餘數為 s。則 a+c=n(q₁+q₃)+(r+s)、b+d=n(q₂+q₄)+(r+s)（N19）。依 L_shift，兩者的餘數都等於 (r+s) mod n，所以 a+c≡b+d。注意 r+s 可能 ≥n，所以要再取一次餘數，而不是直接說餘數是 r+s。 S10.2 · implies操作前 ac=(nq_1+r)(nq_3+s) 操作後 ac=n(nq_1q_3+q_1s+rq_3)+rs,\ (ac)\bmod n=(rs)\bmod n=(bd)\bmod n 條件：無 規則：L_shift · 依賴：S05, G2, distributive 葉節點依據：distributive + mul_assoc + mul_comm + division_algorithm 展開：(nq₁+r)(nq₃+s)=n(nq₁q₃+q₁s+rq₃)+rs（N18）。同理 bd=n(nq₂q₄+q₂s+rq₄)+rs。依 L_shift，兩者的餘數都等於 (rs) mod n，所以 ac≡bd。S10.1 與 S10.2 合起來證得引理 L_add_mul。 ## 逐步反向審查 - S13 · premise_audit · S08, numeric_evaluation — 具體反例；說明遞移性的前提「同一模數」不能省。 - S12 · premise_audit · S01, numeric_evaluation — 一個反例足以否定「無條件取消」；本稿不證明 gcd(c,n)=1 時取消合法。 - S11 · premise_audit · S10, forall_elim, numeric_evaluation — 這是一般結果的實例；直接重算只是核對，不取代 S10 的證明。 - S10.2 · premise_audit · S05, distributive — 只用分配律與 L_shift；沒有使用 L_add_mul 本身。 - S10.1 · premise_audit · S05, distributive — 只用 L_shift 與分配律；沒有使用 L_add_mul 本身。 - S10 · premise_audit · L_add_mul — 不宣稱反向：由 ac≡bd 不能推出 a≡b 或 c≡d（S12）。 - S09 · premise_audit · division_algorithm, mko_cong_def — 兩個餘數直接計算。 - S08 · premise_audit · S01, eq_refl_symm_trans — 遞移性要求兩個同餘式用同一個 n；不同模數的餘數不是同一種量（S13）。 - S07 · premise_audit · S06, exists_intro, numeric_evaluation — 存在性只需一組見證；這裡給兩組以示不唯一。 - S06.2 · premise_audit · S05, eq_congruence — 用到的是已證的 L_shift，不是 L_witness 本身。 - S06.1 · premise_audit · distributive, add_comm, exists_intro — 只用加法交換、結合與見證引入；沒有使用引理本身。 - S06 · inverse_equivalence · L_witness — 兩個方向分別在 S06.1、S06.2 證明。 - S05.2 · premise_audit · division_algorithm — 關鍵是唯一性與 0≤r0 是餘數有定義所必需。 ## 錯誤控制與反例 不能混用模數MKO 指出的誤解之一：混用不同模數。100≡23 (mod 7) 與 23≡5 (mod 3) 不能串成 100≡5；事實上在兩個模數下都不成立（S13）。 不得無條件取消公因子MKO 指出的另一個誤解：在同餘式兩側無條件取消共同因子。2·3≡2·0 (mod 6) 但 3≢0 (mod 6)（S12）。取消需要考慮 c 與 n 的最大公因數；本稿不證明正面的條件。 模數 0 被排除MKO 指出的第三個誤解：允許零模數。帶餘除法需要正除數，a mod 0 在本條目中沒有定義；各程式語言對 x mod 0 的處理不一（有的報錯），本條目刻意不採用這些慣例（MKO 假設 a2）。 同餘不是數值相等100≡23 (mod 7) 而 100≠23。同餘比較的是固定模數下的餘數（MKO 段落 0）。 - 由 2·3≡2·0 (mod 6) 兩邊消去 2，得 3≡0 (mod 6) → reject — 3 mod 6=3≠0；gcd(2,6)=2≠1。 - 100≡23 (mod 7) 且 23≡5 (mod 3)，所以 100≡5 (mod 7) → reject — 100 mod 7=2，5 mod 7=5；遞移性只對同一模數成立。 - 依某些程式語言的慣例 7 mod 0=7，所以可在本條目中判定 7≡7 (mod 0) → reject — 本條目要求 n 為正自然數，n=0 被刻意排除。 - 100≡23 (mod 7)，所以 100=23 → reject — 同餘只表示餘數相等；100≠23。 - 100≡23 (mod 7) 的見證 (k,l) 唯一 → reject — (3,14) 與 (0,11) 都可以。 ## 結論與限制 100≡23 (mod 7)，因為兩者除以 7 都餘 2；餘數定義與見證形式等價，100 與 23 的見證可取 (k,l)=(3,14) 或 (0,11)。同餘在固定模數下是等價關係，並被加法與乘法保持：115≡24、1500≡23 (mod 7)。2·3≡2·0 (mod 6) 但 3≢0 (mod 6)，所以不能無條件取消公因子；不同模數的同餘不能串接；模數 0 被排除。 - 取消律的正面結果（gcd(c,n)=1 時 ca≡cb ⇒ a≡b）不在本稿證明。 - 帶餘除法（含唯一性）作為前置規則引用；自然數 a 的商為自然數，其理由見自然數整除的教學稿。 ## 驗證及來源綁定 21 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 2e962d623d84262cb743a552037824dee16a1980f16f38b26d7bf9aeaa025587 - original source SHA-256: 2e962d623d84262cb743a552037824dee16a1980f16f38b26d7bf9aeaa025587 - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-modular-congruence-01.json)