ND0229

FpAdd(p,a,b,c)

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.

Bounded operands and the actual canonical residue of their natural sum. The old ND0023 residue graph is reused exactly.

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

Definition in prerequisite notation

Lt(a,p) ∧ (Lt(b,p) ∧ CanonicalModularResidue(p,a + b,c))

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

Hygienic expanded first-order definition 
((exists pfa_gap_bottomlayerleft. pfa_gap_bottomlayerleft + S ((a)) = ((p))) /\ (((exists pfa_gap_bottomlayerright. pfa_gap_bottomlayerright + S ((b)) = ((p))) /\ ((((exists pfa_gap_bottomlayerresultbound. pfa_gap_bottomlayerresultbound + S ((c)) = ((p))) /\ ((exists pfa_offset_left_bottomlayerresultcongruence pfa_offset_right_bottomlayerresultcongruence. (((a)) + ((b))) + ((p)) * pfa_offset_left_bottomlayerresultcongruence = ((c)) + ((p)) * pfa_offset_right_bottomlayerresultcongruence))))))))

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)CanonicalModularResidue(m,a,r)

Definitions depending on this notation

FpPolyAdd(p,ab,ac,bb,bc,cb,cc,l)FpHornerStep(p,b,c,x,u,v,i)

Checked theorems using this definition

PP000E · prime_field_polynomial_add_entryPP000F · prime_field_polynomial_add_boundedPP0011 · prime_field_polynomial_add_transportPP0012 · prime_field_polynomial_add_commutativePP001F · prime_field_polynomial_scalar_add_distributesPP0020 · prime_field_polynomial_horner_canonical_stepPP0021 · prime_field_polynomial_horner_trace_from_normalizationPP0025 · prime_field_polynomial_horner_successor_decomposePP0027 · prime_field_polynomial_horner_normalization_residuePP002C · prime_field_polynomial_horner_successor_construct