ND0023

CanonicalModularResidue(m,a,r)

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

A strictly bounded canonical natural residue r<m together with exact balanced congruence to a modulo m.

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

Definition in prerequisite notation

Lt(r,m) ∧ ModEq(m,a,r)

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

Hygienic expanded first-order definition 
((exists ff_gap_binary_advanced. ff_gap_binary_advanced + S (r) = m) /\ (exists ff_left_binary_advanced_congruence ff_right_binary_advanced_congruence. (a) + m * ff_left_binary_advanced_congruence = (r) + m * ff_right_binary_advanced_congruence))

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

Direct definition dependencies

Lt(a,b)ModEq(m,a,b)

Definitions depending on this notation

FpAdd(p,a,b,c)FpMul(p,a,b,c)

Checked theorems using this definition

FP0003 · prime_field_residue_reflexiveFP0004 · prime_field_residue_input_equalFP0005 · prime_field_residue_congruence_transportFP0006 · prime_field_residue_bounded_valueFP0007 · prime_field_residue_modulus_zeroFP0008 · prime_field_add_existsFP000C · prime_field_multiply_existsFP0010 · prime_field_add_associativeFP0011 · prime_field_multiply_associativeFP0012 · prime_field_left_distributiveFP0013 · prime_field_right_distributiveFP0027 · prime_field_residue_addFP0028 · prime_field_residue_multiplyFP0029 · prime_field_positive_below_modulus_not_zeroFP004F · prime_field_unit_trace_residueFP0050 · prime_field_unit_trace_result_boundedFP0052 · prime_field_unit_multiple_residueFP0053 · prime_field_unit_multiple_from_residue