PC0006

prime_bit_prefix_exists

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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 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)))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 3 declared prerequisites and contains 21 exact native proof lines.

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

Proof neighborhood

Direct dependencies

PC0002 prime_bit_prefix_empty PC0001 prime_bit_choice_exists PC0005 prime_bit_prefix_extend

Direct dependents

PC0008 prime_count_exists

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

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.

Named ingredients (3)
prime bit prefix emptyprime bit choice existsprime bit prefix extend

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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
  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
  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 exact 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 : exists b c. forall pc_index_mask_exists_pre. (exists pc_lt_mask_exists_pre_bound. pc_lt_mask_exists_pre_bound + S (pc_index_mask_exists_pre) = (l)) -> exists pc_bit_mask_exists_pre. (((exists fs_h_pc_mask_exists_pre_entry. fs_h_pc_mask_exists_pre_entry + S (pc_bit_mask_exists_pre) = S ((S (pc_index_mask_exists_pre)) * c)) /\ exists fs_q_pc_mask_exists_pre_entry. b = fs_q_pc_mask_exists_pre_entry * S ((S (pc_index_mask_exists_pre)) * c) + (pc_bit_mask_exists_pre))) /\ (((((~(S (pc_index_mask_exists_pre) = 1) /\ forall bpr_left_pc_mask_exists_pre_choice_prime bpr_right_pc_mask_exists_pre_choice_prime. S (pc_index_mask_exists_pre) = bpr_left_pc_mask_exists_pre_choice_prime * bpr_right_pc_mask_exists_pre_choice_prime -> bpr_left_pc_mask_exists_pre_choice_prime = 1 \/ bpr_right_pc_mask_exists_pre_choice_prime = 1)) /\ pc_bit_mask_exists_pre = 1) \/ (~((~(S (pc_index_mask_exists_pre) = 1) /\ forall bpr_left_pc_mask_exists_pre_choice_prime bpr_right_pc_mask_exists_pre_choice_prime. S (pc_index_mask_exists_pre) = bpr_left_pc_mask_exists_pre_choice_prime * bpr_right_pc_mask_exists_pre_choice_prime -> bpr_left_pc_mask_exists_pre_choice_prime = 1 \/ bpr_right_pc_mask_exists_pre_choice_prime = 1)) /\ pc_bit_mask_exists_pre = 0)))
  8. 0008apply IH
  9. 0009cases hpre
  10. 0010cases hpre_witness
  11. 0011have hc : exists e. ((((~(S (l) = 1) /\ forall bpr_left_pc_mask_exists_choice_prime bpr_right_pc_mask_exists_choice_prime. S (l) = 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)) /\ e = 1) \/ (~((~(S (l) = 1) /\ forall bpr_left_pc_mask_exists_choice_prime bpr_right_pc_mask_exists_choice_prime. S (l) = 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)) /\ 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