Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Definition in prerequisite notation
S x ≤ S (S i · c) ∧ (∃ y. b = y · S (S i · c) + x)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((exists ff_h_defined_beta_at. ff_h_defined_beta_at + S (x) = S ((S (i)) * c)) /\ exists ff_q_defined_beta_at. b = ff_q_defined_beta_at * S ((S (i)) * c) + (x))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
none — first-order arithmetic only
Definitions depending on this notation
ModularSetMember(b,c,p,x)ModularSetSubset(b,c,d,e,p)ModularSetUnion(b,c,d,e,u,v,p)ModularSetIntersection(b,c,d,e,u,v,p)ModularSetPullback(b,c,d,e,p,t)ModularSetSumCover(b,c,d,e,u,v,p)ModularSetSum(b,c,d,e,u,v,p)ModularTranslationBoundary(b,c,p,d,a,r)ModularDysonTransform(b,c,d,e,ub,uc,vb,vc,p,t)Sum(b,c,l,z)AllBits(b,c,l)
Checked theorems using this definition
CD0001 · finite_bit_entry_casesCD0002 · finite_bit_membership_decidableCD0003 · finite_bit_count_positive_memberCD0004 · finite_bit_subset_pointwise_leCD0009 · finite_sum_entry_leCD000B · finite_sum_pointwise_strict_atCD000C · finite_bit_count_proper_subset_ltCD000D · finite_bit_count_missing_zeroCD000E · finite_bit_count_two_nonzero_memberCD000F · finite_sum_pointwise_balanceCD0011 · finite_bit_intersection_from_productCD0012 · finite_bit_intersection_existsCD0013 · finite_bit_complement_existsCD0014 · finite_bit_complement_member_iffCD0015 · finite_bit_union_of_complementsCD0016 · finite_bit_union_existsCD0018 · finite_beta_value_one_iffCD0019 · finite_bit_nonmember_zeroCD001B · finite_bit_union_intersection_count_balanceCD001C · finite_beta_composition_existsCD001D · finite_modular_translation_indices_existsCD001E · finite_modular_translation_index_entryCD001F · finite_modular_translation_indices_permutationCD0020 · finite_modular_composition_all_bitsCD0021 · finite_modular_composition_pullbackCD0022 · finite_modular_set_pullback_existsCD0023 · finite_bit_zero_nonmemberCD0027 · finite_modular_pullback_membership_witnessCD0028 · finite_modular_pushforward_membership_witnessCD002A · finite_beta_zero_codeCD002C · finite_partial_sumset_emptyCD002D · finite_partial_sumset_succ_absentCD002E · finite_partial_sumset_succ_presentCD002F · finite_modular_sumset_prefix_existsCD0030 · finite_modular_sumset_existsCD0031 · finite_modular_sumset_coverCD0034 · finite_modular_orbit_member_or_boundaryCD0035 · prime_modular_set_translation_boundary_existsCD0036 · finite_modular_dyson_upper_from_unionCD0037 · finite_modular_dyson_lower_from_pullbackCD0039 · finite_modular_dyson_upper_memberCD003A · finite_modular_dyson_lower_subsetCD003B · finite_modular_dyson_lower_zero_memberCD003C · finite_modular_dyson_lower_boundary_nonmemberCD003D · finite_modular_dyson_sum_coverCD003E · finite_modular_dyson_strict_sizesCD0041 · prime_modular_normalized_boundary_existsCD0044 · finite_modular_pullback_zero_memberCD0045 · finite_modular_opposite_translates_sum_cover