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.

These are the exact finite integer inequalities with constant 8, for every N≥2. The proof uses constructive binomial and primorial infrastructure; it does not assume logarithms, asymptotic estimates, the prime number theorem, or a factorization oracle.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ d. ∀ f. ∀ l. ∀ i. ∀ e. ∀ a. PrimeBitPrefix(b,c,l) → PrimeBitPrefix(d,f,l) → Lt(i,l) → BetaAt(b,c,i,e) → BetaAt(d,f,i,a) → e = a

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

PrimeBitPrefix(b,c,l) · 2 Lt(a,b) · 1 BetaAt(b,c,i,x) · 2

Actual proof prerequisites

prime_bit_choice_functional prime_bit_prefix_entry

Original expanded first-order 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

Complete tactic proof in conservative notation

All 35 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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.