# 負係數方程的全部整數解

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

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

derivation-mko-linear-diophantine-equation-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

−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





## 逐步主鏈

S01 · implies操作前

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

操作後

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

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

Euclid完整兩步給gcd3並回代Bezout式。



S02 · implies操作前

-6x+9y=15

操作後

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

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

任何解必使gcd整除右側，此例通過必要條件。



S03 · implies操作前

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

操作後

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

條件：d=3>0; d divides c

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

葉節點依據：calc

把Bezout係數乘c/d=5得一個整數特解，證充分性。



S04 · implies操作前

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

操作後

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

條件：無

規則：calc · 依賴：G1, S03

葉節點依據：calc

所有此參數值均給解，步長為b/d=3及−a/d=2。



S05 · equivalent操作前

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

操作後

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

條件：無

規則：calc · 依賴：G1, S03

葉節點依據：calc

任意解減特解，取得齊次整數關係。



S06 · implies操作前

2u=3v

操作後

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

條件：無

規則：calc · 依賴：G1, S05

葉節點依據：calc

模3中2·2≡1，故乘2可消去2，所有u必為3倍。



S07 · implies操作前

u=3t,\quad2u=3v

操作後

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

條件：無

規則：mko_definition · 依賴：G1, S04, S05, S06

葉節點依據：mko_definition

代回整數等式除非零3得v=2t，證任意解都在已列族內。



S08 · implies操作前

0x+9y=18

操作後

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

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

單零係數仍能求解，x完全自由，不得漏掉此分支。



S09 · implies操作前

0x+0y=c

操作後

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

條件：無

規則：calc · 依賴：G1, S08

葉節點依據：calc

雙零係數時左右變成0=c，分別所有整數對或無解，永不除以d=0。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- 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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-linear-diophantine-equation-01.json)