# 17模43的正規化逆元

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-modular-inverse/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-modular-inverse-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

17模43的唯一逆類為38；17·38=15·43+1。

n≥2的exact Euclid與Bezout證書，另列nonunit邊界。





## 已知條件與符號


- calc


- G1 — a=17，n=43，要求0≤x<43及17x≡1 mod43。


- x — 正規化逆元代表
- y — Bezout模數係數





## 規則與來源


- calc · prerequisite — 假設精確整數算術、帶餘除法、整除與gcd的定義；同餘等式始終綁定明示模數。
- mko_definition · cited — 使用extended Euclid給exact Bezout certificate ax+ny=1，輸出0≤x mod n<n。modulus0無效；本輪限制n≥2。nonunit明示無inverse，不以除法近似。 · mko-modular-inverse





## 逐步主鏈

S01 · implies操作前

a=17,\quad n=43

操作後

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

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

模數域合法；第一個帶餘除法給餘數9。



S02 · implies操作前

17,9

操作後

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

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

完整除法鏈的餘數依序8、1、0，均小於非零除數。



S03 · implies操作前

u=qv+r

操作後

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

條件：無

規則：calc · 依賴：G1, S01, S02

葉節點依據：calc

共因數集合不變：r=u−qv與u=qv+r給雙方向；最後非零餘數1即gcd。



S04 · implies操作前

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

操作後

1=2\cdot43-5\cdot17

條件：無

規則：calc · 依賴：G1, S01, S02, S03

葉節點依據：calc

逐式回代給原輸入的Bezout係數x=−5、y=2。



S05 · implies操作前

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

操作後

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

條件：無

規則：calc · 依賴：G1, S04

葉節點依據：calc

把負Bezout係數加43正規化，得到候選38。



S06 · implies操作前

x=38

操作後

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

條件：無

規則：mko_definition · 依賴：G1, S05

葉節點依據：mko_definition

整數乘積再核，證候選真是逆元。



S07 · implies操作前

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

操作後

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

條件：無

規則：calc · 依賴：G1, S04, S06

葉節點依據：calc

以已證Bezout式消去17，證逆元只在模43意義下唯一。



S08 · implies操作前

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

操作後

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

條件：無

規則：calc · 依賴：G1, S03

葉節點依據：calc

nonunit示例gcd(6,15)=3，不可能給Bezout1，因此不能用有理1/6代替模逆元。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S03 — 此無解證書對所有整數x、y成立，不僅有限搜尋。
- S07 · premise_audit · G1, S04, S06 — 若x與x'均在0到42，差為43倍且絕對值小43，才得整數相等。
- S06 · premise_audit · G1, S05 — 等式先在Z成立，再推出模43同餘，不混淆兩層。
- S05 · premise_audit · G1, S04 — −5與38是同一逆類，不是兩個不同逆元類。
- S04 · premise_audit · G1, S01, S02, S03 — 直接核86−85=1；符號錯誤會使逆元失效。
- S03 · premise_audit · G1, S01, S02 — gcd不只是猜1，已由整條鏈與共因數不變證明。
- S02 · premise_audit · G1, S01 — 到餘數0停止，不能再除以0。
- S01 · premise_audit · G1 — 除數17非零且餘數界明列，沒有近似除法。





## 錯誤控制與反例

負號回代係數為−5，不是5。

模數域本輪只允許n≥2，n=0或1不採用。


- 逆元為5。 → reject — 17·5=85≡42而非1 mod43。
- 6模15的逆元可寫1/6。 → reject — 3整除任何6x+15y，不可能等1。
- 逆元作整數唯一。 → reject — 38與−5均滿足同餘，只在正規化範圍選38。





## 結論與限制

17模43的唯一逆類為38；17·38=15·43+1。







## 驗證及來源綁定

2 個本稿宣告算術檢查；只支持所列算式。


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: ad89135f0921bf66f257e43757b32ec3605667deebbc8f37408286760c155399
- original source SHA-256: b707f2a218c25be9424d71c4a6c7ef3f1dc204d7cee86331914a9182b0e19932
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-modular-inverse-01.json)