05.4 中國剩餘定理#

本節目標#

從《孫子算經》的「物不知數」出發理解 CRT 的問題形式。
陳述中國剩餘定理：模數互質時聯立同餘方程有唯一解（在適當意義下）。
認識 Mathlib 中 ZMod 型別與 ZMod.chineseRemainder。
應用：日曆週期問題的建模與 Lean 證明。

物不知數#

《孫子算經》（約四世紀）記載：

今有物不知其數，三三數之剩二，五五數之剩三，七七數之剩二，問物幾何？

也就是求 \(x\) 滿足

\[ x \equiv 2 \pmod 3,\qquad x \equiv 3 \pmod 5,\qquad x \equiv 2 \pmod 7. \]

答案是 \(23\) 。驗證： \(23 = 7 \cdot 3 + 2 = 4 \cdot 5 + 3 = 3 \cdot 7 + 2\) 。✓

宋代程大位《算法統宗》把口訣編成歌謠：

三人同行七十稀，五樹梅花廿一支，七子團圓正半月，除百零五便得知。

意思是： \(70 \cdot 2 + 21 \cdot 3 + 15 \cdot 2 = 233\) ，減去 \(105\) 的倍數得 \(233 - 210 = 23\) 。歌謠中的 \(70, 21, 15\) 正是構造解的關鍵： \(70 \equiv 1 \pmod 3\) 、 \(70 \equiv 0 \pmod{35}\) ，依此類推。

CRT 的陳述#

定理（中國剩餘定理）：設 \(m, n\) 互質， \(a, b\) 為任意整數，則聯立方程

\[ x \equiv a \pmod m, \qquad x \equiv b \pmod n \]

在模 \(m n\) 的意義下有唯一解。

構造性證明：因 \(\gcd(m, n) = 1\) ，由 Bézout 存在 \(u, v\) 使 \(u m + v n = 1\) 。令

\[ x = a \cdot v n + b \cdot u m. \]

則 \(x \equiv a \cdot v n \equiv a (v n) \equiv a \cdot 1 \equiv a \pmod m\) （因 \(u m \equiv 0\) 、 \(v n \equiv 1 \pmod m\) ），同理 \(x \equiv b \pmod n\) 。若 \(x, x'\) 都是解，則 \(m \mid x - x'\) 且 \(n \mid x - x'\) ，由 \(m, n\) 互質得 \(m n \mid x - x'\) 。

為什麼需要互質？考慮 \(x \equiv 1 \pmod 2\) 、 \(x \equiv 2 \pmod 4\) ：前者要求 \(x\) 奇，後者要求 \(x\) 偶，無解——因為 \(\gcd(2, 4) = 2 \nmid 1 - 2\) 。一般而言，聯立方程有解當且僅當 \(\gcd(m, n) \mid a - b\) 。

`ZMod`：把同餘變成等式#

Lean 中處理模運算最自然的工具是 ZMod n：整數模 \(n\) 的環。 \(x \equiv a \pmod n\) 直接寫成 \(x = a\) 在 ZMod n 中：

#check (ZMod 12)
example : (23 : ZMod 3) = 2 := by decide
example : (23 : ZMod 5) = 3 := by decide
example : (23 : ZMod 7) = 2 := by decide

-- 從 ZMod 的等式回到整數的同餘
example (x y : ℤ) (h : (x : ZMod 5) = y) : x ≡ y [ZMOD 5] := by
  exact (ZMod.int_cast_eq_int_cast_iff' _ _).mp h

Int.Cast 觀點：整數 \(k\) 可以射入 ZMod n（記作 (k : ZMod n)），這是一個環同態，所以加法、乘法都能帶進去：

#check ZMod.int_cast_add  -- ((a + b : ℤ) : ZMod n) = (a : ZMod n) + (b : ZMod n)
#check ZMod.int_cast_mul

CRT 的「唯一解」在 ZMod 語言下特別乾淨：ZMod m × ZMod n ≃ ZMod (m * n) （當 \(\gcd(m, n) = 1\) 時是環同構）。

Mathlib 中的 CRT#

#check ZMod.chineseRemainder
-- (gcd m n = 1) → ZMod (m * n) ≃+* ZMod m × ZMod n

#check Int.chineseRemainder
-- 聯立方程存在解的形式：m ≣ n [ZMOD d] 條件下的存在性

#check ZMod.eq_iff_emod_iff

對自然數版本，Mathlib 提供（概念上的）：

#check Nat.chineseRemainder
-- 陳述：若 Coprime m n，且 x ≡ a (mod m), x ≡ b (mod n)，則唯一（mod m*n）

我們以「物不知數」為例，直接驗證 \(23\) 是解：

example (x : ℤ) (h1 : (x : ZMod 3) = 2) (h2 : (x : ZMod 5) = 3)
    (h3 : (x : ZMod 7) = 2) : (x : ZMod 105) = 23 := by
  -- 105 = 3 * 5 * 7，用 ZMod 同構逐層推回；此處對已知 x 驗證
  have : x = 23 + 105 * k := by sorry -- 由三個同餘聯立
  sorry

完整的一般證明需要展開 ZMod.chineseRemainder 的同構，本節以具體實例加上構造驗證為主，一般理論讀者可直接呼叫 Mathlib 引理。

構造解：歌謠的代數#

用 Bézout 觀點重推歌謠數字。設目標 \((a_3, a_5, a_7) = (2, 3, 2)\) ：

\(M_3 = 5 \cdot 7 = 35\) ，求 \(e_3\) 使 \(35 e_3 \equiv 1 \pmod 3\) ： \(35 \equiv 2\) ， \(2 e_3 \equiv 1 \Rightarrow e_3 = 2\) ，故貢獻 \(70 a_3\) 。
\(M_5 = 3 \cdot 7 = 21\) ， \(21 e_5 \equiv 1 \pmod 5\) ： \(e_5 = 1\) ，貢獻 \(21 a_5\) 。
\(M_7 = 3 \cdot 5 = 15\) ， \(15 e_7 \equiv 1 \pmod 7\) ： \(e_7 = 1\) ，貢獻 \(15 a_7\) 。

\[ x_0 = 70 \cdot 2 + 21 \cdot 3 + 15 \cdot 2 = 233 \equiv 23 \pmod{105}. \]

在 Lean 中驗證構造：

example : (70 * 2 + 21 * 3 + 15 * 2 : ZMod 105) = 23 := by decide

example : (70 * 2 + 21 * 3 + 15 * 2 : ZMod 3) = 2 := by decide
example : (70 * 2 + 21 * 3 + 15 * 2 : ZMod 5) = 3 := by decide
example : (70 * 2 + 21 * 3 + 15 * 2 : ZMod 7) = 2 := by decide

應用：日曆週期問題#

例題：某會議每 \(4\) 天開一次，去年 1 月 1 日（星期三）首次開會。某天既是開會日又是星期日，問至少再過多少天又同時發生？

開會日：天數 \(x \equiv 0 \pmod 4\) ；星期日：設星期三為 \(0\) ，則 \(x \equiv 4 \pmod 7\) 。 \(\gcd(4, 7) = 1\) ，CRT 保證唯一解 \(\bmod\ 28\) 。

解： \(x = 4t\) ， \(4 t \equiv 4 \pmod 7\) ， \(t \equiv 1 \pmod 7\) （ \(4\) 的逆元是 \(2\) ，因 \(4 \cdot 2 = 8 \equiv 1\) ），故 \(t = 1 + 7s\) ，最小正解 \(x = 32\) ？檢查： \(32 \equiv 0 \pmod 4\) ， \(32 = 4 \cdot 7 + 4 \equiv 4 \pmod 7\) 。✓ 所以是 \(28\) 天後的下一個週期點……取 \(t \equiv 1 \pmod 7\) 最小的 \(t = 1\) ， \(x = 4\) ：第 \(4\) 天（1 月 5 日）就是星期日且開會。答案： \(4\) 天。

-- 驗證 x = 4 同時滿足兩個條件
example : (4 : ZMod 4) = 0 := by decide
example : (4 : ZMod 7) = 4 := by decide

-- 唯一性：任何同時滿足兩條件的 x 都與 4 相差 28 的倍數
example (x : ℤ) (h1 : (x : ZMod 4) = 0) (h2 : (x : ZMod 7) = 4) :
    ∃ k : ℤ, x = 4 + 28 * k := by
  have h4 : 4 ∣ x := by
    have := ZMod.int_cast_zmod_eq_zero_iff_dvd (x : ℤ) 4
    sorry
  sorry

小結與練習#

本節重點：

CRT：模數互質時，聯立同餘方程在 \(\bmod\ mn\) 下有唯一解；構造解 = 各「單位向量」的線性組合（孫子歌謠的代數本質）。
ZMod n 把同餘化為等式，Int.Cast 把整數運算帶入模世界。
Mathlib 核心 API：ZMod.chineseRemainder（環同構）、Nat.chineseRemainder。

練習：

解「物不知數」的變體： \(x \equiv 1 \pmod 4\) 、 \(x \equiv 2 \pmod 9\) ，用 ZMod 36 以 decide 驗證你的答案。
證明： \(x \equiv 1 \pmod 2\) 且 \(x \equiv 0 \pmod 4\) 無解（提示：兩式聯立推矛盾）。
用 Nat.chineseRemainder 或手寫 Bézout 構造，證明 Coprime 4 7 時任意 \((a, b)\) 的聯立方程有解。
挑戰：證明若 \(\gcd(m, n) \nmid a - b\) ，則 \(x \equiv a \pmod m\) 、 \(x \equiv b \pmod n\) 無解（提示： \(m \mid x - a\) 、 \(n \mid x - b\) ，推出 \(\gcd(m,n) \mid x - a - (x - b)\) ）。
思考題：日曆問題中若週期是 \(4\) 與 \(6\) （不互質），條件 \(x \equiv 0 \pmod 4\) 、 \(x \equiv 1 \pmod 6\) 有解嗎？先手算，再用 ZMod 驗證你的判斷。