# Euclid and back-substitution for signed inputs

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

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-euclidean-algorithm-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

gcd(-84,30)=6, with (-84)*1+30*3=6.

Exact divisions, invariant, descent and Bezout; no optimal-complexity claim.





## Givens and symbols


- calc


- G1 — Original a=-84,b=30; the main chain uses absolute values 84,30; gcd is nonnegative and gcd(0,0)=0.


- q,r — division quotient and remainder
- a,b — original signed inputs





## 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 — At every nonzero-divisor step check a=bq+r and 0≤r<|b|, with quotient q and remainder r. Separate gcd invariance, descent/termination and the final nonnegative gcd. The extended version back-substitutes and rechecks ax+by=gcd; zero inputs use gcd(0,0)=0 without division by zero. · mko-euclidean-algorithm





## Main derivation

S01 · impliesBefore

a=-84,\quad b=30

After

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

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

Divisibility is unaffected by input signs, so normalize the main chain first.



S02 · impliesBefore

84,30

After

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

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

The first step has quotient 2 and remainder 24 within the division bounds.



S03 · impliesBefore

30,24

After

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

Conditions: none

Rule: calc · Uses: G1, S02

Leaf basis: calc

The next quotient is 1 and remainder 6, continuing descent.



S04 · impliesBefore

24,6

After

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

Conditions: none

Rule: calc · Uses: G1, S03

Leaf basis: calc

The third remainder is zero; stop and retain last nonzero value 6.



S05 · impliesBefore

u=qv+r,\quad d>0

After

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

Conditions: none

Rule: calc · Uses: G1, S02, S03, S04

Leaf basis: calc

r=u-qv and u=qv+r prove both directions of common-divisor invariance throughout the chain.



S06 · impliesBefore

30>24>6>0

After

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

Conditions: none

Rule: calc · Uses: G1, S04, S05

Leaf basis: calc

Positive divisors strictly decrease, so well-founded nonnegative integers force termination; the final gcd is 6.



S07 · impliesBefore

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

After

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

Conditions: none

Rule: calc · Uses: G1, S01, S02, S03, S06

Leaf basis: calc

Back-substitution gives coefficients -1,3 for 84,30, restored to 1,3 for original -84,30.



S08 · impliesBefore

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

After

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

Conditions: none

Rule: mko_definition · Uses: G1, S06

Leaf basis: mko_definition

A single zero returns the other absolute value; double zero uses the stated convention, with no zero division.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S06 — For (0,30), coefficients 0,1 give 30; for (0,0), coefficients 0,0 give 0.
- S07 · premise_audit · G1, S01, S02, S03, S06 — Check -84+90=6 directly; signs are not guessed from the gcd value.
- S06 · premise_audit · G1, S04, S05 — Termination differs from invariance; both plus the final state establish the algorithm.
- S05 · premise_audit · G1, S02, S03, S04 — The invariant explains why final pair (6,0) has the original gcd, beyond a list of calculations.
- S04 · premise_audit · G1, S03 — Do not use final remainder 0 as the gcd or perform 6/0.
- S03 · premise_audit · G1, S02 — 6 is a positive remainder rather than terminating zero, so another step is needed.
- S02 · premise_audit · G1, S01 — 84-60=24 and divisor 30 is nonzero.
- S01 · premise_audit · G1 — Bezout coefficients must later restore the negative sign.





## Error controls and negative controls

Remainder boundsCheck 0≤r below the nonzero divisor, and stop at r=0.

Restore signsThe main chain uses absolute values; restore original signs for Bezout.


- gcd(-84,30)=-6. → reject — The gcd is nonnegative under this convention, giving 6.
- The last remainder 0 is the gcd. → reject — The last nonzero divisor 6 is the gcd.
- Original Bezout coefficients are -1,3. → reject — (-84)(-1)+30*3=174, not 6.





## Result and limitations

gcd(-84,30)=6, with (-84)*1+30*3=6.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: ab8873c7df2186d225549351554b2b4bea88decba7b0d72aeeb052a0d65fc9a4
- original source SHA-256: ab8873c7df2186d225549351554b2b4bea88decba7b0d72aeeb052a0d65fc9a4
- 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-euclidean-algorithm-01.json)