ND0128

ModularSetMember(b,c,p,x)

The actual characteristic bit at the canonical residue x<p is one. Complete finite sets and their cardinalities reuse the existing BitCount identity.

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

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

Lt(x,p) ∧ BetaAt(b,c,x,1)

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

Hygienic expanded first-order definition 
((exists fms_gap_secondwave. fms_gap_secondwave + S (x) = (p)) /\ (((exists fs_h_fms_secondwave. fs_h_fms_secondwave + S (1) = S ((S (x)) * c)) /\ exists fs_q_fms_secondwave. b = fs_q_fms_secondwave * S ((S (x)) * c) + (1))))

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

Direct definition dependencies

Lt(a,b)BetaAt(b,c,i,x)

Definitions depending on this notation

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)

Checked theorems using this definition

CD0003 · finite_bit_count_positive_memberCD000A · finite_bit_member_count_nonzeroCD000E · finite_bit_count_two_nonzero_memberCD0027 · finite_modular_pullback_membership_witnessCD0028 · finite_modular_pushforward_membership_witnessCD002C · 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_sizesCD003F · finite_modular_zero_sum_left_subsetCD0040 · finite_modular_singleton_cover_boundCD0041 · prime_modular_normalized_boundary_existsCD0042 · prime_cauchy_davenport_normalized_bounded_inductionCD0043 · prime_cauchy_davenport_normalized_cover_boundCD0044 · finite_modular_pullback_zero_memberCD0045 · finite_modular_opposite_translates_sum_coverCD0046 · prime_cauchy_davenport_cover_bound