三模數CRT的構造與唯一類

目標與範圍

x≡2 mod3、3 mod5、2 mod7的全部整數解為23+105t。

正pairwise-coprime主例及noncoprime相容界線，所有算術精確。

已知條件與符號

• calc

• G1 — 模數3、5、7，residues依序2、3、2，t∈Z。

• M — 三模數乘積
• N_i,u_i — 權重與模逆元

規則與來源

• calc · prerequisite — 假設精確整數算術、帶餘除法、整除與gcd的定義；同餘等式始終綁定明示模數。明示假設互質整數的Bezout恆等式。
• mko_definition · cited — residues正規化，使用modular inverses構造x並核全部congruences。唯一性是mod product而非integer unique。modulus0無效；noncoprime不在CRT假設內但可相容，需pairwise gcd compatibility且一般mod lcm唯一。 · mko-chinese-remainder-theorem

逐步主鏈

(m_1,m_2,m_3)=(3,5,7)

\gcd(3,5)=\gcd(3,7)=\gcd(5,7)=1,\quad M=105

N_i=M/m_i

(N_1,N_2,N_3)=(35,21,15)

35\equiv2\pmod3,\quad21\equiv1\pmod5,\quad15\equiv1\pmod7

u_1=2,\quad u_2=1,\quad u_3=1

x_*=\sum_{i=1}^3 a_iN_iu_i

x_*=2\cdot35\cdot2+3\cdot21+2\cdot15=233

x_*=233

x_0=233-2\cdot105=23,\quad0\le23<105

x_0=23

23=7\cdot3+2=4\cdot5+3=3\cdot7+2

m,n\mid d,\quad\gcd(m,n)=1,\quad um+vn=1

d=mk,\quad k=umk+vnk\Rightarrow n\mid k\Rightarrow mn\mid d

x,x'\text{ solve the system}

105\mid x-x';\quad x=23+105t,\quad t\in\mathbb Z

x\equiv1\pmod4,\quad x\equiv3\pmod6

x=9+12t\text{ solves};\quad\gcd(4,6)=2,\ 1\equiv3\pmod2

局部子步與引理

本稿無局部子步。

逐步反向審查

• S09 · premise_audit · G1, S08 — x≡1 mod4、2 mod6則奇偶衝突；不可把所有noncoprime都說無解。
• S08 · premise_audit · G1, S01, S06, S07 — 唯一是residue class，不是唯一整數23。
• S07 · premise_audit · G1, S01, S06 — n|mk源自n|d，n|vnk顯然；這不是無條件把lcm當product。
• S06 · premise_audit · G1, S05 — 每個等式的商不同，不可只核模3便宣告全系統。
• S05 · premise_audit · G1, S01, S04 — 正規化範圍是模product105，不是最大單模數7。
• S04 · premise_audit · G1, S02, S03 — 三項都列出，沒有少一個congruence。
• S03 · premise_audit · G1, S02 — uᵢ屬自己模數，不可交換位置。
• S02 · premise_audit · G1, S01 — 整除105由明示乘積保證，無有理近似。
• S01 · premise_audit · G1 — residues已在各自0至mᵢ−1範圍內。

錯誤控制與反例

逐式驗證

23必分別核mod3、5、7。

唯一類

product唯一性要pairwise-coprime；noncoprime另看gcd與lcm。

• 主例唯一整數解23。 → reject — 128=23+105也滿足全部方程。
• noncoprime模數必矛盾。 → reject — 9滿足1 mod4及3 mod6。
• 模數0可照主公式處理。 → reject — 要求正模數，M/mᵢ及同餘代表正規化在mᵢ=0無此意義。

結論與限制

x≡2 mod3、3 mod5、2 mod7的全部整數解為23+105t。

驗證及來源綁定

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

• source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
• adopted source SHA-256: ab307688f99c20980966f2ca78007d3dfe060ce98516b950fbbb6050f695a939
• original source SHA-256: ab307688f99c20980966f2ca78007d3dfe060ce98516b950fbbb6050f695a939
• Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

同源完整 JSON（含公式、AST、反控制與修訂記錄）