PC0006

prime_bit_prefix_exists

HA induction constructs the complete finite primality mask at every natural bound.

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

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

∀ l. ∃ b. ∃ c. PrimeBitPrefix(b,c,l)

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

Definition DAG

PrimeBitPrefix(b,c,l) · 2Prime(p) · 2

Actual proof prerequisites

prime_bit_prefix_emptyprime_bit_choice_existsprime_bit_prefix_extend
Original expanded first-order statement 
forall l. exists b c. forall pc_index_mask_exists. (exists pc_lt_mask_exists_bound. pc_lt_mask_exists_bound + S (pc_index_mask_exists) = (l)) -> exists pc_bit_mask_exists. (((exists fs_h_pc_mask_exists_entry. fs_h_pc_mask_exists_entry + S (pc_bit_mask_exists) = S ((S (pc_index_mask_exists)) * c)) /\ exists fs_q_pc_mask_exists_entry. b = fs_q_pc_mask_exists_entry * S ((S (pc_index_mask_exists)) * c) + (pc_bit_mask_exists))) /\ (((((~(S (pc_index_mask_exists) = 1) /\ forall bpr_left_pc_mask_exists_choice_prime bpr_right_pc_mask_exists_choice_prime. S (pc_index_mask_exists) = bpr_left_pc_mask_exists_choice_prime * bpr_right_pc_mask_exists_choice_prime -> bpr_left_pc_mask_exists_choice_prime = 1 \/ bpr_right_pc_mask_exists_choice_prime = 1)) /\ pc_bit_mask_exists = 1) \/ (~((~(S (pc_index_mask_exists) = 1) /\ forall bpr_left_pc_mask_exists_choice_prime bpr_right_pc_mask_exists_choice_prime. S (pc_index_mask_exists) = bpr_left_pc_mask_exists_choice_prime * bpr_right_pc_mask_exists_choice_prime -> bpr_left_pc_mask_exists_choice_prime = 1 \/ bpr_right_pc_mask_exists_choice_prime = 1)) /\ pc_bit_mask_exists = 0)))

Complete tactic proof in conservative notation

All 21 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

21 script commands · 8 reading checkpoints · 2 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 (3)
prime bit prefix emptyprime bit choice existsprime bit prefix extend
01Induction on lL1–1

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L1
    induction l
02Construct an explicit witnessL2–3

Supply the displayed value, then prove that it has the required property.

  1. L2
    exists 0
  2. L3
    exists 0
03Use earlier factsL4–6

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L4
    specialize prime_bit_prefix_empty 0
  2. L5
    specialize prime_bit_prefix_empty 0
  3. L6
    apply prime_bit_prefix_empty
04Establish hpreL7–8

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.

  1. L7
    have hpre : ∃ b. ∃ c. PrimeBitPrefix(b,c,l)Definitions: PrimeBitPrefix(b,c,l)Original native command in the exact edition
  2. L8
    apply IH
05Separate the logical casesL9–10

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L9
    cases hpre
  2. L10
    cases hpre_witness
06Establish hcL11–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime bit choice exists.

  1. L11
    have hc : ∃ e. Prime(S l) ∧ e = 1 ∨ ¬Prime(S l) ∧ e = 0Definitions: Prime(S l)Original native command in the exact edition
  2. L12
    specialize prime_bit_choice_exists l
  3. L13
    apply prime_bit_choice_exists
07Separate the logical casesL14–14

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L14
    cases hc
08Use earlier factsL15–21

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L15
    specialize prime_bit_prefix_extend x
  2. L16
    specialize prime_bit_prefix_extend x1
  3. L17
    specialize prime_bit_prefix_extend l
  4. L18
    specialize prime_bit_prefix_extend x2
  5. L19
    apply prime_bit_prefix_extend
  6. L20
    exact hpre_witness_witness
  7. L21
    exact hc_witness

Library-wide reading audit

Original defined command ledger · 21 lines
  1. 0001induction l
  2. 0002exists 0
  3. 0003exists 0
  4. 0004specialize prime_bit_prefix_empty 0
  5. 0005specialize prime_bit_prefix_empty 0
  6. 0006apply prime_bit_prefix_empty
  7. 0007have hpre : ∃ b. ∃ c. PrimeBitPrefix(b,c,l)
  8. 0008apply IH
  9. 0009cases hpre
  10. 0010cases hpre_witness
  11. 0011have hc : ∃ e. Prime(S l) ∧ e = 1 ∨ ¬Prime(S l) ∧ e = 0
  12. 0012specialize prime_bit_choice_exists l
  13. 0013apply prime_bit_choice_exists
  14. 0014cases hc
  15. 0015specialize prime_bit_prefix_extend x
  16. 0016specialize prime_bit_prefix_extend x1
  17. 0017specialize prime_bit_prefix_extend l
  18. 0018specialize prime_bit_prefix_extend x2
  19. 0019apply prime_bit_prefix_extend
  20. 0020exact hpre_witness_witness
  21. 0021exact hc_witness