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

FpNeg(p,a,b)FpFieldLaws(p)FpAddGridValue(p,i,v)FpUnitSteps(p,b,c,n)

Checked theorems using this definition

FP0008 · prime_field_add_existsFP0009 · prime_field_add_functionalFP000A · prime_field_add_exists_uniqueFP000B · prime_field_add_commutativeFP0010 · prime_field_add_associativeFP0012 · prime_field_left_distributiveFP0013 · prime_field_right_distributiveFP0014 · prime_field_add_zero_rightFP0015 · prime_field_add_zero_leftFP001A · prime_field_add_cancel_leftFP001B · prime_field_negate_existsFP001C · prime_field_negate_functionalFP001D · prime_field_negate_exists_uniqueFP0027 · prime_field_residue_addFP002B · prime_field_add_grid_value_existsFP0031 · prime_field_negate_prefix_choiceFP0038 · prime_field_add_grid_value_lookupFP0039 · prime_field_add_table_lookupFP003A · prime_field_add_table_reflectFP003E · prime_field_negate_table_lookupFP003F · prime_field_negate_table_reflectFP0043 · prime_field_add_table_associativeFP0048 · prime_field_left_table_distributiveFP0049 · prime_field_right_table_distributiveFP004D · prime_field_unit_trace_recodeFP004E · prime_field_unit_trace_successorFP004F · prime_field_unit_trace_residueFP0051 · prime_field_unit_trace_exists