# All integer solutions with a negative coefficient

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-linear-diophantine-equation/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

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



## Goal and scope

All integer solutions of -6x+9y=15 are x=5+3t,y=5+2t, t in Z.

An exact two-variable integer equation, complete parameterization and zero-coefficient cases.





## Givens and symbols


- calc


- G1 — a=-6,b=9,c=15; x,y are integers and gcd is nonnegative.


- t — arbitrary integer parameter
- d — nonnegative gcd





## Rules and sources


- calc · prerequisite — Assume exact integer arithmetic, division with remainder, and definitions of divisibility and gcd; every congruence has an explicit modulus.
- mko_definition · cited — Use an extended Euclidean Bezout certificate for a particular solution. If d=gcd(a,b) divides c, all solutions are x=x0+(b/d)t and y=y0−(a/d)t, t∈Z. When a=b=0, c=0 permits every integer pair and c≠0 permits none; never divide by d=0. · mko-linear-diophantine-equation





## Main derivation

S01 · impliesBefore

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

After

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

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

Two complete Euclidean steps give gcd 3 and its Bezout identity.



S02 · impliesBefore

-6x+9y=15

After

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

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

Every solution requires the gcd to divide the right side, which holds here.



S03 · impliesBefore

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

After

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

Conditions: d=3>0; d divides c

Rule: calc · Uses: G1, S01, S02

Leaf basis: calc

Scaling Bezout coefficients by c/d=5 constructs an integer particular solution, proving sufficiency here.



S04 · impliesBefore

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

After

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

Conditions: none

Rule: calc · Uses: G1, S03

Leaf basis: calc

Every parameter value solves the equation, with steps b/d=3 and -a/d=2.



S05 · equivalentBefore

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

After

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

Conditions: none

Rule: calc · Uses: G1, S03

Leaf basis: calc

Subtract the particular solution from an arbitrary solution to get the homogeneous integer relation.



S06 · impliesBefore

2u=3v

After

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

Conditions: none

Rule: calc · Uses: G1, S05

Leaf basis: calc

Since 2*2=1 modulo 3, multiplication by 2 cancels the factor, forcing u to be a multiple of 3.



S07 · impliesBefore

u=3t,\quad2u=3v

After

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

Conditions: none

Rule: mko_definition · Uses: G1, S04, S05, S06

Leaf basis: mko_definition

Substitute back and divide the integer equality by nonzero 3 to get v=2t, proving completeness.



S08 · impliesBefore

0x+9y=18

After

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

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

A single zero coefficient is solvable with x entirely free; this case must not be omitted.



S09 · impliesBefore

0x+0y=c

After

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

Conditions: none

Rule: calc · Uses: G1, S08

Leaf basis: calc

Double-zero coefficients reduce to 0=c, giving all integer pairs or none, never division by gcd zero.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S09 · premise_audit · G1, S08 — For c=0 the solution set cannot be reduced to the one pair (0,0).
- S08 · premise_audit · G1 — Here gcd(0,9)=9 is nonzero, unlike double-zero degeneracy.
- S07 · premise_audit · G1, S04, S05, S06 — S04 proves every parameter is a solution; S05-S07 prove every solution has a parameter.
- S06 · premise_audit · G1, S05 — Cancellation uses the explicitly known inverse 2, not unconditional modular division.
- S05 · inverse_equivalence · G1, S03 — Division by 3 is exact on both sides and loses no solutions.
- S04 · premise_audit · G1, S03 — The negative a makes y's step positive 2, not -2.
- S03 · premise_audit · G1, S01, S02 — d=3 is nonzero and c/d is integral, so scaling is valid.
- S02 · premise_audit · G1, S01 — This is only necessity; the next step constructs a solution.
- S01 · premise_audit · G1 — The original -6 sign is restored, and coefficients 1,1 check directly.





## Error controls and negative controls

CompletenessSubstitution proves only that the family consists of solutions; subtract a particular solution to prove the converse.

Normalized gcdd=3, not -3, with step sizes 3 and 2.


- Listing (5,5) gives all solutions. → reject — t=1 gives the distinct solution (8,7).
- The y-step should be -2. → reject — x=5+3t,y=5-2t gives 15-36t, not identically 15.
- Double-zero coefficients allow c/d with d=0. → reject — Zero division is invalid; split on 0=c first.





## Result and limitations

All integer solutions of -6x+9y=15 are x=5+3t,y=5+2t, t in Z.







## Verification and source binding

2 declared checks for this guide; only the listed expressions are covered.


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

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-linear-diophantine-equation-01.json)