DL0076

integer_vector_add_functional

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

Two actual sums of the same signed vectors are equal as integer vectors, without claiming equality of their beta codes or separate components.

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 ab ac db dc eb ec fb fc pb pc nb nc qb qc mb mc l. (forall ics_index_add_functional_first ics_value0_add_functional_first ics_value1_add_functional_first ics_value2_add_functional_first ics_value3_add_functional_first ics_value4_add_functional_first ics_value5_add_functional_first. (exists ics_gap_add_functional_first_bound. ics_gap_add_functional_first_bound + S (ics_index_add_functional_first) = (l)) -> (((exists fs_h_ics_add_functional_first_at0. fs_h_ics_add_functional_first_at0 + S (ics_value0_add_functional_first) = S ((S (ics_index_add_functional_first)) * ac)) /\ exists fs_q_ics_add_functional_first_at0. ab = fs_q_ics_add_functional_first_at0 * S ((S (ics_index_add_functional_first)) * ac) + (ics_value0_add_functional_first))) -> (((exists fs_h_ics_add_functional_first_at1. fs_h_ics_add_functional_first_at1 + S (ics_value1_add_functional_first) = S ((S (ics_index_add_functional_first)) * dc)) /\ exists fs_q_ics_add_functional_first_at1. db = fs_q_ics_add_functional_first_at1 * S ((S (ics_index_add_functional_first)) * dc) + (ics_value1_add_functional_first))) -> (((exists fs_h_ics_add_functional_first_at2. fs_h_ics_add_functional_first_at2 + S (ics_value2_add_functional_first) = S ((S (ics_index_add_functional_first)) * ec)) /\ exists fs_q_ics_add_functional_first_at2. eb = fs_q_ics_add_functional_first_at2 * S ((S (ics_index_add_functional_first)) * ec) + (ics_value2_add_functional_first))) -> (((exists fs_h_ics_add_functional_first_at3. fs_h_ics_add_functional_first_at3 + S (ics_value3_add_functional_first) = S ((S (ics_index_add_functional_first)) * fc)) /\ exists fs_q_ics_add_functional_first_at3. fb = fs_q_ics_add_functional_first_at3 * S ((S (ics_index_add_functional_first)) * fc) + (ics_value3_add_functional_first))) -> (((exists fs_h_ics_add_functional_first_at4. fs_h_ics_add_functional_first_at4 + S (ics_value4_add_functional_first) = S ((S (ics_index_add_functional_first)) * pc)) /\ exists fs_q_ics_add_functional_first_at4. pb = fs_q_ics_add_functional_first_at4 * S ((S (ics_index_add_functional_first)) * pc) + (ics_value4_add_functional_first))) -> (((exists fs_h_ics_add_functional_first_at5. fs_h_ics_add_functional_first_at5 + S (ics_value5_add_functional_first) = S ((S (ics_index_add_functional_first)) * nc)) /\ exists fs_q_ics_add_functional_first_at5. nb = fs_q_ics_add_functional_first_at5 * S ((S (ics_index_add_functional_first)) * nc) + (ics_value5_add_functional_first))) -> ics_value4_add_functional_first + (ics_value1_add_functional_first + ics_value3_add_functional_first) = (ics_value0_add_functional_first + ics_value2_add_functional_first) + ics_value5_add_functional_first) -> (forall ics_index_add_functional_second ics_value0_add_functional_second ics_value1_add_functional_second ics_value2_add_functional_second ics_value3_add_functional_second ics_value4_add_functional_second ics_value5_add_functional_second. (exists ics_gap_add_functional_second_bound. ics_gap_add_functional_second_bound + S (ics_index_add_functional_second) = (l)) -> (((exists fs_h_ics_add_functional_second_at0. fs_h_ics_add_functional_second_at0 + S (ics_value0_add_functional_second) = S ((S (ics_index_add_functional_second)) * ac)) /\ exists fs_q_ics_add_functional_second_at0. ab = fs_q_ics_add_functional_second_at0 * S ((S (ics_index_add_functional_second)) * ac) + (ics_value0_add_functional_second))) -> (((exists fs_h_ics_add_functional_second_at1. fs_h_ics_add_functional_second_at1 + S (ics_value1_add_functional_second) = S ((S (ics_index_add_functional_second)) * dc)) /\ exists fs_q_ics_add_functional_second_at1. db = fs_q_ics_add_functional_second_at1 * S ((S (ics_index_add_functional_second)) * dc) + (ics_value1_add_functional_second))) -> (((exists fs_h_ics_add_functional_second_at2. fs_h_ics_add_functional_second_at2 + S (ics_value2_add_functional_second) = S ((S (ics_index_add_functional_second)) * ec)) /\ exists fs_q_ics_add_functional_second_at2. eb = fs_q_ics_add_functional_second_at2 * S ((S (ics_index_add_functional_second)) * ec) + (ics_value2_add_functional_second))) -> (((exists fs_h_ics_add_functional_second_at3. fs_h_ics_add_functional_second_at3 + S (ics_value3_add_functional_second) = S ((S (ics_index_add_functional_second)) * fc)) /\ exists fs_q_ics_add_functional_second_at3. fb = fs_q_ics_add_functional_second_at3 * S ((S (ics_index_add_functional_second)) * fc) + (ics_value3_add_functional_second))) -> (((exists fs_h_ics_add_functional_second_at4. fs_h_ics_add_functional_second_at4 + S (ics_value4_add_functional_second) = S ((S (ics_index_add_functional_second)) * qc)) /\ exists fs_q_ics_add_functional_second_at4. qb = fs_q_ics_add_functional_second_at4 * S ((S (ics_index_add_functional_second)) * qc) + (ics_value4_add_functional_second))) -> (((exists fs_h_ics_add_functional_second_at5. fs_h_ics_add_functional_second_at5 + S (ics_value5_add_functional_second) = S ((S (ics_index_add_functional_second)) * mc)) /\ exists fs_q_ics_add_functional_second_at5. mb = fs_q_ics_add_functional_second_at5 * S ((S (ics_index_add_functional_second)) * mc) + (ics_value5_add_functional_second))) -> ics_value4_add_functional_second + (ics_value1_add_functional_second + ics_value3_add_functional_second) = (ics_value0_add_functional_second + ics_value2_add_functional_second) + ics_value5_add_functional_second) -> (forall ics_index_add_functional_result ics_value0_add_functional_result ics_value1_add_functional_result ics_value2_add_functional_result ics_value3_add_functional_result. (exists ics_gap_add_functional_result_bound. ics_gap_add_functional_result_bound + S (ics_index_add_functional_result) = (l)) -> (((exists fs_h_ics_add_functional_result_at0. fs_h_ics_add_functional_result_at0 + S (ics_value0_add_functional_result) = S ((S (ics_index_add_functional_result)) * pc)) /\ exists fs_q_ics_add_functional_result_at0. pb = fs_q_ics_add_functional_result_at0 * S ((S (ics_index_add_functional_result)) * pc) + (ics_value0_add_functional_result))) -> (((exists fs_h_ics_add_functional_result_at1. fs_h_ics_add_functional_result_at1 + S (ics_value1_add_functional_result) = S ((S (ics_index_add_functional_result)) * nc)) /\ exists fs_q_ics_add_functional_result_at1. nb = fs_q_ics_add_functional_result_at1 * S ((S (ics_index_add_functional_result)) * nc) + (ics_value1_add_functional_result))) -> (((exists fs_h_ics_add_functional_result_at2. fs_h_ics_add_functional_result_at2 + S (ics_value2_add_functional_result) = S ((S (ics_index_add_functional_result)) * qc)) /\ exists fs_q_ics_add_functional_result_at2. qb = fs_q_ics_add_functional_result_at2 * S ((S (ics_index_add_functional_result)) * qc) + (ics_value2_add_functional_result))) -> (((exists fs_h_ics_add_functional_result_at3. fs_h_ics_add_functional_result_at3 + S (ics_value3_add_functional_result) = S ((S (ics_index_add_functional_result)) * mc)) /\ exists fs_q_ics_add_functional_result_at3. mb = fs_q_ics_add_functional_result_at3 * S ((S (ics_index_add_functional_result)) * mc) + (ics_value3_add_functional_result))) -> ics_value0_add_functional_result + ics_value3_add_functional_result = ics_value2_add_functional_result + ics_value1_add_functional_result)

Constructive proof overview

Generated structural guide

Two actual sums of the same signed vectors are equal as integer vectors, without claiming equality of their beta codes or separate components.

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

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

Proof neighborhood

Direct dependencies

beta_at_exists Stable theorem; checked-use authorized DL006C integer_span_pair_equal_transitive eq_symm Stable theorem; checked-use authorized

Direct dependents

DL007C integer_matrix_vector_add_constructive

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

93 script commands · 15 reading checkpoints · 4 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 (1)
integer span pair equal transitive
01Fix variables and assumptionsL1–10

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

  1. L1
    intro ab
  2. L2
    intro ac
  3. L3
    intro db
  4. L4
    intro dc
  5. L5
    intro eb
  6. L6
    intro ec
  7. L7
    intro fb
  8. L8
    intro fc
  9. L9
    intro pb
  10. L10
    intro pc
02Fix variables and assumptionsL11–20

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

  1. L11
    intro nb
  2. L12
    intro nc
  3. L13
    intro qb
  4. L14
    intro qc
  5. L15
    intro mb
  6. L16
    intro mc
  7. L17
    intro l
  8. L18
    intro hfirst
  9. L19
    intro hsecond
  10. L20
    intro i
03Fix variables and assumptionsL21–29

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

  1. L21
    intro a
  2. L22
    intro b
  3. L23
    intro c
  4. L24
    intro d
  5. L25
    intro hi
  6. L26
    intro ha
  7. L27
    intro hb
  8. L28
    intro hc
  9. L29
    intro hd
04Establish hinput0L30–34

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

  1. L30
    have hinput0 : exists value. (((exists fs_h_ics_add_functional_input0. fs_h_ics_add_functional_input0 + S (value) = S ((S (i)) * ac)) /\ exists fs_q_ics_add_functional_input0. ab = fs_q_ics_add_functional_input0 * S ((S (i)) * ac) + (value)))
  2. L31
    specialize beta_at_exists (ab)
  3. L32
    specialize beta_at_exists (ac)
  4. L33
    specialize beta_at_exists (i)
  5. L34
    apply beta_at_exists
05Separate the logical casesL35–35

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

  1. L35
    cases hinput0
06Establish hinput1L36–40

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

  1. L36
    have hinput1 : exists value. (((exists fs_h_ics_add_functional_input1. fs_h_ics_add_functional_input1 + S (value) = S ((S (i)) * dc)) /\ exists fs_q_ics_add_functional_input1. db = fs_q_ics_add_functional_input1 * S ((S (i)) * dc) + (value)))
  2. L37
    specialize beta_at_exists (db)
  3. L38
    specialize beta_at_exists (dc)
  4. L39
    specialize beta_at_exists (i)
  5. L40
    apply beta_at_exists
07Separate the logical casesL41–41

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

  1. L41
    cases hinput1
08Establish hinput2L42–46

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

  1. L42
    have hinput2 : exists value. (((exists fs_h_ics_add_functional_input2. fs_h_ics_add_functional_input2 + S (value) = S ((S (i)) * ec)) /\ exists fs_q_ics_add_functional_input2. eb = fs_q_ics_add_functional_input2 * S ((S (i)) * ec) + (value)))
  2. L43
    specialize beta_at_exists (eb)
  3. L44
    specialize beta_at_exists (ec)
  4. L45
    specialize beta_at_exists (i)
  5. L46
    apply beta_at_exists
09Separate the logical casesL47–47

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

  1. L47
    cases hinput2
10Establish hinput3L48–52

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

  1. L48
    have hinput3 : exists value. (((exists fs_h_ics_add_functional_input3. fs_h_ics_add_functional_input3 + S (value) = S ((S (i)) * fc)) /\ exists fs_q_ics_add_functional_input3. fb = fs_q_ics_add_functional_input3 * S ((S (i)) * fc) + (value)))
  2. L49
    specialize beta_at_exists (fb)
  3. L50
    specialize beta_at_exists (fc)
  4. L51
    specialize beta_at_exists (i)
  5. L52
    apply beta_at_exists
11Separate the logical casesL53–53

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

  1. L53
    cases hinput3
12Use earlier factsL54–63

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

  1. L54
    specialize integer_span_pair_equal_transitive (a)
  2. L55
    specialize integer_span_pair_equal_transitive (b)
  3. L56
    specialize integer_span_pair_equal_transitive (x + x2)
  4. L57
    specialize integer_span_pair_equal_transitive (x1 + x3)
  5. L58
    specialize integer_span_pair_equal_transitive (c)
  6. L59
    specialize integer_span_pair_equal_transitive (d)
  7. L60
    apply integer_span_pair_equal_transitive
  8. L61
    specialize hfirst (i)
  9. L62
    specialize hfirst (x)
  10. L63
    specialize hfirst (x1)
13Use earlier factsL64–73

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

  1. L64
    specialize hfirst (x2)
  2. L65
    specialize hfirst (x3)
  3. L66
    specialize hfirst (a)
  4. L67
    specialize hfirst (b)
  5. L68
    apply hfirst
  6. L69
    exact hi
  7. L70
    exact hinput0_witness
  8. L71
    exact hinput1_witness
  9. L72
    exact hinput2_witness
  10. L73
    exact hinput3_witness
14Use earlier factsL74–83

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

  1. L74
    exact ha
  2. L75
    exact hb
  3. L76
    specialize eq_symm (c + (x1 + x3))
  4. L77
    specialize eq_symm ((x + x2) + d)
  5. L78
    apply eq_symm
  6. L79
    specialize hsecond (i)
  7. L80
    specialize hsecond (x)
  8. L81
    specialize hsecond (x1)
  9. L82
    specialize hsecond (x2)
  10. L83
    specialize hsecond (x3)
15Use earlier factsL84–93

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

  1. L84
    specialize hsecond (c)
  2. L85
    specialize hsecond (d)
  3. L86
    apply hsecond
  4. L87
    exact hi
  5. L88
    exact hinput0_witness
  6. L89
    exact hinput1_witness
  7. L90
    exact hinput2_witness
  8. L91
    exact hinput3_witness
  9. L92
    exact hc
  10. L93
    exact hd

Library-wide reading audit

Original exact command ledger · 93 lines
  1. 0001intro ab
  2. 0002intro ac
  3. 0003intro db
  4. 0004intro dc
  5. 0005intro eb
  6. 0006intro ec
  7. 0007intro fb
  8. 0008intro fc
  9. 0009intro pb
  10. 0010intro pc
  11. 0011intro nb
  12. 0012intro nc
  13. 0013intro qb
  14. 0014intro qc
  15. 0015intro mb
  16. 0016intro mc
  17. 0017intro l
  18. 0018intro hfirst
  19. 0019intro hsecond
  20. 0020intro i
  21. 0021intro a
  22. 0022intro b
  23. 0023intro c
  24. 0024intro d
  25. 0025intro hi
  26. 0026intro ha
  27. 0027intro hb
  28. 0028intro hc
  29. 0029intro hd
  30. 0030have hinput0 : exists value. (((exists fs_h_ics_add_functional_input0. fs_h_ics_add_functional_input0 + S (value) = S ((S (i)) * ac)) /\ exists fs_q_ics_add_functional_input0. ab = fs_q_ics_add_functional_input0 * S ((S (i)) * ac) + (value)))
  31. 0031specialize beta_at_exists (ab)
  32. 0032specialize beta_at_exists (ac)
  33. 0033specialize beta_at_exists (i)
  34. 0034apply beta_at_exists
  35. 0035cases hinput0
  36. 0036have hinput1 : exists value. (((exists fs_h_ics_add_functional_input1. fs_h_ics_add_functional_input1 + S (value) = S ((S (i)) * dc)) /\ exists fs_q_ics_add_functional_input1. db = fs_q_ics_add_functional_input1 * S ((S (i)) * dc) + (value)))
  37. 0037specialize beta_at_exists (db)
  38. 0038specialize beta_at_exists (dc)
  39. 0039specialize beta_at_exists (i)
  40. 0040apply beta_at_exists
  41. 0041cases hinput1
  42. 0042have hinput2 : exists value. (((exists fs_h_ics_add_functional_input2. fs_h_ics_add_functional_input2 + S (value) = S ((S (i)) * ec)) /\ exists fs_q_ics_add_functional_input2. eb = fs_q_ics_add_functional_input2 * S ((S (i)) * ec) + (value)))
  43. 0043specialize beta_at_exists (eb)
  44. 0044specialize beta_at_exists (ec)
  45. 0045specialize beta_at_exists (i)
  46. 0046apply beta_at_exists
  47. 0047cases hinput2
  48. 0048have hinput3 : exists value. (((exists fs_h_ics_add_functional_input3. fs_h_ics_add_functional_input3 + S (value) = S ((S (i)) * fc)) /\ exists fs_q_ics_add_functional_input3. fb = fs_q_ics_add_functional_input3 * S ((S (i)) * fc) + (value)))
  49. 0049specialize beta_at_exists (fb)
  50. 0050specialize beta_at_exists (fc)
  51. 0051specialize beta_at_exists (i)
  52. 0052apply beta_at_exists
  53. 0053cases hinput3
  54. 0054specialize integer_span_pair_equal_transitive (a)
  55. 0055specialize integer_span_pair_equal_transitive (b)
  56. 0056specialize integer_span_pair_equal_transitive (x + x2)
  57. 0057specialize integer_span_pair_equal_transitive (x1 + x3)
  58. 0058specialize integer_span_pair_equal_transitive (c)
  59. 0059specialize integer_span_pair_equal_transitive (d)
  60. 0060apply integer_span_pair_equal_transitive
  61. 0061specialize hfirst (i)
  62. 0062specialize hfirst (x)
  63. 0063specialize hfirst (x1)
  64. 0064specialize hfirst (x2)
  65. 0065specialize hfirst (x3)
  66. 0066specialize hfirst (a)
  67. 0067specialize hfirst (b)
  68. 0068apply hfirst
  69. 0069exact hi
  70. 0070exact hinput0_witness
  71. 0071exact hinput1_witness
  72. 0072exact hinput2_witness
  73. 0073exact hinput3_witness
  74. 0074exact ha
  75. 0075exact hb
  76. 0076specialize eq_symm (c + (x1 + x3))
  77. 0077specialize eq_symm ((x + x2) + d)
  78. 0078apply eq_symm
  79. 0079specialize hsecond (i)
  80. 0080specialize hsecond (x)
  81. 0081specialize hsecond (x1)
  82. 0082specialize hsecond (x2)
  83. 0083specialize hsecond (x3)
  84. 0084specialize hsecond (c)
  85. 0085specialize hsecond (d)
  86. 0086apply hsecond
  87. 0087exact hi
  88. 0088exact hinput0_witness
  89. 0089exact hinput1_witness
  90. 0090exact hinput2_witness
  91. 0091exact hinput3_witness
  92. 0092exact hc
  93. 0093exact hd