Arbitrary finite pairwise-coprime lists · exact LCM · G011 partial · Constructive arithmetic

Finite Chinese remainder theorem and canonical LCM solutions

∀ finite coprime positive lists. ∃!x<lcm(mᵢ). ∀i. x≡aᵢ (mod mᵢ)

Twenty-seven independently checked constructive theorems compute the universal-property LCM of arbitrary finite modulus lists and prove existence and canonical uniqueness for every positive pairwise-coprime finite congruence system.

Open the definition-aware map Read the final theorem See campaign milestone G011

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact certificate

Fully expanded arithmetic

Inspect all 1106 native tactic lines and 83 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem CR001B and follow only the lemmas and conservative definitions supporting crt_pairwise_coprime_prefix_canonical_exists_unique.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G011 milestone → theorem and definition dependencies.
Major independently established statements: CR0010 crt_prefix_lcm_exists_unique · CR0013 crt_pairwise_coprime_prefix_solution_exists · CR0018 crt_prefix_solution_class_iff_lcm · CR001B crt_pairwise_coprime_prefix_canonical_exists_unique.
Independently verified Alpha v34 checked-use theorem family: 27 dependency-curried kernel-checked theorem bodies · 83 proof prerequisites · 12 linked definitions · 16 definition-dependency arrows · 1106 exact tactic lines · first admitted v24 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 203 bundle nodes; SHA-256 627e39ed29b10db48bf37d5bef8750d48009a7524c822a7c5e7c83e96a8e9cf9.
Exact mathematical boundary: Historical partial components only: this chapter proves canonical solutions for finite positive pairwise-coprime systems and exact LCM solution classes. G011 is now closed in the separate Alpha-v27 generalized-crt branch for arbitrary pairwise-compatible systems, including noncoprime moduli.

Separate complete second-wave branches: Full G011 proof · Alpha v27.