KU0007

add_quotient_carry_prefix_extend

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

A three-prefix additive carry code extends by one selected terminal bit.

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 lb lc rb rc tb tc cb cc l. (forall kmc_index_kmcpe_before. (exists bcf_lt_gap_kmcpe_before_bound. bcf_lt_gap_kmcpe_before_bound + S (kmc_index_kmcpe_before) = l) -> exists kmc_left_kmcpe_before kmc_right_kmcpe_before kmc_total_kmcpe_before kmc_bit_kmcpe_before. (((exists fs_h_kmcpe_before_left. fs_h_kmcpe_before_left + S (kmc_left_kmcpe_before) = S ((S (kmc_index_kmcpe_before)) * lc)) /\ exists fs_q_kmcpe_before_left. lb = fs_q_kmcpe_before_left * S ((S (kmc_index_kmcpe_before)) * lc) + (kmc_left_kmcpe_before))) /\ ((((exists fs_h_kmcpe_before_right. fs_h_kmcpe_before_right + S (kmc_right_kmcpe_before) = S ((S (kmc_index_kmcpe_before)) * rc)) /\ exists fs_q_kmcpe_before_right. rb = fs_q_kmcpe_before_right * S ((S (kmc_index_kmcpe_before)) * rc) + (kmc_right_kmcpe_before))) /\ ((((exists fs_h_kmcpe_before_total. fs_h_kmcpe_before_total + S (kmc_total_kmcpe_before) = S ((S (kmc_index_kmcpe_before)) * tc)) /\ exists fs_q_kmcpe_before_total. tb = fs_q_kmcpe_before_total * S ((S (kmc_index_kmcpe_before)) * tc) + (kmc_total_kmcpe_before))) /\ ((((exists fs_h_kmcpe_before_bit. fs_h_kmcpe_before_bit + S (kmc_bit_kmcpe_before) = S ((S (kmc_index_kmcpe_before)) * cc)) /\ exists fs_q_kmcpe_before_bit. cb = fs_q_kmcpe_before_bit * S ((S (kmc_index_kmcpe_before)) * cc) + (kmc_bit_kmcpe_before))) /\ (((kmc_bit_kmcpe_before = 0 /\ kmc_total_kmcpe_before = kmc_left_kmcpe_before + kmc_right_kmcpe_before) \/ (kmc_bit_kmcpe_before = 1 /\ kmc_total_kmcpe_before = S (kmc_left_kmcpe_before + kmc_right_kmcpe_before)))))))) -> (exists q s Q bit. (((exists fs_h_kmcpe_last_left. fs_h_kmcpe_last_left + S (q) = S ((S (l)) * lc)) /\ exists fs_q_kmcpe_last_left. lb = fs_q_kmcpe_last_left * S ((S (l)) * lc) + (q))) /\ ((((exists fs_h_kmcpe_last_right. fs_h_kmcpe_last_right + S (s) = S ((S (l)) * rc)) /\ exists fs_q_kmcpe_last_right. rb = fs_q_kmcpe_last_right * S ((S (l)) * rc) + (s))) /\ ((((exists fs_h_kmcpe_last_total. fs_h_kmcpe_last_total + S (Q) = S ((S (l)) * tc)) /\ exists fs_q_kmcpe_last_total. tb = fs_q_kmcpe_last_total * S ((S (l)) * tc) + (Q))) /\ (((bit = 0 /\ Q = q + s) \/ (bit = 1 /\ Q = S (q + s))))))) -> exists z h. (forall kmc_index_kmcpe_after. (exists bcf_lt_gap_kmcpe_after_bound. bcf_lt_gap_kmcpe_after_bound + S (kmc_index_kmcpe_after) = S l) -> exists kmc_left_kmcpe_after kmc_right_kmcpe_after kmc_total_kmcpe_after kmc_bit_kmcpe_after. (((exists fs_h_kmcpe_after_left. fs_h_kmcpe_after_left + S (kmc_left_kmcpe_after) = S ((S (kmc_index_kmcpe_after)) * lc)) /\ exists fs_q_kmcpe_after_left. lb = fs_q_kmcpe_after_left * S ((S (kmc_index_kmcpe_after)) * lc) + (kmc_left_kmcpe_after))) /\ ((((exists fs_h_kmcpe_after_right. fs_h_kmcpe_after_right + S (kmc_right_kmcpe_after) = S ((S (kmc_index_kmcpe_after)) * rc)) /\ exists fs_q_kmcpe_after_right. rb = fs_q_kmcpe_after_right * S ((S (kmc_index_kmcpe_after)) * rc) + (kmc_right_kmcpe_after))) /\ ((((exists fs_h_kmcpe_after_total. fs_h_kmcpe_after_total + S (kmc_total_kmcpe_after) = S ((S (kmc_index_kmcpe_after)) * tc)) /\ exists fs_q_kmcpe_after_total. tb = fs_q_kmcpe_after_total * S ((S (kmc_index_kmcpe_after)) * tc) + (kmc_total_kmcpe_after))) /\ ((((exists fs_h_kmcpe_after_bit. fs_h_kmcpe_after_bit + S (kmc_bit_kmcpe_after) = S ((S (kmc_index_kmcpe_after)) * h)) /\ exists fs_q_kmcpe_after_bit. z = fs_q_kmcpe_after_bit * S ((S (kmc_index_kmcpe_after)) * h) + (kmc_bit_kmcpe_after))) /\ (((kmc_bit_kmcpe_after = 0 /\ kmc_total_kmcpe_after = kmc_left_kmcpe_after + kmc_right_kmcpe_after) \/ (kmc_bit_kmcpe_after = 1 /\ kmc_total_kmcpe_after = S (kmc_left_kmcpe_after + kmc_right_kmcpe_after))))))))

Constructive proof overview

Generated structural guide

A three-prefix additive carry code extends by one selected terminal bit.

The unchanged tactic script uses 2 declared prerequisites and contains 85 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

beta_prefix_extend Stable theorem; checked-use authorized finite_lt_succ_eq_or_lt Stable theorem; checked-use authorized

Direct dependents

KU0008 add_quotient_carry_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

85 script commands · 31 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.

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–10

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

  1. L1
    intro lb
  2. L2
    intro lc
  3. L3
    intro rb
  4. L4
    intro rc
  5. L5
    intro tb
  6. L6
    intro tc
  7. L7
    intro cb
  8. L8
    intro cc
  9. L9
    intro l
  10. L10
    intro hprefix
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hlast
03Separate the logical casesL12–18

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

  1. L12
    cases hlast
  2. L13
    cases hlast_witness
  3. L14
    cases hlast_witness_witness
  4. L15
    cases hlast_witness_witness_witness
  5. L16
    cases hlast_witness_witness_witness_witness
  6. L17
    cases hlast_witness_witness_witness_witness_right
  7. L18
    cases hlast_witness_witness_witness_witness_right_right
04Use earlier factsL19–22

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

  1. L19
    specialize beta_prefix_extend l
  2. L20
    specialize beta_prefix_extend cb
  3. L21
    specialize beta_prefix_extend cc
  4. L22
    specialize beta_prefix_extend x3
05Separate the logical casesL23–25

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

  1. L23
    cases beta_prefix_extend
  2. L24
    cases beta_prefix_extend_witness
  3. L25
    cases beta_prefix_extend_witness_witness
06Construct an explicit witnessL26–27

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

  1. L26
    exists x4
  2. L27
    exists x5
07Fix variables and assumptionsL28–29

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

  1. L28
    intro i
  2. L29
    intro hi
08Use earlier factsL30–31

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

  1. L30
    specialize finite_lt_succ_eq_or_lt l
  2. L31
    specialize finite_lt_succ_eq_or_lt i
09Establish hsplitL32–34

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

  1. L32
    have hsplit : i = l \/ exists z. z + S i = l
  2. L33
    apply finite_lt_succ_eq_or_lt
  3. L34
    exact hi
10Separate the logical casesL35–35

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

  1. L35
    cases hsplit
11Calculate and transport equalitiesL36–43

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

  1. L36
    rewrite hsplit_left
  2. L37
    rewrite hsplit_left
  3. L38
    rewrite hsplit_left
  4. L39
    rewrite hsplit_left
  5. L40
    rewrite hsplit_left
  6. L41
    rewrite hsplit_left
  7. L42
    rewrite hsplit_left
  8. L43
    rewrite hsplit_left
12Construct an explicit witnessL44–47

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

  1. L44
    exists x
  2. L45
    exists x1
  3. L46
    exists x2
  4. L47
    exists x3
13Separate the logical casesL48–48

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

  1. L48
    split
14Use earlier factsL49–49

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

  1. L49
    exact hlast_witness_witness_witness_witness_left
15Separate the logical casesL50–50

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

  1. L50
    split
16Use earlier factsL51–51

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

  1. L51
    exact hlast_witness_witness_witness_witness_right_left
17Separate the logical casesL52–52

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

  1. L52
    split
18Use earlier factsL53–53

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

  1. L53
    exact hlast_witness_witness_witness_witness_right_right_left
19Separate the logical casesL54–54

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

  1. L54
    split
20Use earlier factsL55–56

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

  1. L55
    exact beta_prefix_extend_witness_witness_left
  2. L56
    exact hlast_witness_witness_witness_witness_right_right_right
21Establish holdL57–60

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

  1. L57
    have hold : ∃ q. ∃ s. ∃ Q. ∃ bit. BetaAt(lb,lc,i,q) ∧ (BetaAt(rb,rc,i,s) ∧ (BetaAt(tb,tc,i,Q) ∧ (BetaAt(cb,cc,i,bit) ∧ (bit = 0 ∧ Q = q + s ∨ bit = 1 ∧ Q = S (q + s)))))Definitions: BetaAt
  2. L58
    specialize hprefix i
  3. L59
    apply hprefix
  4. L60
    exact hsplit_right
22Separate the logical casesL61–68

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

  1. L61
    cases hold
  2. L62
    cases hold_witness
  3. L63
    cases hold_witness_witness
  4. L64
    cases hold_witness_witness_witness
  5. L65
    cases hold_witness_witness_witness_witness
  6. L66
    cases hold_witness_witness_witness_witness_right
  7. L67
    cases hold_witness_witness_witness_witness_right_right
  8. L68
    cases hold_witness_witness_witness_witness_right_right_right
23Construct an explicit witnessL69–72

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

  1. L69
    exists x6
  2. L70
    exists x7
  3. L71
    exists x8
  4. L72
    exists x9
24Separate the logical casesL73–73

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

  1. L73
    split
25Use earlier factsL74–74

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

  1. L74
    exact hold_witness_witness_witness_witness_left
26Separate the logical casesL75–75

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

  1. L75
    split
27Use earlier factsL76–76

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

  1. L76
    exact hold_witness_witness_witness_witness_right_left
28Separate the logical casesL77–77

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

  1. L77
    split
29Use earlier factsL78–78

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

  1. L78
    exact hold_witness_witness_witness_witness_right_right_left
30Separate the logical casesL79–79

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

  1. L79
    split
31Use earlier factsL80–85

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

  1. L80
    specialize beta_prefix_extend_witness_witness_right i
  2. L81
    specialize beta_prefix_extend_witness_witness_right x9
  3. L82
    apply beta_prefix_extend_witness_witness_right
  4. L83
    exact hsplit_right
  5. L84
    exact hold_witness_witness_witness_witness_right_right_right_left
  6. L85
    exact hold_witness_witness_witness_witness_right_right_right_right

Library-wide reading audit

Original exact command ledger · 85 lines
  1. 0001intro lb
  2. 0002intro lc
  3. 0003intro rb
  4. 0004intro rc
  5. 0005intro tb
  6. 0006intro tc
  7. 0007intro cb
  8. 0008intro cc
  9. 0009intro l
  10. 0010intro hprefix
  11. 0011intro hlast
  12. 0012cases hlast
  13. 0013cases hlast_witness
  14. 0014cases hlast_witness_witness
  15. 0015cases hlast_witness_witness_witness
  16. 0016cases hlast_witness_witness_witness_witness
  17. 0017cases hlast_witness_witness_witness_witness_right
  18. 0018cases hlast_witness_witness_witness_witness_right_right
  19. 0019specialize beta_prefix_extend l
  20. 0020specialize beta_prefix_extend cb
  21. 0021specialize beta_prefix_extend cc
  22. 0022specialize beta_prefix_extend x3
  23. 0023cases beta_prefix_extend
  24. 0024cases beta_prefix_extend_witness
  25. 0025cases beta_prefix_extend_witness_witness
  26. 0026exists x4
  27. 0027exists x5
  28. 0028intro i
  29. 0029intro hi
  30. 0030specialize finite_lt_succ_eq_or_lt l
  31. 0031specialize finite_lt_succ_eq_or_lt i
  32. 0032have hsplit : i = l \/ exists z. z + S i = l
  33. 0033apply finite_lt_succ_eq_or_lt
  34. 0034exact hi
  35. 0035cases hsplit
  36. 0036rewrite hsplit_left
  37. 0037rewrite hsplit_left
  38. 0038rewrite hsplit_left
  39. 0039rewrite hsplit_left
  40. 0040rewrite hsplit_left
  41. 0041rewrite hsplit_left
  42. 0042rewrite hsplit_left
  43. 0043rewrite hsplit_left
  44. 0044exists x
  45. 0045exists x1
  46. 0046exists x2
  47. 0047exists x3
  48. 0048split
  49. 0049exact hlast_witness_witness_witness_witness_left
  50. 0050split
  51. 0051exact hlast_witness_witness_witness_witness_right_left
  52. 0052split
  53. 0053exact hlast_witness_witness_witness_witness_right_right_left
  54. 0054split
  55. 0055exact beta_prefix_extend_witness_witness_left
  56. 0056exact hlast_witness_witness_witness_witness_right_right_right
  57. 0057have hold : exists q s Q bit. (((exists fs_h_kmcpe_old_left. fs_h_kmcpe_old_left + S (q) = S ((S (i)) * lc)) /\ exists fs_q_kmcpe_old_left. lb = fs_q_kmcpe_old_left * S ((S (i)) * lc) + (q))) /\ ((((exists fs_h_kmcpe_old_right. fs_h_kmcpe_old_right + S (s) = S ((S (i)) * rc)) /\ exists fs_q_kmcpe_old_right. rb = fs_q_kmcpe_old_right * S ((S (i)) * rc) + (s))) /\ ((((exists fs_h_kmcpe_old_total. fs_h_kmcpe_old_total + S (Q) = S ((S (i)) * tc)) /\ exists fs_q_kmcpe_old_total. tb = fs_q_kmcpe_old_total * S ((S (i)) * tc) + (Q))) /\ ((((exists fs_h_kmcpe_old_bit. fs_h_kmcpe_old_bit + S (bit) = S ((S (i)) * cc)) /\ exists fs_q_kmcpe_old_bit. cb = fs_q_kmcpe_old_bit * S ((S (i)) * cc) + (bit))) /\ (((bit = 0 /\ Q = q + s) \/ (bit = 1 /\ Q = S (q + s)))))))
  58. 0058specialize hprefix i
  59. 0059apply hprefix
  60. 0060exact hsplit_right
  61. 0061cases hold
  62. 0062cases hold_witness
  63. 0063cases hold_witness_witness
  64. 0064cases hold_witness_witness_witness
  65. 0065cases hold_witness_witness_witness_witness
  66. 0066cases hold_witness_witness_witness_witness_right
  67. 0067cases hold_witness_witness_witness_witness_right_right
  68. 0068cases hold_witness_witness_witness_witness_right_right_right
  69. 0069exists x6
  70. 0070exists x7
  71. 0071exists x8
  72. 0072exists x9
  73. 0073split
  74. 0074exact hold_witness_witness_witness_witness_left
  75. 0075split
  76. 0076exact hold_witness_witness_witness_witness_right_left
  77. 0077split
  78. 0078exact hold_witness_witness_witness_witness_right_right_left
  79. 0079split
  80. 0080specialize beta_prefix_extend_witness_witness_right i
  81. 0081specialize beta_prefix_extend_witness_witness_right x9
  82. 0082apply beta_prefix_extend_witness_witness_right
  83. 0083exact hsplit_right
  84. 0084exact hold_witness_witness_witness_witness_right_right_right_left
  85. 0085exact hold_witness_witness_witness_witness_right_right_right_right