Pairwise gcd compatibility · arbitrary noncoprime lists · zero moduli · Constructive arithmetic

Complete finite generalized Chinese remainder theorem

PairwiseCompatible(aᵢ,mᵢ) ⇔ ∃x.∀i.x≡aᵢ (mod mᵢ)

Construct a simultaneous solution for every finite pairwise-compatible list, prove the exact LCM solution class, and obtain unique normalized representatives without a supplied compatible prefix or dominating last modulus.

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

Open the exact edition →

Focused route

Final dependency cone

Start at theorem FC0013 and follow only the lemmas and conservative definitions supporting crt_pairwise_compatible_prefix_normalized_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: FC0014 crt_pairwise_compatible_prefix_solvable_iff · FC000F crt_pairwise_compatible_prefix_canonical_exists_unique · FC0013 crt_pairwise_compatible_prefix_normalized_exists_unique.
Independently verified Alpha v34 checked-use theorem family: 24 dependency-curried kernel-checked theorem bodies · 72 proof prerequisites · 13 linked definitions · 20 definition-dependency arrows · 1099 exact tactic lines · first admitted v27 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 1224 bundle nodes; SHA-256 c4711433c92b67d2ebeb30131669c60563c70e0464dafa851d417fb88fb21a6d.
Exact mathematical boundary: All finite lists are included, even the empty list and zero moduli. A positive LCM gives x<M; at zero LCM congruence is exact equality and normalization deliberately does not require the impossible x<0.