負係數方程的全部整數解

目標與範圍

−6x+9y=15全部解為x=5+3t,y=5+2t，t∈Z。

二變數精確整數方程、完整參數化及零係數分支。

已知條件與符號

• calc

• G1 — a=−6,b=9,c=15；x,y須為整數，gcd使用非負慣例。

• t — 任意整數參數
• d — 非負gcd

規則與來源

• calc · prerequisite — 假設精確整數算術、帶餘除法、整除與gcd的定義；同餘等式始終綁定明示模數。
• mko_definition · cited — 使用extended Euclidean Bézout證書構造particular solution；若d=gcd(a,b)整除c，全部解為x=x0+(b/d)t、y=y0-(a/d)t。a=b=0時c=0有所有整數對，c非零則無解且不得除以d=0。 · mko-linear-diophantine-equation

逐步主鏈

9=1\cdot6+3,\quad6=2\cdot3+0

d=\gcd(-6,9)=3,\quad3=(-6)\cdot1+9\cdot1

-6x+9y=15

3\mid(-6x+9y),\quad3\mid15

3=(-6)1+9(1),\quad15=5\cdot3

x_0=5,\quad y_0=5,\quad-6(5)+9(5)=15

x=5+3t,\quad y=5+2t,\quad t\in\mathbb Z

-6x+9y=15+(-18+18)t=15

(x,y)\text{ any solution},\quad u=x-5,\ v=y-5

-6u+9v=0\iff2u=3v

2u=3v

2u\equiv0\pmod3\Rightarrow u\equiv0\pmod3\Rightarrow u=3t

u=3t,\quad2u=3v

v=2t,\quad x=5+3t,\ y=5+2t

0x+9y=18

y=2,\quad x\in\mathbb Z\text{ arbitrary}

0x+0y=c

c=0\Rightarrow\mathbb Z^2;\qquad c\ne0\Rightarrow\varnothing

局部子步與引理

本稿無局部子步。

逐步反向審查

• S09 · premise_audit · G1, S08 — c=0時不能把參數族縮成單一解(0,0)。
• S08 · premise_audit · G1 — 此處gcd(0,9)=9非零，並非雙零退化。
• S07 · premise_audit · G1, S04, S05, S06 — S04給每個參數是解，S05至S07給每個解有參數，兩方向完備。
• S06 · premise_audit · G1, S05 — 消去用已明示的逆2，不是任意模數都能消去。
• S05 · inverse_equivalence · G1, S03 — 除3合法且兩邊均可整除，沒有丟解。
• S04 · premise_audit · G1, S03 — 係數負號使y步長為正2，不是−2。
• S03 · premise_audit · G1, S01, S02 — d=3非零，c/d是整數，因此縮放合法。
• S02 · premise_audit · G1, S01 — 這只證必要性；存在解仍由下一步構造。
• S01 · premise_audit · G1 — −6原符號已恢復，1、1係數直接核正確。

錯誤控制與反例

完整性

代回只證族內都是解，還需任意解減特解證反向。

gcd正規化

d=3而非−3，步長分別3、2。

• 只需列(5,5)便是全部解。 → reject — t=1給不同解(8,7)。
• y步長應為−2。 → reject — x=5+3t,y=5−2t使左側15−36t，不恒等15。
• 雙零係數可使用c/d且d=0。 → reject — 除零非法，必先分0=c兩分支。

結論與限制

−6x+9y=15全部解為x=5+3t,y=5+2t，t∈Z。

驗證及來源綁定

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

• source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
• adopted source SHA-256: 51507b62feb5851a8cf0c74a7f420b24a166be908dc2a9f02c03852a04af9026
• original source SHA-256: 4e219790cfd274009340791ffd283bde4d21693b21fdc40ee88a5d801a4090e1
• Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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