Exact successive-LCM compatibility · genuine noncoprime lists · G011 partial · Constructive arithmetic

Noncoprime constructive CRT compatibility and canonical solutions

MergeCompatible(aᵢ,mᵢ) ⇒ ∃!x<lcm(mᵢ). ∀i. x≡aᵢ (mod mᵢ)

Twenty-four independently checked constructive theorems solve arbitrary positive noncoprime finite systems satisfying their exact successive-LCM/gcd compatibility invariant and also establish the genuinely pairwise-compatible dominating-last case.

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 1097 native tactic lines and 90 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem GC000C and follow only the lemmas and conservative definitions supporting crt_merge_compatible_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: GC0005 crt_prefix_solution_implies_pairwise_compatible · GC0009 crt_merge_compatible_prefix_solution_exists · GC000B crt_prefix_zero_lcm_solution_unique · GC000E crt_is_gcd_scale · GC0012 crt_lcm_gcd_cofactor_product · GC0015 crt_gcd_lcm_distributes_divisibility · GC0018 crt_pairwise_compatible_dominating_last_canonical_exists_unique · GC000C crt_merge_compatible_prefix_canonical_exists_unique.
Independently verified Alpha v34 checked-use theorem family: 24 dependency-curried kernel-checked theorem bodies · 90 proof prerequisites · 14 linked definitions · 26 definition-dependency arrows · 1097 exact tactic lines · first admitted v25 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 302 bundle nodes; SHA-256 d4532076049be869e4e397d0fcee81b668bd3fd5c7d9173028bb1bdb80b9793a.
Exact mathematical boundary: Historical partial components only: this chapter proves canonical solutions under successive-merge compatibility and in the pairwise-compatible dominating-last case. G011 is now closed in the separate Alpha-v27 generalized-crt branch for arbitrary pairwise-compatible finite lists, including noncoprime moduli.

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