ND0251

ArithTable(N,F)

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.

An actual packed signed table with canonical signed entries through index N, including index zero. It contains no divisor transform or inversion hypothesis.

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

Definition in prerequisite notation

∃ dst_positive_code_bottomlayer. ∃ dst_positive_scale_bottomlayer. ∃ dst_negative_code_bottomlayer. ∃ dst_negative_scale_bottomlayer. MatrixMinorFourCode(F,dst_positive_code_bottomlayer,dst_positive_scale_bottomlayer,dst_negative_code_bottomlayer,dst_negative_scale_bottomlayer) ∧ (∀ x. Le(x,N) → ∃ y. ∃ z. ∃ n. BetaAt(dst_positive_code_bottomlayer,dst_positive_scale_bottomlayer,x,y) ∧ (BetaAt(dst_negative_code_bottomlayer,dst_negative_scale_bottomlayer,x,z) ∧ SignedBalance(n,y,z)))

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

Hygienic expanded first-order definition 
exists dst_positive_code_bottomlayer dst_positive_scale_bottomlayer dst_negative_code_bottomlayer dst_negative_scale_bottomlayer. ((((F)) = (((((dst_positive_code_bottomlayer) + (dst_positive_scale_bottomlayer)) * S ((dst_positive_code_bottomlayer) + (dst_positive_scale_bottomlayer)) + ((dst_positive_scale_bottomlayer) + (dst_positive_scale_bottomlayer))) + (((dst_negative_code_bottomlayer) + (dst_negative_scale_bottomlayer)) * S ((dst_negative_code_bottomlayer) + (dst_negative_scale_bottomlayer)) + ((dst_negative_scale_bottomlayer) + (dst_negative_scale_bottomlayer)))) * S ((((dst_positive_code_bottomlayer) + (dst_positive_scale_bottomlayer)) * S ((dst_positive_code_bottomlayer) + (dst_positive_scale_bottomlayer)) + ((dst_positive_scale_bottomlayer) + (dst_positive_scale_bottomlayer))) + (((dst_negative_code_bottomlayer) + (dst_negative_scale_bottomlayer)) * S ((dst_negative_code_bottomlayer) + (dst_negative_scale_bottomlayer)) + ((dst_negative_scale_bottomlayer) + (dst_negative_scale_bottomlayer)))) + ((((dst_negative_code_bottomlayer) + (dst_negative_scale_bottomlayer)) * S ((dst_negative_code_bottomlayer) + (dst_negative_scale_bottomlayer)) + ((dst_negative_scale_bottomlayer) + (dst_negative_scale_bottomlayer))) + (((dst_negative_code_bottomlayer) + (dst_negative_scale_bottomlayer)) * S ((dst_negative_code_bottomlayer) + (dst_negative_scale_bottomlayer)) + ((dst_negative_scale_bottomlayer) + (dst_negative_scale_bottomlayer)))))) /\ (forall dst_index_bottomlayer. (exists pvs_le_gap_bottomlayerdomain. pvs_le_gap_bottomlayerdomain + (dst_index_bottomlayer) = ((N))) -> exists dst_positive_bottomlayer dst_negative_bottomlayer dst_value_bottomlayer. ((((exists ff_h_pvs_bottomlayerentrypositive. ff_h_pvs_bottomlayerentrypositive + S (dst_positive_bottomlayer) = S ((S (dst_index_bottomlayer)) * dst_positive_scale_bottomlayer)) /\ exists ff_q_pvs_bottomlayerentrypositive. dst_positive_code_bottomlayer = ff_q_pvs_bottomlayerentrypositive * S ((S (dst_index_bottomlayer)) * dst_positive_scale_bottomlayer) + (dst_positive_bottomlayer))) /\ (((((exists ff_h_pvs_bottomlayerentrynegative. ff_h_pvs_bottomlayerentrynegative + S (dst_negative_bottomlayer) = S ((S (dst_index_bottomlayer)) * dst_negative_scale_bottomlayer)) /\ exists ff_q_pvs_bottomlayerentrynegative. dst_negative_code_bottomlayer = ff_q_pvs_bottomlayerentrynegative * S ((S (dst_index_bottomlayer)) * dst_negative_scale_bottomlayer) + (dst_negative_bottomlayer))) /\ (exists ge_balance_positive_bottomlayerentryvalue ge_balance_negative_bottomlayerentryvalue. (((((dst_value_bottomlayer) = 2 * (ge_balance_positive_bottomlayerentryvalue) /\ (ge_balance_negative_bottomlayerentryvalue) = 0) \/ exists ge_signed_half_bottomlayerentryvaluedecode. (((dst_value_bottomlayer) = 2 * ge_signed_half_bottomlayerentryvaluedecode + 1 /\ (ge_balance_positive_bottomlayerentryvalue) = 0) /\ (ge_balance_negative_bottomlayerentryvalue) = S ge_signed_half_bottomlayerentryvaluedecode))) /\ ((dst_positive_bottomlayer) + ge_balance_negative_bottomlayerentryvalue = (dst_negative_bottomlayer) + ge_balance_positive_bottomlayerentryvalue))))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

MatrixMinorFourCode(z,up,us,un,ut)Le(a,b)BetaAt(b,c,i,x)SignedBalance(z,p,n)

Definitions depending on this notation

ArithExtend(F,G,l,z)ArithAdd(F,G,H,l)ArithMul(F,G,H,l)ArithScale(a,F,G,l)

Checked theorems using this definition

WS0001 · signed_table_domain_resizeWS0002 · signed_table_lookup_anyWS0005 · signed_table_add_emptyWS0006 · signed_table_add_extensional_uniqueWS0009 · signed_table_multiply_emptyWS000A · signed_table_multiply_extensional_uniqueWS000D · signed_table_scalar_emptyWS000E · signed_table_scalar_extensional_uniqueWS000F · signed_table_add_extendWS0010 · signed_table_add_existsWS0011 · signed_table_add_exists_extensionally_uniqueWS0012 · signed_table_multiply_extendWS0013 · signed_table_multiply_existsWS0014 · signed_table_multiply_exists_extensionally_uniqueWS0015 · signed_table_scalar_extendWS0016 · signed_table_scalar_existsWS0017 · signed_table_scalar_exists_extensionally_uniqueWS001F · signed_weighted_sum_existsWS0021 · signed_weighted_sum_exists_uniqueWS0023 · signed_weighted_sum_empty_exists