PC0033 — prime_bit_prefix_equal_entry

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.

Exact expanded first-order arithmetic statement

forall b c d f l i e a. (forall pc_index_mask_equal_left. (exists pc_lt_mask_equal_left_bound. pc_lt_mask_equal_left_bound + S (pc_index_mask_equal_left) = (l)) -> exists pc_bit_mask_equal_left. (((exists fs_h_pc_mask_equal_left_entry. fs_h_pc_mask_equal_left_entry + S (pc_bit_mask_equal_left) = S ((S (pc_index_mask_equal_left)) * c)) /\ exists fs_q_pc_mask_equal_left_entry. b = fs_q_pc_mask_equal_left_entry * S ((S (pc_index_mask_equal_left)) * c) + (pc_bit_mask_equal_left))) /\ (((((~(S (pc_index_mask_equal_left) = 1) /\ forall bpr_left_pc_mask_equal_left_choice_prime bpr_right_pc_mask_equal_left_choice_prime. S (pc_index_mask_equal_left) = bpr_left_pc_mask_equal_left_choice_prime * bpr_right_pc_mask_equal_left_choice_prime -> bpr_left_pc_mask_equal_left_choice_prime = 1 \/ bpr_right_pc_mask_equal_left_choice_prime = 1)) /\ pc_bit_mask_equal_left = 1) \/ (~((~(S (pc_index_mask_equal_left) = 1) /\ forall bpr_left_pc_mask_equal_left_choice_prime bpr_right_pc_mask_equal_left_choice_prime. S (pc_index_mask_equal_left) = bpr_left_pc_mask_equal_left_choice_prime * bpr_right_pc_mask_equal_left_choice_prime -> bpr_left_pc_mask_equal_left_choice_prime = 1 \/ bpr_right_pc_mask_equal_left_choice_prime = 1)) /\ pc_bit_mask_equal_left = 0)))) -> (forall pc_index_mask_equal_right. (exists pc_lt_mask_equal_right_bound. pc_lt_mask_equal_right_bound + S (pc_index_mask_equal_right) = (l)) -> exists pc_bit_mask_equal_right. (((exists fs_h_pc_mask_equal_right_entry. fs_h_pc_mask_equal_right_entry + S (pc_bit_mask_equal_right) = S ((S (pc_index_mask_equal_right)) * f)) /\ exists fs_q_pc_mask_equal_right_entry. d = fs_q_pc_mask_equal_right_entry * S ((S (pc_index_mask_equal_right)) * f) + (pc_bit_mask_equal_right))) /\ (((((~(S (pc_index_mask_equal_right) = 1) /\ forall bpr_left_pc_mask_equal_right_choice_prime bpr_right_pc_mask_equal_right_choice_prime. S (pc_index_mask_equal_right) = bpr_left_pc_mask_equal_right_choice_prime * bpr_right_pc_mask_equal_right_choice_prime -> bpr_left_pc_mask_equal_right_choice_prime = 1 \/ bpr_right_pc_mask_equal_right_choice_prime = 1)) /\ pc_bit_mask_equal_right = 1) \/ (~((~(S (pc_index_mask_equal_right) = 1) /\ forall bpr_left_pc_mask_equal_right_choice_prime bpr_right_pc_mask_equal_right_choice_prime. S (pc_index_mask_equal_right) = bpr_left_pc_mask_equal_right_choice_prime * bpr_right_pc_mask_equal_right_choice_prime -> bpr_left_pc_mask_equal_right_choice_prime = 1 \/ bpr_right_pc_mask_equal_right_choice_prime = 1)) /\ pc_bit_mask_equal_right = 0)))) -> (exists pc_lt_mask_equal_bound. pc_lt_mask_equal_bound + S (i) = (l)) -> (((exists fs_h_pc_mask_equal_e. fs_h_pc_mask_equal_e + S (e) = S ((S (i)) * c)) /\ exists fs_q_pc_mask_equal_e. b = fs_q_pc_mask_equal_e * S ((S (i)) * c) + (e))) -> (((exists fs_h_pc_mask_equal_a. fs_h_pc_mask_equal_a + S (a) = S ((S (i)) * f)) /\ exists fs_q_pc_mask_equal_a. d = fs_q_pc_mask_equal_a * S ((S (i)) * f) + (a))) -> e = a

Constructive proof overview

Generated structural guide

Primality masks with different beta codes have equal entries at every actual shared index.

The unchanged tactic script uses 2 declared prerequisites and contains 35 exact native proof lines.

Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

PC0032 prime_bit_choice_functional PC0004 prime_bit_prefix_entry

Direct dependents

PC0034 prime_count_functional

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

35 script commands · 5 reading checkpoints · 0 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (2)

prime bit choice functional prime bit prefix entry

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.