自然數模同餘：餘數定義、見證形式、運算保持與取消的限制

目標與範圍

依 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≤r<n；a 為自然數時商 q 也是自然數。
• G3 — 例子：模 7 的 100、23、15、1；模 6 的 2·3 與 2·0；模 7 與模 3 的 100、23、5。

• a\equiv b\pmod n — a 與 b 模 n 同餘
• a\bmod n — a 除以 n 的餘數，0≤a mod n<n
• k,\ l — 見證形式中的自然數
• n — 正模數

規則與來源

• division_algorithm · prerequisite — 帶餘除法：對整數 a 與正整數 b，存在唯一的整數 q、r 使 a=bq+r 且 0≤r<b。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• add_comm · prerequisite — 加法交換律：u+v=v+u。
• add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
• exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
• eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
• mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
• mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
• forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
• mko_cong_def · cited — 對自然數 a、b 與正自然數 n，a≡b (mod n) 當且僅當 a mod n=b mod n；等價地，存在自然數 k、l 使 a+n·k=b+n·l。 · mko-modular-congruence
• L_shift · lemma — 對 n>0 與自然數 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)。

逐步主鏈

a\equiv b\pmod n

a\bmod n=b\bmod n\quad(n>0)

100

100=7\cdot 14+2,\ 0\le 2<7,\ 100\bmod 7=2

23

23=7\cdot 3+2,\ 23\bmod 7=2

100\bmod 7=2=23\bmod 7

100\equiv 23\pmod 7

(x+nm)\bmod n

x\bmod n

a\bmod n=b\bmod n

\exists k,l\in\mathbb{N}:\ a+nk=b+nl

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

\equiv\pmod n\ \text{for one fixed}\ n

\text{reflexive, symmetric, transitive}

15=7\cdot 2+1,\ 1=7\cdot 0+1

15\equiv 1\pmod 7

a\equiv b,\ c\equiv d\pmod n

a+c\equiv b+d,\ ac\equiv bd\pmod n

100\equiv 23,\ 15\equiv 1\pmod 7

115\equiv 24,\quad 1500\equiv 23\pmod 7

2\cdot 3\equiv 2\cdot 0\pmod 6

3\not\equiv 0\pmod 6

100\equiv 23\pmod 7,\ 23\equiv 5\pmod 3

100\not\equiv 5\pmod 7,\ 100\not\equiv 5\pmod 3

局部子步與引理

x=nq+r,\ 0\le r<n

x+nm=n(q+m)+r

x+nm=n(q+m)+r,\ 0\le r<n

(x+nm)\bmod n=r=x\bmod n

a=nq+r,\ b=nq'+r

a+nq'=b+nq

a+nk=b+nl

a\bmod n=(a+nk)\bmod n=(b+nl)\bmod n=b\bmod n

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

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

逐步反向審查

• 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≤r<n；沒有使用引理本身。
• S05.1 · premise_audit · distributive, add_comm, add_assoc — 只用分配律與加法律（N21 為格點恆等式核對）；沒有使用引理本身。
• S05 · inverse_equivalence · L_shift — 兩邊是同一個數，等式雙向成立。
• S04 · inverse_equivalence · mko_cong_def — 定義本身是雙向的：同餘恰好當餘數相等。
• S03 · premise_audit · division_algorithm, numeric_evaluation — 同 S02。
• S02 · premise_audit · division_algorithm, numeric_evaluation — 餘數必須落在 0 到 6；這保證它是唯一的。
• S01 · premise_audit · G1, G2, mko_cong_def — 此步只展開定義；n>0 是餘數有定義所必需。

錯誤控制與反例

不能混用模數

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