S01 · implies
Before
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.
Euclid and back-substitution for signed inputs
On this page
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 remaindera,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
S02 · implies
Before
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 · implies
Before
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 · implies
Before
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 · implies
Before
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 · implies
Before
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 · implies
Before
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 · implies
Before
(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 bounds
Check 0≤r below the nonzero divisor, and stop at r=0.
Restore signs
The 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)