# Question 69: Normalize the Inverse Representative, Not the Bezout Coefficients

[Return to catalogue page 1](https://ocme.evemisslab.com/en/questions/)

[← Question derivation index](https://ocme.evemisslab.com/en/questions/) · [Original question batch](https://ocme.evemisslab.com/en/practice/batch-20261014-advance-20261103-r07-modular-inverse-foundations/#q-20261014-advance-20261103-r07-modular-inverse-0069)

This teaching derivation has second-context AI mathematical and bilingual semantic review, limited to the model and assumptions stated in this question. It has no human review or new Lean proof and does not promote the original question or MKO to Canonical truth.

P250-0069 · q-20261014-advance-20261103-r07-modular-inverse-0069



## Original question and givens

Use the original signed integer a=2 and modulus n=45≥2. Exact extended Euclid gives nonnegative g=gcd(a,n) and signed coefficients x,y satisfying a*x+n*y=g. An inverse exists exactly when g=1; normalize its representative to 0≤inverse<n. Uniqueness means one residue class modulo n, not a unique integer representative. This family excludes moduli 0 and 1 and does not use approximate division. Require gcd(a,n)=1. Give (a,n,inverse,product_mod_n,valid?,unique_modulo_n).


- G001 — Use the original signed integer a=2 and modulus n=45≥2. Exact extended Euclid gives nonnegative g=gcd(a,n) and signed coefficients x,y satisfying a*x+n*y=g. An inverse exists exactly when g=1; normalize its representative to 0≤inverse<n. Uniqueness means one residue class modulo n, not a unique integer representative. This family excludes moduli 0 and 1 and does not use approximate division. Require gcd(a,n)=1. Give (a,n,inverse,product_mod_n,valid?,unique_modulo_n).





## Definition and scope

Use integer modulus n≥2 with gcd(a,n)=1. Uniqueness concerns the residue class and its representative in the declared interval.


- [mko-modular-inverse](https://ocme.evemisslab.com/en/mko/mko-modular-inverse/)





## Step-by-step derivation

S001 · impliesBefore

a=2, modulus=45

After

n=45≥2; seek u with 2u≡1 (mod 45)

Conditions: none

Fix the modulus and inverse condition; the integer product need not equal 1.

Step identifiers and dependenciesRule: inverse_definition · Uses: G001





S002 · impliesBefore

divide 2 by 45

After

2=0·45+2

Conditions: 0≤2<45

The quotient is 0 and remainder 2; continue with the preceding divisor and remainder.

Step identifiers and dependenciesRule: euclidean_division · Uses: G001, S001





S003 · impliesBefore

divide 45 by 2

After

45=22·2+1

Conditions: 0≤1<2

The quotient is 22 and remainder 1; continue with the preceding divisor and remainder.

Step identifiers and dependenciesRule: euclidean_division · Uses: G001, S002





S004 · impliesBefore

divide 2 by 1

After

2=2·1+0

Conditions: 0≤0<1

The quotient is 2 and remainder 0; continue with the preceding divisor and remainder.

Step identifiers and dependenciesRule: euclidean_division · Uses: G001, S003





S005 · impliesBefore

last nonzero Euclidean remainder

After

gcd(2,45)=1; 2·(-22)+45·(1)=1

Conditions: none

Track integer linear combinations along the division chain to obtain this explicit Bezout identity.

Step identifiers and dependenciesRule: bezout_identity · Uses: G001, S004





S006 · impliesBefore

2·(-22)+45·(1)=1

After

-22 mod 45=23; 0≤23<45

Conditions: none

The coefficient of a represents the inverse class; reduce it to the required representative interval.

Step identifiers and dependenciesRule: normalize_residue · Uses: G001, S005





S007 · calculationBefore

a·u := mul(2, 23)

After

a·u = 46

Conditions: none

Multiply the original a by the normalized inverse.

Step identifiers and dependenciesRule: exact_rational_arithmetic · Uses: G001, S006





S008 · impliesBefore

a·u=46

After

46=1·45+1 ⇒ a·u mod n=1

Conditions: none

The product minus 1 is an integer multiple of the modulus, verifying the inverse condition.

Step identifiers and dependenciesRule: congruence_check · Uses: G001, S007





S009 · impliesBefore

a·v≡a·u≡1 (mod n), gcd(a,n)=1

After

n divides v−u; if 0≤u,v<n then u=v

Conditions: none

From n|a(v−u), multiply the Bezout identity by v−u to get n|(v−u). Two normalized representatives differ by less than n in absolute value, so their difference is zero.

Step identifiers and dependenciesRule: inverse_uniqueness · Uses: G001, S008









## Reverse checks


- S009 · premise_and_result_audit — The class and its normalized representative are unique; u+kn gives other integer representatives.
- S008 · premise_and_result_audit — The quotient is an integer and the remainder really is 1.
- S007 · premise_and_result_audit — Recompute a·u with exact rational arithmetic, not rounded decimals.
- S006 · premise_and_result_audit — Normalize the inverse representative, not both Bezout coefficients.
- S005 · premise_and_result_audit — Multiply out the identity directly rather than trusting a gcd label.
- S004 · premise_and_result_audit — Check both the division identity and 0≤remainder<divisor.
- S003 · premise_and_result_audit — Check both the division identity and 0≤remainder<divisor.
- S002 · premise_and_result_audit — Check both the division identity and 0≤remainder<divisor.
- S001 · premise_and_result_audit — A modular inverse requires gcd(a,n)=1.





## Result

(2, 45, 23, 1, Yes, unique_modulo_n)

The inverse representative is 23, unique modulo 45.





## This question review and source binding

Review date: 2026-10-24

Original questions, answers, step expressions, numeric ASTs and historical records are retained. Source candidate labels remain historical and are not overwritten as formal proof.

Source hashes and review receipts
- input commit: 0f7be61e2c22317a4075561dc822c87d881a50db
- original question SHA-256: 560635a2c92330ab16ddb52e8402626013976291a60361ad42e5c811efc87bb2
- candidate record SHA-256: 1b2ce9ad16f52482fe5c8a69cf3fc559aee573c3d7de14f708af963b7c3f418f
- semantic review receipt SHA-256: 4727d1bd957a9b7f6cadb7972ddb5ab80a31f5259dc5394c1dff2b71944ed36b
- question-first witness SHA-256: 51e18649133238ac992229f6e16542a5f3af53ca73b2262ab0524508ea937dee
- Lean: NOT_RUN · human review: NOT_PERFORMED

[Same-source full JSON](https://ocme.evemisslab.com/data/question-derivations/questions/q-20261014-advance-20261103-r07-modular-inverse-0069.json)