Exact modular equations · actual arithmetic witnesses · Constructive arithmetic

Congruence Arithmetic

Exact registered congruence arithmetic contracts; see each fully quantified theorem.

Explore the exact twelve newly checked congruence arithmetic statements and their complete original proofs.

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

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 certificate

Fully expanded arithmetic

Inspect all 658 native tactic lines and 61 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem CG000C and follow only the lemmas and conservative definitions supporting fermat_little_all_inputs.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G012 milestone → theorem and definition dependencies.
Major independently established statements: CG0008 linear_congruence_exact_bounded_enumeration_exists · CG0009 linear_congruence_zero_modulus_nonzero_coefficient_unique · CG000A linear_congruence_zero_modulus_zero_coefficient_iff · CG000B linear_congruence_modulus_one_bounded_iff_zero · CG000C fermat_little_all_inputs.
Independently verified Alpha v34 checked-use theorem family: 12 dependency-curried kernel-checked theorem bodies · 61 proof prerequisites · 12 linked definitions · 9 definition-dependency arrows · 658 exact tactic lines · first admitted v34 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 215 bundle nodes; SHA-256 983051afddc637a4e033546b8f3ddb8dc0ac22aa996b4e28b3822be8895576ad.
Exact mathematical boundary: Each statement retains its explicit modulus, coprimality and divisibility assumptions. These twelve arithmetic laws do not assert all order, primitive-root, Carmichael, exponential or simultaneous-polynomial congruence goals are finished.