# 帶符號輸入的Euclid與回代

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-euclidean-algorithm/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-euclidean-algorithm-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

gcd(−84,30)=6，且(−84)·1+30·3=6。

exact整數的除法鏈、不變量、下降終止與Bezout；不聲稱複雜度最佳。





## 已知條件與符號


- calc


- G1 — 原輸入a=−84,b=30；主鏈使用|a|=84,|b|=30，gcd約定非負且gcd(0,0)=0。


- q,r — 帶餘除法商餘數
- a,b — 原signed輸入





## 規則與來源


- calc · prerequisite — 假設精確整數算術、帶餘除法、整除與gcd的定義；同餘等式始終綁定明示模數。
- mko_definition · cited — 逐步驗a=bq+r與0<=r<|b|，把gcd invariant、嚴格下降終止及最終非負gcd分開。extended版本回代並重驗ax+by=gcd；零輸入採gcd(0,0)=0且不執行除以零。 · mko-euclidean-algorithm





## 逐步主鏈

S01 · implies操作前

a=-84,\quad b=30

操作後

(|a|,|b|)=(84,30),\quad\gcd(a,b)=\gcd(84,30)

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

整除不受輸入負號影響，先正規化主鏈。



S02 · implies操作前

84,30

操作後

84=2\cdot30+24,\quad0\le24<30

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

第一步商2餘24，符合帶餘除法界。



S03 · implies操作前

30,24

操作後

30=1\cdot24+6,\quad0\le6<24

條件：無

規則：calc · 依賴：G1, S02

葉節點依據：calc

第二步商1餘6，餘數繼續下降。



S04 · implies操作前

24,6

操作後

24=4\cdot6+0,\quad0\le0<6

條件：無

規則：calc · 依賴：G1, S03

葉節點依據：calc

第三步餘數0，停止並保留最後非零值6。



S05 · implies操作前

u=qv+r,\quad d>0

操作後

d\mid u,v\iff d\mid v,r

條件：無

規則：calc · 依賴：G1, S02, S03, S04

葉節點依據：calc

r=u−qv與u=qv+r證兩方向整除不變，所以整鏈的共因數相同。



S06 · implies操作前

30>24>6>0

操作後

\gcd(84,30)=\gcd(6,0)=6

條件：無

規則：calc · 依賴：G1, S04, S05

葉節點依據：calc

正除數每步下降，非負整數不能無限嚴降，故終止；末gcd為6。



S07 · implies操作前

6=30-24,\quad24=84-2\cdot30

操作後

6=3\cdot30-84=(-84)\cdot1+30\cdot3

條件：無

規則：calc · 依賴：G1, S01, S02, S03, S06

葉節點依據：calc

回代得到正規化係數−1、3，再恢復原a負號為1、3。



S08 · implies操作前

(a,b)=(0,30)\text{ or }(0,0)

操作後

\gcd(0,30)=30,\quad\gcd(0,0)=0

條件：無

規則：mko_definition · 依賴：G1, S06

葉節點依據：mko_definition

單零輸入直接讀非零絕對值，雙零採明示慣例，均不執行零除法。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S06 — (0,30)有Bezout0·0+30·1=30；(0,0)取係數0、0得0。
- S07 · premise_audit · G1, S01, S02, S03, S06 — 直接核−84+90=6；此符號不可從gcd值猜測。
- S06 · premise_audit · G1, S04, S05 — 終止責任與不變量不同，兩者加上末狀態才證演算法。
- S05 · premise_audit · G1, S02, S03, S04 — 不變量說明為何末對(6,0)仍代表原gcd，而不只給一串計算。
- S04 · premise_audit · G1, S03 — 不可把最後餘數0當gcd，或再做6/0。
- S03 · premise_audit · G1, S02 — 6是正餘數而非終止0，仍須下一步。
- S02 · premise_audit · G1, S01 — 84−60=24且除數30非零。
- S01 · premise_audit · G1 — Bezout係數最後必恢復負號，不能直接沿正數係數。





## 錯誤控制與反例

餘數界每步核0≤r<非零除數，並於r=0停止。

符號恢復主鏈用絕對值，Bezout最後回原輸入。


- gcd(−84,30)=−6。 → reject — 本慣例gcd非負，正規化結果6。
- 最後餘數0就是gcd。 → reject — 最後非零除數6才是gcd。
- 原Bezout係數可取−1、3。 → reject — (−84)(−1)+30·3=174，不是6。





## 結論與限制

gcd(−84,30)=6，且(−84)·1+30·3=6。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: ab8873c7df2186d225549351554b2b4bea88decba7b0d72aeeb052a0d65fc9a4
- original source SHA-256: ab8873c7df2186d225549351554b2b4bea88decba7b0d72aeeb052a0d65fc9a4
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-euclidean-algorithm-01.json)