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
∃ 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
Definitions depending on this notation
ArithScale(a,F,G,l)ArithSlice(F,G,o,s,l)ArithRowSums(F,R,o,s,t,m,n)DirichletPrefix(F,G,n,l,M)DirichletTable(N,F,G,H)KroneckerDeltaTable(N,E)MultiplicativePrefix(N,F)SignedCartesianProduct(F,G,T,m,n)SignedSupportReindex(A,B,r,s,L,M)SignedIncidenceFlatPrefix(A,r,s,M,l,T)SignedSupportIncidence(A,r,s,L,M,T)
Checked theorems using this definition
MX0002 · signed_multiplicative_tableMX0005 · signed_multiplicative_introMX000A · signed_positive_table_entry_transportMX000B · signed_multiplicative_positive_extensionalMX0018 · signed_slice_identityMX0019 · signed_slice_sum_unit_prefix_iffMX001D · signed_prefix_sum_row_major_iffMX001E · signed_prefix_sum_row_major_existsMX001F · signed_cartesian_flat_entry_existsMX0021 · signed_cartesian_flat_prefix_zeroMX0022 · signed_cartesian_flat_prefix_appendMX0023 · signed_cartesian_flat_prefix_existsMX0024 · signed_cartesian_product_from_flat_prefixMX0025 · signed_cartesian_product_empty_columnsMX0026 · signed_cartesian_product_existsMX002C · signed_cartesian_product_sums_existsMX0031 · signed_cartesian_product_reencodeMX0032 · signed_cartesian_product_exists_extensionally_uniqueMX0033 · signed_prefix_sum_single_spike_valueMX0034 · signed_prefix_sum_single_spike_existsMX0035 · signed_prefix_sum_point_spike_valueMX003A · signed_support_incidence_entry_existsMX003D · signed_support_incidence_flat_entry_existsMX003F · signed_support_incidence_flat_prefix_zeroMX0040 · signed_support_incidence_flat_prefix_appendMX0041 · signed_support_incidence_flat_prefix_existsMX0042 · signed_support_incidence_from_flat_prefixMX0043 · signed_support_incidence_exists