ND0246

FpAddPrefix(p,b,c,l)

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.

Every genuine beta entry below l gives the addition grid value at its actual index.

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

Definition in prerequisite notation

∀ pft_index_bottomlayer. Lt(pft_index_bottomlayer,l) → ∃ x. BetaAt(b,c,pft_index_bottomlayer,x) ∧ FpAddGridValue(p,pft_index_bottomlayer,x)

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

Hygienic expanded first-order definition 
forall pft_index_bottomlayer. (exists pfa_gap_bottomlayerprefix. pfa_gap_bottomlayerprefix + S (pft_index_bottomlayer) = ((l))) -> exists pft_value_bottomlayer. (((((exists ff_h_pft_bottomlayerpointentry. ff_h_pft_bottomlayerpointentry + S (pft_value_bottomlayer) = S ((S (pft_index_bottomlayer)) * (c))) /\ exists ff_q_pft_bottomlayerpointentry. (b) = ff_q_pft_bottomlayerpointentry * S ((S (pft_index_bottomlayer)) * (c)) + (pft_value_bottomlayer))) /\ ((exists pft_row_bottomlayerpointvalue pft_column_bottomlayerpointvalue. (((pft_index_bottomlayer) = pft_row_bottomlayerpointvalue * ((p)) + pft_column_bottomlayerpointvalue) /\ ((((exists pfa_gap_bottomlayerpointvalueoperationleft. pfa_gap_bottomlayerpointvalueoperationleft + S (pft_row_bottomlayerpointvalue) = ((p))) /\ (((exists pfa_gap_bottomlayerpointvalueoperationright. pfa_gap_bottomlayerpointvalueoperationright + S (pft_column_bottomlayerpointvalue) = ((p))) /\ ((((exists pfa_gap_bottomlayerpointvalueoperationresultbound. pfa_gap_bottomlayerpointvalueoperationresultbound + S (pft_value_bottomlayer) = ((p))) /\ ((exists pfa_offset_left_bottomlayerpointvalueoperationresultcongruence pfa_offset_right_bottomlayerpointvalueoperationresultcongruence. ((pft_row_bottomlayerpointvalue) + (pft_column_bottomlayerpointvalue)) + ((p)) * pfa_offset_left_bottomlayerpointvalueoperationresultcongruence = (pft_value_bottomlayer) + ((p)) * pfa_offset_right_bottomlayerpointvalueoperationresultcongruence)))))))))))))))

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)BetaAt(b,c,i,x)FpAddGridValue(p,i,v)

Definitions depending on this notation

FpOperationTables(p,ab,ac,mb,mc,nb,nc,ib,ic)

Checked theorems using this definition

FP002F · prime_field_add_prefix_choiceFP0033 · prime_field_add_table_existsFP0037 · prime_field_operation_tables_existsFP0039 · prime_field_add_table_lookupFP003A · prime_field_add_table_reflectFP0042 · prime_field_add_table_commutativeFP0043 · prime_field_add_table_associativeFP0048 · prime_field_left_table_distributiveFP0049 · prime_field_right_table_distributive