PD0008

ModEq(m,a,b)

Balanced-natural congruence modulo m.

Conservative notation; not a theorem, primitive, or axiom.

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.

Definition in prerequisite notation

∃ u. ∃ v. a + m · u = b + m · v

Only definitions earlier in this acyclic notation graph are used here.

Hygienic expanded first-order definition 
exists u v. a + m * u = b + m * v

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

none — first-order arithmetic only

Definitions depending on this notation

ModularSetPullback(b,c,d,e,p,t)ModularSetSumCover(b,c,d,e,u,v,p)ModularSetSum(b,c,d,e,u,v,p)ModularTranslationBoundary(b,c,p,d,a,r)ModularDysonTransform(b,c,d,e,ub,uc,vb,vc,p,t)

Checked theorems using this definition

CD001D · finite_modular_translation_indices_existsCD001E · finite_modular_translation_index_entryCD001F · finite_modular_translation_indices_permutationCD0020 · finite_modular_composition_all_bitsCD0021 · finite_modular_composition_pullbackCD0022 · finite_modular_set_pullback_existsCD0024 · finite_modular_residue_existsCD0026 · finite_modular_inverse_shiftCD0027 · finite_modular_pullback_membership_witnessCD0028 · finite_modular_pushforward_membership_witnessCD0029 · finite_modular_shifted_sum_congruenceCD002C · finite_partial_sumset_emptyCD002D · finite_partial_sumset_succ_absentCD002E · finite_partial_sumset_succ_presentCD002F · finite_modular_sumset_prefix_existsCD0030 · finite_modular_sumset_existsCD0031 · finite_modular_sumset_coverCD0032 · finite_modular_add_modulusCD0033 · prime_modular_additive_orbit_hitsCD0034 · finite_modular_orbit_member_or_boundaryCD0035 · prime_modular_set_translation_boundary_existsCD0036 · finite_modular_dyson_upper_from_unionCD0037 · finite_modular_dyson_lower_from_pullbackCD0039 · finite_modular_dyson_upper_memberCD003A · finite_modular_dyson_lower_subsetCD003B · finite_modular_dyson_lower_zero_memberCD003C · finite_modular_dyson_lower_boundary_nonmemberCD003D · finite_modular_dyson_sum_coverCD0045 · finite_modular_opposite_translates_sum_cover