PC0005

prime_bit_prefix_extend

Append a genuinely decided prime bit while preserving the entire existing prefix.

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

∀ b. ∀ c. ∀ l. ∀ e. PrimeBitPrefix(b,c,l) → Prime(S l) ∧ e = 1 ∨ ¬Prime(S l) ∧ e = 0 → ∃ x. ∃ y. PrimeBitPrefix(x,y,S l)

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

Definition DAG

PrimeBitPrefix(b,c,l) · 2Lt(a,b) · 2Prime(p) · 4BetaAt(b,c,i,x) · 4

Actual proof prerequisites

beta_prefix_extend · checked external prerequisitele_eq_or_lt · checked external prerequisitele_of_succ_le_succ · checked external prerequisite
Original expanded first-order statement 
forall b c l e. (forall pc_index_mask_extend_source. (exists pc_lt_mask_extend_source_bound. pc_lt_mask_extend_source_bound + S (pc_index_mask_extend_source) = (l)) -> exists pc_bit_mask_extend_source. (((exists fs_h_pc_mask_extend_source_entry. fs_h_pc_mask_extend_source_entry + S (pc_bit_mask_extend_source) = S ((S (pc_index_mask_extend_source)) * c)) /\ exists fs_q_pc_mask_extend_source_entry. b = fs_q_pc_mask_extend_source_entry * S ((S (pc_index_mask_extend_source)) * c) + (pc_bit_mask_extend_source))) /\ (((((~(S (pc_index_mask_extend_source) = 1) /\ forall bpr_left_pc_mask_extend_source_choice_prime bpr_right_pc_mask_extend_source_choice_prime. S (pc_index_mask_extend_source) = bpr_left_pc_mask_extend_source_choice_prime * bpr_right_pc_mask_extend_source_choice_prime -> bpr_left_pc_mask_extend_source_choice_prime = 1 \/ bpr_right_pc_mask_extend_source_choice_prime = 1)) /\ pc_bit_mask_extend_source = 1) \/ (~((~(S (pc_index_mask_extend_source) = 1) /\ forall bpr_left_pc_mask_extend_source_choice_prime bpr_right_pc_mask_extend_source_choice_prime. S (pc_index_mask_extend_source) = bpr_left_pc_mask_extend_source_choice_prime * bpr_right_pc_mask_extend_source_choice_prime -> bpr_left_pc_mask_extend_source_choice_prime = 1 \/ bpr_right_pc_mask_extend_source_choice_prime = 1)) /\ pc_bit_mask_extend_source = 0)))) -> (((((~(S (l) = 1) /\ forall bpr_left_pc_mask_extend_choice_prime bpr_right_pc_mask_extend_choice_prime. S (l) = bpr_left_pc_mask_extend_choice_prime * bpr_right_pc_mask_extend_choice_prime -> bpr_left_pc_mask_extend_choice_prime = 1 \/ bpr_right_pc_mask_extend_choice_prime = 1)) /\ e = 1) \/ (~((~(S (l) = 1) /\ forall bpr_left_pc_mask_extend_choice_prime bpr_right_pc_mask_extend_choice_prime. S (l) = bpr_left_pc_mask_extend_choice_prime * bpr_right_pc_mask_extend_choice_prime -> bpr_left_pc_mask_extend_choice_prime = 1 \/ bpr_right_pc_mask_extend_choice_prime = 1)) /\ e = 0))) -> exists d f. forall pc_index_mask_extend_target. (exists pc_lt_mask_extend_target_bound. pc_lt_mask_extend_target_bound + S (pc_index_mask_extend_target) = (S l)) -> exists pc_bit_mask_extend_target. (((exists fs_h_pc_mask_extend_target_entry. fs_h_pc_mask_extend_target_entry + S (pc_bit_mask_extend_target) = S ((S (pc_index_mask_extend_target)) * f)) /\ exists fs_q_pc_mask_extend_target_entry. d = fs_q_pc_mask_extend_target_entry * S ((S (pc_index_mask_extend_target)) * f) + (pc_bit_mask_extend_target))) /\ (((((~(S (pc_index_mask_extend_target) = 1) /\ forall bpr_left_pc_mask_extend_target_choice_prime bpr_right_pc_mask_extend_target_choice_prime. S (pc_index_mask_extend_target) = bpr_left_pc_mask_extend_target_choice_prime * bpr_right_pc_mask_extend_target_choice_prime -> bpr_left_pc_mask_extend_target_choice_prime = 1 \/ bpr_right_pc_mask_extend_target_choice_prime = 1)) /\ pc_bit_mask_extend_target = 1) \/ (~((~(S (pc_index_mask_extend_target) = 1) /\ forall bpr_left_pc_mask_extend_target_choice_prime bpr_right_pc_mask_extend_target_choice_prime. S (pc_index_mask_extend_target) = bpr_left_pc_mask_extend_target_choice_prime * bpr_right_pc_mask_extend_target_choice_prime -> bpr_left_pc_mask_extend_target_choice_prime = 1 \/ bpr_right_pc_mask_extend_target_choice_prime = 1)) /\ pc_bit_mask_extend_target = 0)))

Complete tactic proof in conservative notation

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

52 script commands · 18 reading checkpoints · 3 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.

01Fix variables and assumptionsL1–6

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro e
  5. L5
    intro h
  6. L6
    intro he
02Establish hextL7–12

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

  1. L7
    have hext : ∃ d. ∃ f. BetaAt(d,f,l,e) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(d,f,x,y))Definitions: BetaAt(d,f,l,e)Lt(x,l)BetaAt(b,c,x,y)BetaAt(d,f,x,y)Original native command in the exact edition
  2. L8
    specialize beta_prefix_extend l
  3. L9
    specialize beta_prefix_extend b
  4. L10
    specialize beta_prefix_extend c
  5. L11
    specialize beta_prefix_extend e
  6. L12
    apply beta_prefix_extend
03Separate the logical casesL13–15

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

  1. L13
    cases hext
  2. L14
    cases hext_witness
  3. L15
    cases hext_witness_witness
04Construct an explicit witnessL16–17

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

  1. L16
    exists x
  2. L17
    exists x1
05Fix variables and assumptionsL18–19

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

  1. L18
    intro i
  2. L19
    intro hi
06Establish hcasesL20–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L20
    have hcases : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L21
    specialize le_eq_or_lt i
  3. L22
    specialize le_eq_or_lt l
  4. L23
    apply le_eq_or_lt
  5. L24
    specialize le_of_succ_le_succ i
  6. L25
    specialize le_of_succ_le_succ l
  7. L26
    apply le_of_succ_le_succ
  8. L27
    exact hi
07Separate the logical casesL28–28

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

  1. L28
    cases hcases
08Construct an explicit witnessL29–29

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

  1. L29
    exists e
09Separate the logical casesL30–30

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

  1. L30
    split
10Calculate and transport equalitiesL31–32

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L31
    rewrite hcases_left
  2. L32
    rewrite hcases_left
11Use earlier factsL33–33

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

  1. L33
    exact hext_witness_witness_left
12Calculate and transport equalitiesL34–37

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L34
    rewrite hcases_left
  2. L35
    rewrite hcases_left
  3. L36
    rewrite hcases_left
  4. L37
    rewrite hcases_left
13Use earlier factsL38–38

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

  1. L38
    exact he
14Establish hpL39–42

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

  1. L39
    have hp : ∃ a. BetaAt(b,c,i,a) ∧ (Prime(S i) ∧ a = 1 ∨ ¬Prime(S i) ∧ a = 0)Definitions: BetaAt(b,c,i,a)Prime(S i)Original native command in the exact edition
  2. L40
    specialize h i
  3. L41
    apply h
  4. L42
    exact hcases_right
15Separate the logical casesL43–44

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

  1. L43
    cases hp
  2. L44
    cases hp_witness
16Construct an explicit witnessL45–45

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

  1. L45
    exists x2
17Separate the logical casesL46–46

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

  1. L46
    split
18Use earlier factsL47–52

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

  1. L47
    specialize hext_witness_witness_right i
  2. L48
    specialize hext_witness_witness_right x2
  3. L49
    apply hext_witness_witness_right
  4. L50
    exact hcases_right
  5. L51
    exact hp_witness_left
  6. L52
    exact hp_witness_right

Library-wide reading audit

Original defined command ledger · 52 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro e
  5. 0005intro h
  6. 0006intro he
  7. 0007have hext : ∃ d. ∃ f. BetaAt(d,f,l,e) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(d,f,x,y))
  8. 0008specialize beta_prefix_extend l
  9. 0009specialize beta_prefix_extend b
  10. 0010specialize beta_prefix_extend c
  11. 0011specialize beta_prefix_extend e
  12. 0012apply beta_prefix_extend
  13. 0013cases hext
  14. 0014cases hext_witness
  15. 0015cases hext_witness_witness
  16. 0016exists x
  17. 0017exists x1
  18. 0018intro i
  19. 0019intro hi
  20. 0020have hcases : i = l ∨ Lt(i,l)
  21. 0021specialize le_eq_or_lt i
  22. 0022specialize le_eq_or_lt l
  23. 0023apply le_eq_or_lt
  24. 0024specialize le_of_succ_le_succ i
  25. 0025specialize le_of_succ_le_succ l
  26. 0026apply le_of_succ_le_succ
  27. 0027exact hi
  28. 0028cases hcases
  29. 0029exists e
  30. 0030split
  31. 0031rewrite hcases_left
  32. 0032rewrite hcases_left
  33. 0033exact hext_witness_witness_left
  34. 0034rewrite hcases_left
  35. 0035rewrite hcases_left
  36. 0036rewrite hcases_left
  37. 0037rewrite hcases_left
  38. 0038exact he
  39. 0039have hp : ∃ a. BetaAt(b,c,i,a) ∧ (Prime(S i) ∧ a = 1 ∨ ¬Prime(S i) ∧ a = 0)
  40. 0040specialize h i
  41. 0041apply h
  42. 0042exact hcases_right
  43. 0043cases hp
  44. 0044cases hp_witness
  45. 0045exists x2
  46. 0046split
  47. 0047specialize hext_witness_witness_right i
  48. 0048specialize hext_witness_witness_right x2
  49. 0049apply hext_witness_witness_right
  50. 0050exact hcases_right
  51. 0051exact hp_witness_left
  52. 0052exact hp_witness_right