最大公因數與互質：以整除刻畫驗證歐幾里得算法

目標與範圍

依 MKO 的整除刻畫（d∣a、d∣b，且每個公因數 c 都整除 d）：(1) 證明滿足刻畫的 d 至多一個；(2) 證明歐幾里得算法每一步保持公因數集合且必會停止，並以它算出 gcd(84,36)=12，再直接驗證 12 滿足刻畫；(3) 說明公因數 6 不是 gcd；(4) 算出 gcd(8,15)=1，說明 8 與 15 互質但都不是質數；(5) 處理含 0 的情形 gcd(0,1)=1、gcd(0,6)=6、gcd(0,0)=0。

在包含 0 的自然數中，以整除刻畫定義 gcd（MKO 假設 a1、a2）。歐幾里得算法的正確性由「每步保持公因數集合」與「gcd(x,0)=x」兩個事實推出，停止性由良序原理推出。不處理 Bézout 等式、負整數或多個數的 gcd；不改動 canonical MKO 或英文 edition。

已知條件與符號

• division_algorithm
• order_basics
• distributive
• well_ordering
• numeric_evaluation

• G1 — a、b 是自然數，可以為 0（MKO 假設 a1）；整除依 MKO 自然數整除的定義，見證須為自然數。
• G2 — 歐幾里得算法（MKO 段落 0）：當 y≠0 時，把 (x,y) 換成 (y, x mod y)；y=0 時輸出 x。(0,0) 依約定輸出 0。
• G3 — 輸入：(84,36)、(8,15)、(0,1)、(0,6)、(0,0)。

• \gcd(a,b) — 最大公因數（整除刻畫）
• \mathrm{CD}(a,b) — a、b 的公因數集合
• (x,y)\mapsto(y,\,x\bmod y) — 歐幾里得算法的一步（y>0）
• c\mid x — c 整除 x

規則與來源

• 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。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• well_ordering · prerequisite — 良序原理：ℕ 的每個非空子集都有最小元素。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。
• 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)。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
• set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• logic_chain · prerequisite — 推論的傳遞：由 P⇒Q 與 Q⇒R 得 P⇒R；⇔ 同理。
• eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
• mko_gcd_def · cited — 自然數 d=gcd(a,b) 由 d∣a、d∣b，且每個同時整除 a、b 的自然數 c 都滿足 c∣d 刻畫。採 gcd(0,0)=0；a、b 互質表示 gcd(a,b)=1。 · mko-gcd-coprime
• mko_dvd_def · cited — 對自然數 a、b，a∣b 當且僅當存在自然數 k 使 b=a·k。 · mko-natural-divisibility
• dvd_basic · prerequisite — 自然數整除的基本事實：a∣a（a=a·1）；a∣0（0=a·0）；a>0 時 a∣b ⇔ b 除以 a 的餘數為 0。
• L_dvd_antisymm · lemma — 對自然數 d、e：若 d∣e 且 e∣d，則 d=e。
• L_cd_step · lemma — 對自然數 x、y、q、r，若 y>0 且 x=yq+r，則每個自然數 c 都有 (c∣x 且 c∣y) ⇔ (c∣y 且 c∣r)。

逐步主鏈

d=\gcd(a,b)

d\mid a\ \land\ d\mid b\ \land\ \forall c\in\mathbb{N}\,(c\mid a\land c\mid b\Rightarrow c\mid d)

d,\ d'\ \text{both satisfy S01 for}\ (a,b)

d=d'

(x,0)

x\ \text{satisfies S01 for}\ (x,0),\ \text{so}\ \gcd(x,0)=x

x=yq+r,\ y>0

c\mid x\land c\mid y\iff c\mid y\land c\mid r

x=yq+r,\ y>0

d\ \text{satisfies S01 for}\ (x,y)\iff d\ \text{satisfies S01 for}\ (y,r)

(84,36)

84=36\cdot 2+12,\ 0\le 12<36;\ (84,36)\mapsto(36,12)

(36,12)

36=12\cdot 3+0;\ (36,12)\mapsto(12,0)

\gcd(12,0)=12

\gcd(84,36)=\gcd(36,12)=\gcd(12,0)=12

(x,y)\mapsto(y,\,x\bmod y),\ y>0

\text{the algorithm stops after finitely many steps}

d=12

12\mid 84,\ 12\mid 36,\ (c\mid 84\land c\mid 36\Rightarrow c\mid 12)

6\mid 84,\ 6\mid 36

12\nmid 6,\ \text{so}\ 6\neq\gcd(84,36)

(8,15)

(8,15)\mapsto(15,8)\mapsto(8,7)\mapsto(7,1)\mapsto(1,0);\ \gcd(8,15)=1

\gcd(8,15)=1,\ 8=2\cdot 4,\ 15=3\cdot 5

8,15\ \text{coprime, neither prime}

(0,1),\ (0,6),\ (0,0)

\gcd(0,1)=1,\ \gcd(0,6)=6,\ \gcd(0,0)=0

局部子步與引理

e=dk,\ d=el,\ d=0

e=0=d

d=el=d(kl),\ d>0

kl=1,\ k=1,\ e=d

y=cu,\ r=cv

x=c(uq+v),\ \text{so}\ c\mid x

x=cs,\ y=cu,\ y>0

r=c(s-uq),\ s-uq\in\mathbb{N},\ \text{so}\ c\mid r

逐步反向審查

• S14 · premise_audit · S03, S05, dvd_basic — (0,1) 與 (0,6) 用算法一步加 S03、S05；(0,0) 直接用 S03。
• S13 · premise_audit · S12, mko_gcd_def — 只用互質的定義與兩個非平凡因數見證。
• S12 · premise_audit · S03, S05, division_algorithm — 與 S06 到 S08 相同的結構；每一步的餘數都滿足 0≤r<y。
• S11 · premise_audit · S01, S10, order_basics — 否定只需一個不整除 6 的公因數（12）。
• S10 · premise_audit · S04, S06, mko_gcd_def — 第二部分是對所有公因數的一般論證，不是只看列出的六個；列出的只是例子。
• S09 · premise_audit · division_algorithm, well_ordering, contradiction — 停止性只需 r<y 與良序原理；它保證 S08 的回推從有限的終點開始。
• S08 · premise_audit · S03, S05, S06, S07, logic_chain — 從算法終點往回套用 S05；每一步的前提 y>0 都已確認（36>0、12>0）。
• S07 · premise_audit · division_algorithm, numeric_evaluation — 餘數 0 滿足 0≤0<12。
• S06 · premise_audit · division_algorithm, numeric_evaluation — 需要 0≤12<36，這使 12 是唯一的餘數。
• S05 · inverse_equivalence · S04, set_extensionality — 集合相等是雙向的，所以刻畫的等價也是雙向的。
• S04.2 · premise_audit · order_basics, distributive, contradiction — 自然數減法 s−uq 只有在 s≥uq 時才是自然數，所以先證 s≥uq；這需要 c>0，由 y>0 保證。沒有使用引理本身。
• S04.1 · premise_audit · distributive, mul_assoc, exists_intro — 只用分配律與 ℕ 對加法、乘法封閉；沒有使用引理本身。
• S04 · inverse_equivalence · L_cd_step — 引理的兩個方向分別在 S04.1、S04.2 證明。
• S03 · premise_audit · S01, S02, dvd_basic — 兩部分刻畫都已檢查；唯一性來自 S02。
• S02.2 · premise_audit · order_basics, mul_assoc, case_analysis — 兩種情況 d=0、d>0 涵蓋所有自然數 d；沒有使用引理本身。
• S02.1 · premise_audit · mko_dvd_def, mul_zero — 只用乘以零；沒有使用引理本身。
• S02 · premise_audit · S01, L_dvd_antisymm — 只用兩個候選各自的刻畫；存在性另由算法給出（S08）。
• S01 · premise_audit · G1, mko_gcd_def — 此步只展開定義；驗證候選 d 時兩部分都要檢查（MKO 段落 1）。

錯誤控制與反例

公因數不一定是最大公因數

MKO 指出的誤解：把任何共同因數稱為最大公因數。6 同時整除 84 與 36，但公因數 12 不整除 6，刻畫第二部分失敗（S11）。驗證候選時必須檢查所有公因數都整除它，只找到一個大的公因數不夠。

互質不要求兩數是質數

MKO 指出的另一個誤解：以為互質的兩數都必須是質數。8 與 15 都不是質數，卻互質；0 與 1 也互質（S13、S14）。

自然數減法要先確認不為負

S04.2 中 r=c(s−uq) 必須先證 s≥uq，s−uq 才是自然數，見證才合法；這一步用到 c>0，而 c>0 來自 y>0。

• 6 是 84 與 36 的最大公因數，因為 6 同時整除兩者 → reject — 公因數 12 不整除 6；gcd(84,36)=12。
• 8 與 15 不互質，因為兩者都不是質數 → reject — gcd(8,15)=1，所以互質。
• 0 與 6 互質 → reject — gcd(0,6)=6≠1；2 同時整除 0 與 6。
• gcd(0,0) 不存在，因為每個數都整除 0 → reject — 依整除刻畫，0 是公因數且每個公因數都整除 0，所以 gcd(0,0)=0，與 MKO 約定一致。

結論與限制

滿足整除刻畫的 gcd 至多一個；歐幾里得算法每步保持公因數集合且必停止。gcd(84,36)=12（84→36→12→0），12 直接滿足刻畫；公因數 6 不是 gcd，因為 12∤6。gcd(8,15)=1，所以 8 與 15 互質，雖然兩者都不是質數。gcd(0,1)=1（互質）、gcd(0,6)=6（不互質）、gcd(0,0)=0（與刻畫一致）。

• Bézout 等式（gcd 可寫成兩數的整數線性組合）不在本稿處理。
• dvd_basic 與帶餘除法作為前置規則使用；前者的證明見自然數整除的教學稿，本稿不重證。

驗證及來源綁定

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

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

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