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. ∃ 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
Definitions depending on this notation
ArithTableEqual(F,G,l)ArithPositiveEqual(F,G,N)ArithScale(a,F,G,l)ArithSlice(F,G,o,s,l)ArithRowSums(F,R,o,s,t,m,n)SignedZeroWindow(F,k,l)DirichletEntry(F,G,n,d,z)DirichletPrefix(F,G,n,l,M)DirichletTable(N,F,G,H)KroneckerDeltaTable(N,E)DirichletUnitAtOne(F)MultiplicativePrefix(N,F)SignedCartesianProduct(F,G,T,m,n)SignedSupportReindex(A,B,r,s,L,M)SignedIncidenceEntry(A,r,s,i,j,z)SignedIncidenceFlatPrefix(A,r,s,M,l,T)SignedSupportIncidence(A,r,s,L,M,T)
Checked theorems using this definition
MX0003 · signed_multiplicative_normalizedMX0004 · signed_multiplicative_coprime_productMX0005 · signed_multiplicative_introMX0007 · signed_multiplicative_at_one_valueMX0009 · signed_multiplicative_product_values_existMX000A · signed_positive_table_entry_transportMX000B · signed_multiplicative_positive_extensionalMX0018 · signed_slice_identityMX001A · signed_slice_sum_concatenateMX001C · signed_row_sums_flattenMX001F · signed_cartesian_flat_entry_existsMX0020 · signed_cartesian_flat_entry_lookupMX0021 · signed_cartesian_flat_prefix_zeroMX0022 · signed_cartesian_flat_prefix_appendMX0023 · signed_cartesian_flat_prefix_existsMX0024 · signed_cartesian_product_from_flat_prefixMX0026 · signed_cartesian_product_existsMX0027 · signed_cartesian_product_row_scalarMX0028 · signed_cartesian_product_row_sumMX0029 · signed_cartesian_product_row_sums_scalarMX002F · signed_cartesian_product_flat_lookupMX0030 · signed_cartesian_product_extensional_uniqueMX0031 · signed_cartesian_product_reencodeMX0033 · signed_prefix_sum_single_spike_valueMX0034 · signed_prefix_sum_single_spike_existsMX0035 · signed_prefix_sum_point_spike_valueMX0036 · signed_support_incidence_entry_hitMX0037 · signed_support_incidence_entry_missMX0038 · signed_support_incidence_entry_decodeMX003A · signed_support_incidence_entry_existsMX003B · signed_support_incidence_zero_source_valueMX003C · signed_support_incidence_nonzero_source_imageMX003F · signed_support_incidence_flat_prefix_zeroMX0040 · signed_support_incidence_flat_prefix_appendMX0041 · signed_support_incidence_flat_prefix_existsMX0044 · signed_support_incidence_row_lookupMX0045 · signed_support_incidence_column_lookupMX0046 · signed_support_incidence_row_sum_valueMX0047 · signed_support_incidence_column_sum_valueMX004F · dirichlet_multiplicative_pair_factorizationMX0051 · dirichlet_coprime_grid_nonzero_coordinatesMX0052 · dirichlet_coprime_grid_support_preservingMX0053 · dirichlet_coprime_grid_support_injectiveMX0054 · dirichlet_coprime_grid_support_coveringMX0058 · dirichlet_convolution_multiplicative_tableMX005A · dirichlet_multiplicative_function_invertible