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

FpCoefficientReduction(p,b,c,d,e,l)FpAdd(p,a,b,c)FpMul(p,a,b,c)

Checked theorems using this definition

PP0003 · prime_field_polynomial_normalization_entryPP0004 · prime_field_polynomial_normalization_boundedPP0007 · prime_field_polynomial_normalization_transportPP000C · prime_field_polynomial_add_from_normalizationPP0014 · prime_field_polynomial_scale_from_normalizationPP0020 · prime_field_polynomial_horner_canonical_stepPP0021 · prime_field_polynomial_horner_trace_from_normalizationPP0022 · prime_field_polynomial_horner_existsPP0027 · prime_field_polynomial_horner_normalization_residuePP0028 · prime_field_polynomial_horner_residuePP002F · prime_field_polynomial_normalized_horner_iffPP0030 · prime_field_polynomial_horner_result_boundedPP0031 · prime_field_polynomial_reduce_and_evaluate_exists