帶符號輸入的Euclid與回代

目標與範圍

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

逐步主鏈

a=-84,\quad b=30

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

84,30

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

30,24

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

24,6

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

u=qv+r,\quad d>0

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

30>24>6>0

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

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

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

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

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

局部子步與引理

本稿無局部子步。

逐步反向審查

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