# The normalized inverse of 17 modulo 43

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

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-modular-inverse-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

The unique inverse residue class of 17 modulo 43 is represented by 38; 17*38=15*43+1.

Exact Euclid and Bezout for n≥2, with a nonunit boundary.





## Givens and symbols


- calc


- G1 — a=17, n=43; require 0≤x<43 and 17x congruent to 1 modulo 43.


- x — normalized inverse representative
- y — Bezout coefficient of the modulus





## 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 extended Euclid for an exact Bezout certificate a*x+n*y=1 and return the normalized representative 0≤x mod n<n. Modulus zero is invalid, and this slice requires n≥2. A nonunit explicitly has no inverse; approximate division is not used. · mko-modular-inverse





## Main derivation

S01 · impliesBefore

a=17,\quad n=43

After

n\ge2,\quad43=2\cdot17+9,\quad0\le9<17

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

The modulus domain is valid; the first exact division gives remainder 9.



S02 · impliesBefore

17,9

After

17=1\cdot9+8,\quad9=1\cdot8+1,\quad8=8\cdot1+0

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

The complete division chain has remainders 8,1,0, each below its nonzero divisor.



S03 · impliesBefore

u=qv+r

After

d\mid u,v\iff d\mid v,r;\quad\gcd(17,43)=1

Conditions: none

Rule: calc · Uses: G1, S01, S02

Leaf basis: calc

Common divisors are preserved in both directions using r=u-qv and u=qv+r; the last nonzero remainder 1 is the gcd.



S04 · impliesBefore

1=9-8,\quad8=17-9,\quad9=43-2\cdot17

After

1=2\cdot43-5\cdot17

Conditions: none

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

Leaf basis: calc

Back-substitution gives Bezout coefficients x=-5,y=2 for the original inputs.



S05 · impliesBefore

17(-5)+43(2)=1

After

-5\equiv38\pmod{43},\quad0\le38<43

Conditions: none

Rule: calc · Uses: G1, S04

Leaf basis: calc

Add 43 to the negative Bezout coefficient to normalize the candidate to 38.



S06 · impliesBefore

x=38

After

17\cdot38=646=15\cdot43+1\Rightarrow17\cdot38\equiv1\pmod{43}

Conditions: none

Rule: mko_definition · Uses: G1, S05

Leaf basis: mko_definition

An independent exact product check confirms the candidate is an inverse.



S07 · impliesBefore

17x\equiv17x'\equiv1\pmod{43}

After

43\mid17(x-x');\quad x-x'=(2\cdot43-5\cdot17)(x-x')\Rightarrow43\mid x-x'

Conditions: none

Rule: calc · Uses: G1, S04, S06

Leaf basis: calc

Use the established Bezout identity to cancel 17 and prove uniqueness modulo 43.



S08 · impliesBefore

6x+15y=1\text{ proposed}

After

3\mid6x+15y\text{ but }3\nmid1\Rightarrow6\text{ has no inverse mod }15

Conditions: none

Rule: calc · Uses: G1, S03

Leaf basis: calc

For nonunit 6 modulo 15, gcd 3 makes Bezout 1 impossible; rational 1/6 is not a modular inverse.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S03 — The obstruction applies to all integer x,y, not just a bounded search.
- S07 · premise_audit · G1, S04, S06 — Only if both are normalized to 0 through 42 does the multiple-of-43 difference force integer equality.
- S06 · premise_audit · G1, S05 — The equality is in Z before passing to congruence modulo 43.
- S05 · premise_audit · G1, S04 — -5 and 38 represent the same inverse class, not distinct inverse classes.
- S04 · premise_audit · G1, S01, S02, S03 — Directly check 86-85=1; a sign error would invalidate the inverse.
- S03 · premise_audit · G1, S01, S02 — The gcd is not guessed; the full chain and divisor invariant prove it.
- S02 · premise_audit · G1, S01 — Stop at remainder zero without a subsequent division by zero.
- S01 · premise_audit · G1 — The divisor 17 is nonzero and the remainder bound is explicit; no approximate division is used.





## Error controls and negative controls

SignBack-substitution gives -5, not 5.

Modulus domainThis slice requires n≥2, excluding 0 and 1.


- The inverse is 5. → reject — 17*5=85 is 42, not 1, modulo 43.
- The inverse of 6 modulo 15 is 1/6. → reject — Every 6x+15y is divisible by 3 and cannot equal 1.
- An inverse is unique as an integer. → reject — 38 and -5 both satisfy the congruence; normalization selects 38.





## Result and limitations

The unique inverse residue class of 17 modulo 43 is represented by 38; 17*38=15*43+1.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: ad89135f0921bf66f257e43757b32ec3605667deebbc8f37408286760c155399
- original source SHA-256: b707f2a218c25be9424d71c4a6c7ef3f1dc204d7cee86331914a9182b0e19932
- 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-modular-inverse-01.json)