ND0229

FpAdd(p,a,b,c)

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.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

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)FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,L)FpPolynomialQuotientStep(p,k,ab,ac,bb,bc,M,qb,qc,i,q)

Checked theorems using this definition

PX0008 · prime_field_convolution_coefficient_appendPX001E · prime_field_polynomial_add_left_pad_transportPX001F · prime_field_polynomial_subtract_left_pad_transportPX0023 · prime_field_polynomial_constant_right_coefficientPX0027 · prime_field_polynomial_quotient_scalar_cancellationPX002E · prime_field_polynomial_quotient_prefix_existsPX002F · prime_field_polynomial_quotient_prefix_convolution_entryPX0041 · polynomial_zero_extended_add_congruentPX0046 · prime_field_convolution_coefficient_left_addPX0047 · prime_field_convolution_coefficient_right_add