ND0252

ArithAt(F,i,z)

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.

Two genuine beta entries of the packed table represent the unique canonical signed value z. Distinct component representations need not be equal.

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. ∃ dst_positive_bottomlayer. ∃ dst_negative_bottomlayer. MatrixMinorFourCode(F,dst_positive_code_bottomlayer,dst_positive_scale_bottomlayer,dst_negative_code_bottomlayer,dst_negative_scale_bottomlayer) ∧ (BetaAt(dst_positive_code_bottomlayer,dst_positive_scale_bottomlayer,i,dst_positive_bottomlayer) ∧ (BetaAt(dst_negative_code_bottomlayer,dst_negative_scale_bottomlayer,i,dst_negative_bottomlayer) ∧ SignedBalance(z,dst_positive_bottomlayer,dst_negative_bottomlayer)))

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 dst_positive_bottomlayer dst_negative_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)))))) /\ (((((exists ff_h_pvs_bottomlayerpositive. ff_h_pvs_bottomlayerpositive + S (dst_positive_bottomlayer) = S ((S ((i))) * dst_positive_scale_bottomlayer)) /\ exists ff_q_pvs_bottomlayerpositive. dst_positive_code_bottomlayer = ff_q_pvs_bottomlayerpositive * S ((S ((i))) * dst_positive_scale_bottomlayer) + (dst_positive_bottomlayer))) /\ (((((exists ff_h_pvs_bottomlayernegative. ff_h_pvs_bottomlayernegative + S (dst_negative_bottomlayer) = S ((S ((i))) * dst_negative_scale_bottomlayer)) /\ exists ff_q_pvs_bottomlayernegative. dst_negative_code_bottomlayer = ff_q_pvs_bottomlayernegative * S ((S ((i))) * dst_negative_scale_bottomlayer) + (dst_negative_bottomlayer))) /\ (exists ge_balance_positive_bottomlayervalue ge_balance_negative_bottomlayervalue. ((((((z)) = 2 * (ge_balance_positive_bottomlayervalue) /\ (ge_balance_negative_bottomlayervalue) = 0) \/ exists ge_signed_half_bottomlayervaluedecode. ((((z)) = 2 * ge_signed_half_bottomlayervaluedecode + 1 /\ (ge_balance_positive_bottomlayervalue) = 0) /\ (ge_balance_negative_bottomlayervalue) = S ge_signed_half_bottomlayervaluedecode))) /\ ((dst_positive_bottomlayer) + ge_balance_negative_bottomlayervalue = (dst_negative_bottomlayer) + ge_balance_positive_bottomlayervalue))))))))

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)BetaAt(b,c,i,x)SignedBalance(z,p,n)

Definitions depending on this notation

ArithTableEqual(F,G,l)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

WS0002 · signed_table_lookup_anyWS0003 · signed_table_add_lookupWS0006 · signed_table_add_extensional_uniqueWS0007 · signed_table_multiply_lookupWS000A · signed_table_multiply_extensional_uniqueWS000B · signed_table_scalar_lookupWS000E · signed_table_scalar_extensional_uniqueWS000F · signed_table_add_extendWS0010 · signed_table_add_existsWS0012 · signed_table_multiply_extendWS0013 · signed_table_multiply_existsWS0015 · signed_table_scalar_extendWS0016 · signed_table_scalar_existsWS001B · signed_prefix_sum_pointwise_addWS001C · signed_prefix_sum_scalar_multiplyWS0024 · signed_table_weighted_add_distributiveWS0026 · signed_table_weighted_scalar_commute