ND0230

FpMul(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 product; no multiplication law is assumed.

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

FpInv(p,a,b)FpFieldLaws(p)FpMulGridValue(p,i,v)

Checked theorems using this definition

FP000C · prime_field_multiply_existsFP000D · prime_field_multiply_functionalFP000E · prime_field_multiply_exists_uniqueFP000F · prime_field_multiply_commutativeFP0011 · prime_field_multiply_associativeFP0012 · prime_field_left_distributiveFP0013 · prime_field_right_distributiveFP0016 · prime_field_multiply_one_rightFP0017 · prime_field_multiply_one_leftFP0018 · prime_field_multiply_zero_rightFP0019 · prime_field_multiply_zero_leftFP0021 · prime_field_zero_has_no_multiplicative_inverseFP0022 · prime_field_inverse_output_nonzeroFP0025 · prime_field_multiply_cancel_nonzero_leftFP0026 · prime_field_no_zero_divisorsFP0028 · prime_field_residue_multiplyFP002C · prime_field_multiply_grid_value_existsFP003B · prime_field_multiply_grid_value_lookupFP003C · prime_field_multiply_table_lookupFP003D · prime_field_multiply_table_reflectFP0045 · prime_field_multiply_table_associativeFP0047 · prime_field_inverse_table_nonzeroFP0048 · prime_field_left_table_distributiveFP0049 · prime_field_right_table_distributive