ND0094

PrimeBitPrefix(b,c,l)

At each index i<l the actual bit is one exactly when S i is prime, and otherwise zero.

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

∀ pc_index_secondwave. Lt(pc_index_secondwave,l) → ∃ x. BetaAt(b,c,pc_index_secondwave,x) ∧ (Prime(S pc_index_secondwave) ∧ x = 1 ∨ ¬Prime(S pc_index_secondwave) ∧ x = 0)

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

Hygienic expanded first-order definition 
forall pc_index_secondwave. (exists pc_lt_secondwave_bound. pc_lt_secondwave_bound + S (pc_index_secondwave) = (l)) -> exists pc_bit_secondwave. (((exists fs_h_pc_secondwave_entry. fs_h_pc_secondwave_entry + S (pc_bit_secondwave) = S ((S (pc_index_secondwave)) * c)) /\ exists fs_q_pc_secondwave_entry. b = fs_q_pc_secondwave_entry * S ((S (pc_index_secondwave)) * c) + (pc_bit_secondwave))) /\ (((((~(S (pc_index_secondwave) = 1) /\ forall bpr_left_pc_secondwave_choice_prime bpr_right_pc_secondwave_choice_prime. S (pc_index_secondwave) = bpr_left_pc_secondwave_choice_prime * bpr_right_pc_secondwave_choice_prime -> bpr_left_pc_secondwave_choice_prime = 1 \/ bpr_right_pc_secondwave_choice_prime = 1)) /\ pc_bit_secondwave = 1) \/ (~((~(S (pc_index_secondwave) = 1) /\ forall bpr_left_pc_secondwave_choice_prime bpr_right_pc_secondwave_choice_prime. S (pc_index_secondwave) = bpr_left_pc_secondwave_choice_prime * bpr_right_pc_secondwave_choice_prime -> bpr_left_pc_secondwave_choice_prime = 1 \/ bpr_right_pc_secondwave_choice_prime = 1)) /\ pc_bit_secondwave = 0)))

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

Direct definition dependencies

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

Definitions depending on this notation

PrimeCount(x,z)

Checked theorems using this definition

PC0002 · prime_bit_prefix_emptyPC0003 · prime_bit_prefix_drop_lastPC0004 · prime_bit_prefix_entryPC0005 · prime_bit_prefix_extendPC0006 · prime_bit_prefix_existsPC0007 · prime_bit_prefix_all_bitsPC0008 · prime_count_existsPC001D · central_binom_prime_mask_weighted_upperPC001E · primorial_cutoff_weighted_lowerPC0020 · primorial_cutoff_count_power_boundPC0028 · prime_cutoff_exponent_boundPC0033 · prime_bit_prefix_equal_entry