自然數整除：以乘數見證判定、處理 0 的情形並證明遞移性

目標與範圍

依 MKO 定義（a∣b ⇔ 存在自然數 k 使 b=a·k）：(1) 證明 6∣84；(2) 證明 6∤87；(3) 證明 4∤10，雖然 10/4=5/2 是一個數；(4) 證明每個 a 都整除 0；(5) 證明 0∣b ⇔ b=0，並說明 0∣0 的見證不唯一、0∤5；(6) 證明 a>0 時見證至多一個（若 a∣b，則既有見證唯一）；(7) 證明整除的自反性與遞移性，並由 3∣6、6∣84 求出 3∣84 的見證。

只在包含 0 的自然數中工作（MKO 假設 a1），見證必須是自然數（a2）。為判定 a>0 的情形，本稿由帶餘除法（引用的前置規則）證明「a∣b ⇔ 餘數為 0」。不處理負整數的整除、最大公因數或質數；不改動 canonical MKO 或英文 edition。

已知條件與符號

• division_algorithm
• order_basics
• mul_zero
• mul_assoc
• numeric_evaluation

• G1 — ℕ 包含 0；乘法是自然數乘法，自然數的和與積仍是自然數（MKO 假設 a1）。
• G2 — 整除的見證 k 必須是自然數；非整數的商不是見證（MKO 假設 a2）。
• G3 — 要判定的數對：(6,84)、(6,87)、(4,10)、(3,6)、(0,0)、(0,5)。

• a\mid b — a 整除 b
• a\nmid b — a 不整除 b
• k — 乘數見證，必須是自然數
• b\bmod a — b 除以 a（a>0）的餘數
• \mathbb{N} — 自然數，包含 0

規則與來源

• division_algorithm · prerequisite — 帶餘除法：對整數 a 與正整數 b，存在唯一的整數 q、r 使 a=bq+r 且 0≤r<b。
• order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
• mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
• mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
• contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
• add_zero · prerequisite — 加法單位元：u+0=u。
• mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
• frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• mul_one · prerequisite — 乘法單位元：1·u=u。
• exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
• mko_dvd_def · cited — 對自然數 a、b，a∣b 當且僅當存在自然數 k 使 b=a·k。 · mko-natural-divisibility
• nat_discrete · prerequisite — 自然數沒有中間值：對自然數 k 與 n，必有 k≤n 或 k≥n+1。
• L_rem_test · lemma — 對自然數 b 與正自然數 a：a∣b ⇔ b 除以 a 的餘數 r 為 0。

逐步主鏈

a\mid b

\exists k\in\mathbb{N}:\ b=a\cdot k

84=6\cdot 14,\ 14\in\mathbb{N}

6\mid 84

a\mid b\quad(a>0)

b\bmod a=0

87=6\cdot 14+3,\ 0\le 3<6

6\nmid 87

10=4k,\ k\in\mathbb{N}\ ?

4\nmid 10

a\in\mathbb{N}

0=a\cdot 0,\ \text{so}\ a\mid 0

0\mid b

b=0

0=0\cdot 0=0\cdot 5,\quad 5\neq 0

0\mid 0\ \text{with non-unique witness};\ 0\nmid 5

b=a k=a k',\ a>0,\ k,k'\in\mathbb{N}

k=k'

a\in\mathbb{N}

a=a\cdot 1,\ \text{so}\ a\mid a

a\mid b,\ b\mid c

a\mid c

6=3\cdot 2,\ 84=6\cdot 14

84=3\cdot 28,\ 3\mid 84

(a,b)\in\mathbb{N}^2

a=0:\ a\mid b\iff b=0;\quad a>0:\ a\mid b\iff b\bmod a=0

局部子步與引理

b=aq+r,\ 0\le r<a,\ q\in\mathbb{Z},\ b\ge 0

q\ge 0,\ \text{so}\ q\in\mathbb{N}

b=aq+0,\ q\in\mathbb{N}

a\mid b

b=a\cdot k,\ k\in\mathbb{N}

b\bmod a=0

b=ak,\ c=bl

c=(ak)l

c=(ak)l

c=a(kl),\ kl\in\mathbb{N}

逐步反向審查

• S13 · sufficient_goal_reduction · S03, S07, case_analysis — 目標 G：對每個數對正確判定。足夠條件 H：a=0 與 a>0 兩種情況各有已證的判準；H⇒G 由分情況論證。H 由 S03、S07 正向證成。
• S12 · premise_audit · S11, forall_elim, numeric_evaluation — 這是 S11 的一個實例並附數值核對；它不能取代一般證明。
• S11.2 · premise_audit · mul_assoc, G1 — 需要 ℕ 對乘法封閉；在有理數中這一步會允許非自然數見證。
• S11.1 · premise_audit · eq_replace — 等值代換。
• S11 · premise_audit · S01, exists_elim, mul_assoc — 結論不含暫取的名字 k、l，所以 ∃消去合法。不宣稱反向：a∣c 不推出 a∣b。
• S10 · premise_audit · mul_one, exists_intro — 只用乘法單位元。
• S09 · premise_audit · order_basics, case_analysis — 需要 a>0 才能保持嚴格不等；a=0 時結論不成立（S08）。
• S08 · premise_audit · S07, mul_zero — 只是 S07 的兩個實例與一個見證不唯一的例子。
• S07 · inverse_equivalence · mul_zero, exists_intro — 反向：若 b=0，取 k=0 得 b=0·0，所以 0∣b。兩向都成立。
• S06 · premise_audit · S01, mul_zero, exists_intro, forall_intro — 只用乘以零的性質；對每個 a 都成立，所以可全稱推廣。
• S05 · premise_audit · S01, S03, G2, mul_inverse_nonzero — 論證依賴「有理解唯一」：若唯一的解不是自然數，就沒有自然數解。有一個數值商不代表整除。
• S04 · premise_audit · S03, nat_discrete, order_basics — 否定需要排除所有 k，S03 的等價或 nat_discrete 的兩段夾擠都做到了這一點；只檢查幾個 k 不夠。
• S03.3 · premise_audit · division_algorithm — 關鍵是帶餘除法的唯一性；若只有存在性，不能由一種寫法推出餘數為 0。沒有使用引理本身。
• S03.2 · premise_audit · S03.1, exists_intro — 只用到 q 是自然數；沒有使用引理本身。
• S03.1 · premise_audit · division_algorithm, order_basics — 需要 a>0 與 b≥0；這保證商可以當自然數見證。
• S03 · inverse_equivalence · L_rem_test — 引理的兩個方向（S03.2、S03.3）都已證；前提 a>0 是帶餘除法所需。
• S02 · premise_audit · S01, exists_intro, numeric_evaluation — 存在性只需一個見證；這一步不宣稱見證唯一（唯一性見 S09）。
• S01 · premise_audit · G1, G2, mko_dvd_def — 此步只展開定義；見證限定為自然數（G2），不是有理數。

錯誤控制與反例

有數值商不等於整除

MKO 指出的誤解：看到 b/a 是一個數就宣稱 a∣b。10/4=5/2 是有理數，但見證必須是自然數，所以 4∤10（S05）。判定要看自然數見證或餘數是否為 0。

除數為 0 不是一律不整除

MKO 指出的另一個誤解：把除數為零一律判成沒有整除關係。依定義 0∣b ⇔ b=0（S07），所以 0∣0 成立，0∤5。注意這裡沒有做「除以 0」，只是找乘數見證。

否定要排除所有見證

證明 6∤87 時，試 k=14、15 兩個值不夠；必須用餘數引理或 nat_discrete 的夾擠排除所有 k（S04）。同理，6∣3 不成立：3=6·(1/2) 的 1/2 不是自然數，3 除以 6 的餘數是 3。

• 4∣10，因為 10/4=2.5 是一個數 → reject — 見證必須是自然數；10=4·2+2，餘數 2≠0。
• 0 不整除任何數 → reject — 0=0·0，所以 0∣0。
• 0∣5 → reject — 對每個 k，0·k=0≠5。
• 6∣3，因為 3=6·(1/2) → reject — 1/2 不是自然數；3=6·0+3，餘數 3≠0。
• 0∣0 的見證唯一 → reject — 0=0·0=0·5，k=0 與 k=5 都是見證。

結論與限制

6∣84（見證 14）；6∤87（餘數 3）；4∤10（唯一的有理解 5/2 不是自然數，餘數 2）；每個 a 都整除 0（見證 0）；0∣b ⇔ b=0，所以 0∣0 而 0∤5，且 0∣0 的見證不唯一；a>0 時見證至多一個，存在時唯一；整除具自反性與遞移性，3∣84 的見證為 2·14=28。

• 帶餘除法（存在與唯一）作為前置規則引用，本稿只由它推出餘數判準 L_rem_test。
• 本稿只處理 ℕ；含負數的整數整除不在範圍內。

驗證及來源綁定

14 個本稿宣告算術檢查；只支持所列算式。

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: c7700b425af628e5a943830098f9039a8ba739a667d2577ec46189e0e2124324
• original source SHA-256: 1b68c27c071f5fe0cfe48fffd7605f00b4dfae82833e7c47a8a473157438e68f
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）