# Constructing a three-modulus CRT class [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-chinese-remainder-theorem/) 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-chinese-remainder-theorem-01 · ocme-new142-reader-adoption-20261021 ## Goal and scope All integer solutions of x=2 mod 3, x=3 mod 5, x=2 mod 7 are 23+105t. A positive pairwise-coprime instance and noncoprime compatibility boundaries, using exact arithmetic. ## Givens and symbols - calc - G1 — Moduli 3,5,7 with respective residues 2,3,2; t is an integer. - M — product of three moduli - N_i,u_i — weights and modular inverses ## Rules and sources - calc · prerequisite — Assume exact integer arithmetic, division with remainder, and definitions of divisibility and gcd; every congruence has an explicit modulus. Explicitly assume the Bezout identity for coprime integers. - mko_definition · cited — Normalize residues, construct a simultaneous solution using modular-inverse methods and check every congruence. Uniqueness is modulo the product, not uniqueness as an integer. Modulus zero is invalid. A noncoprime system is outside the main hypothesis but may be compatible; test pairwise gcd conditions and use the lcm period in general. · mko-chinese-remainder-theorem ## Main derivation S01 · impliesBefore (m_1,m_2,m_3)=(3,5,7) After \gcd(3,5)=\gcd(3,7)=\gcd(5,7)=1,\quad M=105 Conditions: none Rule: calc · Uses: G1 Leaf basis: calc All three pairwise gcds are one and moduli positive, qualifying CRT first. S02 · impliesBefore N_i=M/m_i After (N_1,N_2,N_3)=(35,21,15) Conditions: none Rule: calc · Uses: G1, S01 Leaf basis: calc Each N_i contains the other two moduli and is zero modulo both. S03 · impliesBefore 35\equiv2\pmod3,\quad21\equiv1\pmod5,\quad15\equiv1\pmod7 After u_1=2,\quad u_2=1,\quad u_3=1 Conditions: none Rule: calc · Uses: G1, S02 Leaf basis: calc Check each modular inverse: 35*2=1 mod 3, 21=1 mod 5, 15=1 mod 7. S04 · impliesBefore x_*=\sum_{i=1}^3 a_iN_iu_i After x_*=2\cdot35\cdot2+3\cdot21+2\cdot15=233 Conditions: none Rule: calc · Uses: G1, S02, S03 Leaf basis: calc For each modulus the weighted sum leaves only its corresponding residue, constructing a simultaneous solution. S05 · impliesBefore x_*=233 After x_0=233-2\cdot105=23,\quad0\le23<105 Conditions: none Rule: calc · Uses: G1, S01, S04 Leaf basis: calc Subtract a multiple of M to normalize while preserving every congruence. S06 · impliesBefore x_0=23 After 23=7\cdot3+2=4\cdot5+3=3\cdot7+2 Conditions: none Rule: calc · Uses: G1, S05 Leaf basis: calc Independently verify all three residues directly. S07 · impliesBefore m,n\mid d,\quad\gcd(m,n)=1,\quad um+vn=1 After d=mk,\quad k=umk+vnk\Rightarrow n\mid k\Rightarrow mn\mid d Conditions: none Rule: calc · Uses: G1, S01, S06 Leaf basis: calc Bezout proves that two coprime divisors of d have product dividing d; apply successively to 3,5,7. S08 · impliesBefore x,x'\text{ solve the system} After 105\mid x-x';\quad x=23+105t,\quad t\in\mathbb Z Conditions: none Rule: mko_definition · Uses: G1, S01, S06, S07 Leaf basis: mko_definition Each modulus divides a solution difference; S07 gives uniqueness modulo 105, and adding 105t preserves all equations. S09 · impliesBefore x\equiv1\pmod4,\quad x\equiv3\pmod6 After x=9+12t\text{ solves};\quad\gcd(4,6)=2,\ 1\equiv3\pmod2 Conditions: none Rule: calc · Uses: G1, S08 Leaf basis: calc Noncoprime systems can be compatible; residues must agree modulo the gcd, and this example has lcm period 12 rather than product 24. ## Substeps and lemmas No substeps in this guide. ## Reverse audits - S09 · premise_audit · G1, S08 — The system 1 mod 4,2 mod 6 has conflicting parity, but not all noncoprime systems are inconsistent. - S08 · premise_audit · G1, S01, S06, S07 — Uniqueness is of a residue class, not of the integer 23 alone. - S07 · premise_audit · G1, S01, S06 — n divides mk since n divides d, and n divides vnk directly; this does not unconditionally identify lcm with product. - S06 · premise_audit · G1, S05 — The quotients differ; checking only modulus 3 cannot certify the system. - S05 · premise_audit · G1, S01, S04 — The normalization modulus is product 105, not the largest individual modulus 7. - S04 · premise_audit · G1, S02, S03 — All three terms are explicit; no congruence is omitted. - S03 · premise_audit · G1, S02 — Each u_i belongs to its own modulus and cannot be permuted. - S02 · premise_audit · G1, S01 — Exact divisibility follows from the stated product, with no rational approximation. - S01 · premise_audit · G1 — Each residue is normalized to its own range 0 through m_i-1. ## Error controls and negative controls Every congruenceCheck 23 separately modulo 3,5,7. Unique classProduct-modulus uniqueness needs pairwise coprimality; otherwise audit gcd and lcm separately. - The main system has unique integer solution 23. → reject — 128=23+105 satisfies every congruence too. - Noncoprime moduli are always inconsistent. → reject — 9 satisfies 1 mod 4 and 3 mod 6. - Modulus zero can use the main construction. → reject — Positive moduli are required; M/m_i and normalization do not have this meaning for m_i=0. ## Result and limitations All integer solutions of x=2 mod 3, x=3 mod 5, x=2 mod 7 are 23+105t. ## Verification and source binding 2 declared checks for this guide; only the listed expressions are covered. - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: ab307688f99c20980966f2ca78007d3dfe060ce98516b950fbbb6050f695a939 - original source SHA-256: ab307688f99c20980966f2ca78007d3dfe060ce98516b950fbbb6050f695a939 - 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-chinese-remainder-theorem-01.json)