PC0005

prime_bit_prefix_extend

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

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

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

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

beta_prefix_extend Stable theorem; checked-use authorized le_eq_or_lt Stable theorem; checked-use authorized le_of_succ_le_succ Stable theorem; checked-use authorized

Direct dependents

PC0006 prime_bit_prefix_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

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.

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.

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: LtBetaAt
  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 \/ exists g. g + S i = l
  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: PrimeBetaAt
  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 exact 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 : exists d f. (((exists fs_h_pc_mask_extend_last. fs_h_pc_mask_extend_last + S (e) = S ((S (l)) * f)) /\ exists fs_q_pc_mask_extend_last. d = fs_q_pc_mask_extend_last * S ((S (l)) * f) + (e))) /\ forall i a. (exists pc_lt_mask_extend_bound. pc_lt_mask_extend_bound + S (i) = (l)) -> (((exists fs_h_pc_mask_extend_old. fs_h_pc_mask_extend_old + S (a) = S ((S (i)) * c)) /\ exists fs_q_pc_mask_extend_old. b = fs_q_pc_mask_extend_old * S ((S (i)) * c) + (a))) -> (((exists fs_h_pc_mask_extend_new. fs_h_pc_mask_extend_new + S (a) = S ((S (i)) * f)) /\ exists fs_q_pc_mask_extend_new. d = fs_q_pc_mask_extend_new * S ((S (i)) * f) + (a)))
  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 \/ exists g. g + S 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 : exists a. (((exists fs_h_pc_mask_extend_point. fs_h_pc_mask_extend_point + S (a) = S ((S (i)) * c)) /\ exists fs_q_pc_mask_extend_point. b = fs_q_pc_mask_extend_point * S ((S (i)) * c) + (a))) /\ (((((~(S (i) = 1) /\ forall bpr_left_pc_mask_extend_point_choice_prime bpr_right_pc_mask_extend_point_choice_prime. S (i) = bpr_left_pc_mask_extend_point_choice_prime * bpr_right_pc_mask_extend_point_choice_prime -> bpr_left_pc_mask_extend_point_choice_prime = 1 \/ bpr_right_pc_mask_extend_point_choice_prime = 1)) /\ a = 1) \/ (~((~(S (i) = 1) /\ forall bpr_left_pc_mask_extend_point_choice_prime bpr_right_pc_mask_extend_point_choice_prime. S (i) = bpr_left_pc_mask_extend_point_choice_prime * bpr_right_pc_mask_extend_point_choice_prime -> bpr_left_pc_mask_extend_point_choice_prime = 1 \/ bpr_right_pc_mask_extend_point_choice_prime = 1)) /\ 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