KU0000

division_add_quotient_bit

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

Adding arbitrary dividends changes the sum of their quotients by at most one carry.

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 d a b q r s t Q R. (((a) = (d) * (q) + (r) /\ (exists bcf_lt_gap_kmvadqb_left_bound. bcf_lt_gap_kmvadqb_left_bound + S (r) = d))) -> (((b) = (d) * (s) + (t) /\ (exists bcf_lt_gap_kmvadqb_right_bound. bcf_lt_gap_kmvadqb_right_bound + S (t) = d))) -> (((a + b) = (d) * (Q) + (R) /\ (exists bcf_lt_gap_kmvadqb_total_bound. bcf_lt_gap_kmvadqb_total_bound + S (R) = d))) -> (Q = q + s \/ Q = S (q + s))

Constructive proof overview

Generated structural guide

Adding arbitrary dividends changes the sum of their quotients by at most one carry.

The unchanged tactic script uses 12 declared prerequisites and contains 138 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

le_or_lt Stable theorem; checked-use authorized le_eq_or_lt Stable theorem; checked-use authorized lt_not_le Stable theorem; checked-use authorized zero_le Stable theorem; checked-use authorized one_le_of_ne_zero Stable theorem; checked-use authorized add_shuffle_middle Alpha theorem; checked-use authorized mul_add Stable theorem; checked-use authorized add_assoc Stable theorem; checked-use authorized add_comm Stable theorem; checked-use authorized add_lt_add Alpha theorem; checked-use authorized add_lt_cancel_left Alpha theorem; checked-use authorized division_remainder_unique Stable theorem; checked-use authorized

Direct dependents

KU0001 division_add_quotient_lower KU0002 division_add_quotient_upper KU0006 add_quotient_carry_choice

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

138 script commands · 30 reading checkpoints · 12 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.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro d
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro q
  5. L5
    intro r
  6. L6
    intro s
  7. L7
    intro t
  8. L8
    intro Q
  9. L9
    intro R
  10. L10
    intro hleft
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hright
  2. L12
    intro htotal
03Separate the logical casesL13–15

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

  1. L13
    cases hleft
  2. L14
    cases hright
  3. L15
    cases htotal
04Establish hsum_eqL16–25

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

  1. L16
    have hsum_eq : a + b = d * (q + s) + (r + t)
  2. L17
    rewrite hleft_left
  3. L18
    rewrite hright_left
  4. L19
    trans (d * q + d * s) + (r + t)
  5. L20
    apply add_shuffle_middle
  6. L21
    congr
  7. L22
    symm
  8. L23
    apply mul_add
  9. L24
    refl
  10. L25
    specialize le_or_lt (r + t)
05Use earlier factsL26–26

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

  1. L26
    specialize le_or_lt d
06Separate the logical casesL27–27

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

  1. L27
    cases le_or_lt
07Establish hsplitL28–32

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

  1. L28
    have hsplit : r + t = d \/ exists z. z + S (r + t) = d
  2. L29
    specialize le_eq_or_lt (r + t)
  3. L30
    specialize le_eq_or_lt d
  4. L31
    apply le_eq_or_lt
  5. L32
    exact le_or_lt_left
08Separate the logical casesL33–33

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

  1. L33
    cases hsplit
09Establish hd0L34–42

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

  1. L34
    have hd0 : ~(d = 0)
  2. L35
    intro hd
  3. L36
    rewrite hd at hleft_right
  4. L37
    specialize lt_not_le r
  5. L38
    specialize lt_not_le 0
  6. L39
    apply lt_not_le
  7. L40
    exact hleft_right
  8. L41
    specialize zero_le r
  9. L42
    exact zero_le
10Establish hzero_boundL43–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply one le of ne zero.

  1. L43
    have hzero_bound : exists z. z + S 0 = d
  2. L44
    specialize one_le_of_ne_zero d
  3. L45
    apply one_le_of_ne_zero
  4. L46
    exact hd0
11Establish hcandidate_eqL47–55

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

  1. L47
    have hcandidate_eq : a + b = d * S (q + s) + 0
  2. L48
    trans d * (q + s) + (r + t)
  3. L49
    exact hsum_eq
  4. L50
    rewrite hsplit_left
  5. L51
    trans d * S (q + s)
  6. L52
    symm
  7. L53
    apply PA6
  8. L54
    symm
  9. L55
    apply PA3
12Establish huniqueL56–65

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

  1. L56
    have hunique : Q = S (q + s) /\ R = 0
  2. L57
    specialize division_remainder_unique d
  3. L58
    specialize division_remainder_unique (a + b)
  4. L59
    specialize division_remainder_unique Q
  5. L60
    specialize division_remainder_unique R
  6. L61
    specialize division_remainder_unique (S (q + s))
  7. L62
    specialize division_remainder_unique 0
  8. L63
    apply division_remainder_unique
  9. L64
    exact htotal_left
  10. L65
    exact htotal_right
13Use earlier factsL66–67

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

  1. L66
    exact hcandidate_eq
  2. L67
    exact hzero_bound
14Separate the logical casesL68–69

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

  1. L68
    cases hunique
  2. L69
    right
15Use earlier factsL70–70

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

  1. L70
    exact hunique_left
16Establish huniqueL71–80

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

  1. L71
    have hunique : Q = q + s /\ R = r + t
  2. L72
    specialize division_remainder_unique d
  3. L73
    specialize division_remainder_unique (a + b)
  4. L74
    specialize division_remainder_unique Q
  5. L75
    specialize division_remainder_unique R
  6. L76
    specialize division_remainder_unique (q + s)
  7. L77
    specialize division_remainder_unique (r + t)
  8. L78
    apply division_remainder_unique
  9. L79
    exact htotal_left
  10. L80
    exact htotal_right
17Use earlier factsL81–82

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

  1. L81
    exact hsum_eq
  2. L82
    exact hsplit_right
18Separate the logical casesL83–84

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

  1. L83
    cases hunique
  2. L84
    left
19Use earlier factsL85–85

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

  1. L85
    exact hunique_left
20Separate the logical casesL86–86

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

  1. L86
    cases le_or_lt_right
21Establish hremaindersL87–96

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

  1. L87
    have hremainders : r + t = d + S x
  2. L88
    trans x + S d
  3. L89
    symm
  4. L90
    exact le_or_lt_right_witness
  5. L91
    trans S (x + d)
  6. L92
    apply PA4
  7. L93
    trans S (d + x)
  8. L94
    congr
  9. L95
    apply add_comm
  10. L96
    symm
22Use earlier factsL97–97

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

  1. L97
    apply PA4
23Establish hsum_ltL98–106

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

  1. L98
    have hsum_lt : exists z. z + S (r + t) = d + d
  2. L99
    specialize add_lt_add r
  3. L100
    specialize add_lt_add d
  4. L101
    specialize add_lt_add t
  5. L102
    specialize add_lt_add d
  6. L103
    apply add_lt_add
  7. L104
    exact hleft_right
  8. L105
    exact hright_right
  9. L106
    rewrite hremainders at hsum_lt
24Establish hcarry_boundL107–112

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add lt cancel left.

  1. L107
    have hcarry_bound : exists z. z + S (S x) = d
  2. L108
    specialize add_lt_cancel_left d
  3. L109
    specialize add_lt_cancel_left (S x)
  4. L110
    specialize add_lt_cancel_left d
  5. L111
    apply add_lt_cancel_left
  6. L112
    exact hsum_lt
25Establish hcandidate_eqL113–122

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

  1. L113
    have hcandidate_eq : a + b = d * S (q + s) + S x
  2. L114
    trans d * (q + s) + (r + t)
  3. L115
    exact hsum_eq
  4. L116
    rewrite hremainders
  5. L117
    trans (d * (q + s) + d) + S x
  6. L118
    symm
  7. L119
    apply add_assoc
  8. L120
    congr
  9. L121
    symm
  10. L122
    apply PA6
26Calculate and transport equalitiesL123–123

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

  1. L123
    refl
27Establish huniqueL124–133

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

  1. L124
    have hunique : Q = S (q + s) /\ R = S x
  2. L125
    specialize division_remainder_unique d
  3. L126
    specialize division_remainder_unique (a + b)
  4. L127
    specialize division_remainder_unique Q
  5. L128
    specialize division_remainder_unique R
  6. L129
    specialize division_remainder_unique (S (q + s))
  7. L130
    specialize division_remainder_unique (S x)
  8. L131
    apply division_remainder_unique
  9. L132
    exact htotal_left
  10. L133
    exact htotal_right
28Use earlier factsL134–135

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

  1. L134
    exact hcandidate_eq
  2. L135
    exact hcarry_bound
29Separate the logical casesL136–137

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

  1. L136
    cases hunique
  2. L137
    right
30Use earlier factsL138–138

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

  1. L138
    exact hunique_left

Library-wide reading audit

Original exact command ledger · 138 lines
  1. 0001intro d
  2. 0002intro a
  3. 0003intro b
  4. 0004intro q
  5. 0005intro r
  6. 0006intro s
  7. 0007intro t
  8. 0008intro Q
  9. 0009intro R
  10. 0010intro hleft
  11. 0011intro hright
  12. 0012intro htotal
  13. 0013cases hleft
  14. 0014cases hright
  15. 0015cases htotal
  16. 0016have hsum_eq : a + b = d * (q + s) + (r + t)
  17. 0017rewrite hleft_left
  18. 0018rewrite hright_left
  19. 0019trans (d * q + d * s) + (r + t)
  20. 0020apply add_shuffle_middle
  21. 0021congr
  22. 0022symm
  23. 0023apply mul_add
  24. 0024refl
  25. 0025specialize le_or_lt (r + t)
  26. 0026specialize le_or_lt d
  27. 0027cases le_or_lt
  28. 0028have hsplit : r + t = d \/ exists z. z + S (r + t) = d
  29. 0029specialize le_eq_or_lt (r + t)
  30. 0030specialize le_eq_or_lt d
  31. 0031apply le_eq_or_lt
  32. 0032exact le_or_lt_left
  33. 0033cases hsplit
  34. 0034have hd0 : ~(d = 0)
  35. 0035intro hd
  36. 0036rewrite hd at hleft_right
  37. 0037specialize lt_not_le r
  38. 0038specialize lt_not_le 0
  39. 0039apply lt_not_le
  40. 0040exact hleft_right
  41. 0041specialize zero_le r
  42. 0042exact zero_le
  43. 0043have hzero_bound : exists z. z + S 0 = d
  44. 0044specialize one_le_of_ne_zero d
  45. 0045apply one_le_of_ne_zero
  46. 0046exact hd0
  47. 0047have hcandidate_eq : a + b = d * S (q + s) + 0
  48. 0048trans d * (q + s) + (r + t)
  49. 0049exact hsum_eq
  50. 0050rewrite hsplit_left
  51. 0051trans d * S (q + s)
  52. 0052symm
  53. 0053apply PA6
  54. 0054symm
  55. 0055apply PA3
  56. 0056have hunique : Q = S (q + s) /\ R = 0
  57. 0057specialize division_remainder_unique d
  58. 0058specialize division_remainder_unique (a + b)
  59. 0059specialize division_remainder_unique Q
  60. 0060specialize division_remainder_unique R
  61. 0061specialize division_remainder_unique (S (q + s))
  62. 0062specialize division_remainder_unique 0
  63. 0063apply division_remainder_unique
  64. 0064exact htotal_left
  65. 0065exact htotal_right
  66. 0066exact hcandidate_eq
  67. 0067exact hzero_bound
  68. 0068cases hunique
  69. 0069right
  70. 0070exact hunique_left
  71. 0071have hunique : Q = q + s /\ R = r + t
  72. 0072specialize division_remainder_unique d
  73. 0073specialize division_remainder_unique (a + b)
  74. 0074specialize division_remainder_unique Q
  75. 0075specialize division_remainder_unique R
  76. 0076specialize division_remainder_unique (q + s)
  77. 0077specialize division_remainder_unique (r + t)
  78. 0078apply division_remainder_unique
  79. 0079exact htotal_left
  80. 0080exact htotal_right
  81. 0081exact hsum_eq
  82. 0082exact hsplit_right
  83. 0083cases hunique
  84. 0084left
  85. 0085exact hunique_left
  86. 0086cases le_or_lt_right
  87. 0087have hremainders : r + t = d + S x
  88. 0088trans x + S d
  89. 0089symm
  90. 0090exact le_or_lt_right_witness
  91. 0091trans S (x + d)
  92. 0092apply PA4
  93. 0093trans S (d + x)
  94. 0094congr
  95. 0095apply add_comm
  96. 0096symm
  97. 0097apply PA4
  98. 0098have hsum_lt : exists z. z + S (r + t) = d + d
  99. 0099specialize add_lt_add r
  100. 0100specialize add_lt_add d
  101. 0101specialize add_lt_add t
  102. 0102specialize add_lt_add d
  103. 0103apply add_lt_add
  104. 0104exact hleft_right
  105. 0105exact hright_right
  106. 0106rewrite hremainders at hsum_lt
  107. 0107have hcarry_bound : exists z. z + S (S x) = d
  108. 0108specialize add_lt_cancel_left d
  109. 0109specialize add_lt_cancel_left (S x)
  110. 0110specialize add_lt_cancel_left d
  111. 0111apply add_lt_cancel_left
  112. 0112exact hsum_lt
  113. 0113have hcandidate_eq : a + b = d * S (q + s) + S x
  114. 0114trans d * (q + s) + (r + t)
  115. 0115exact hsum_eq
  116. 0116rewrite hremainders
  117. 0117trans (d * (q + s) + d) + S x
  118. 0118symm
  119. 0119apply add_assoc
  120. 0120congr
  121. 0121symm
  122. 0122apply PA6
  123. 0123refl
  124. 0124have hunique : Q = S (q + s) /\ R = S x
  125. 0125specialize division_remainder_unique d
  126. 0126specialize division_remainder_unique (a + b)
  127. 0127specialize division_remainder_unique Q
  128. 0128specialize division_remainder_unique R
  129. 0129specialize division_remainder_unique (S (q + s))
  130. 0130specialize division_remainder_unique (S x)
  131. 0131apply division_remainder_unique
  132. 0132exact htotal_left
  133. 0133exact htotal_right
  134. 0134exact hcandidate_eq
  135. 0135exact hcarry_bound
  136. 0136cases hunique
  137. 0137right
  138. 0138exact hunique_left