DL0074

integer_vector_add_exists

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

Every two finite signed vectors have a constructively produced coded integer sum, including the empty vector.

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 l. exists pb pc nb nc. (forall ics_index_vector_add_exists ics_value0_vector_add_exists ics_value1_vector_add_exists ics_value2_vector_add_exists ics_value3_vector_add_exists ics_value4_vector_add_exists ics_value5_vector_add_exists. (exists ics_gap_vector_add_exists_bound. ics_gap_vector_add_exists_bound + S (ics_index_vector_add_exists) = (l)) -> (((exists fs_h_ics_vector_add_exists_at0. fs_h_ics_vector_add_exists_at0 + S (ics_value0_vector_add_exists) = S ((S (ics_index_vector_add_exists)) * ac)) /\ exists fs_q_ics_vector_add_exists_at0. ab = fs_q_ics_vector_add_exists_at0 * S ((S (ics_index_vector_add_exists)) * ac) + (ics_value0_vector_add_exists))) -> (((exists fs_h_ics_vector_add_exists_at1. fs_h_ics_vector_add_exists_at1 + S (ics_value1_vector_add_exists) = S ((S (ics_index_vector_add_exists)) * dc)) /\ exists fs_q_ics_vector_add_exists_at1. db = fs_q_ics_vector_add_exists_at1 * S ((S (ics_index_vector_add_exists)) * dc) + (ics_value1_vector_add_exists))) -> (((exists fs_h_ics_vector_add_exists_at2. fs_h_ics_vector_add_exists_at2 + S (ics_value2_vector_add_exists) = S ((S (ics_index_vector_add_exists)) * ec)) /\ exists fs_q_ics_vector_add_exists_at2. eb = fs_q_ics_vector_add_exists_at2 * S ((S (ics_index_vector_add_exists)) * ec) + (ics_value2_vector_add_exists))) -> (((exists fs_h_ics_vector_add_exists_at3. fs_h_ics_vector_add_exists_at3 + S (ics_value3_vector_add_exists) = S ((S (ics_index_vector_add_exists)) * fc)) /\ exists fs_q_ics_vector_add_exists_at3. fb = fs_q_ics_vector_add_exists_at3 * S ((S (ics_index_vector_add_exists)) * fc) + (ics_value3_vector_add_exists))) -> (((exists fs_h_ics_vector_add_exists_at4. fs_h_ics_vector_add_exists_at4 + S (ics_value4_vector_add_exists) = S ((S (ics_index_vector_add_exists)) * pc)) /\ exists fs_q_ics_vector_add_exists_at4. pb = fs_q_ics_vector_add_exists_at4 * S ((S (ics_index_vector_add_exists)) * pc) + (ics_value4_vector_add_exists))) -> (((exists fs_h_ics_vector_add_exists_at5. fs_h_ics_vector_add_exists_at5 + S (ics_value5_vector_add_exists) = S ((S (ics_index_vector_add_exists)) * nc)) /\ exists fs_q_ics_vector_add_exists_at5. nb = fs_q_ics_vector_add_exists_at5 * S ((S (ics_index_vector_add_exists)) * nc) + (ics_value5_vector_add_exists))) -> ics_value4_vector_add_exists + (ics_value1_vector_add_exists + ics_value3_vector_add_exists) = (ics_value0_vector_add_exists + ics_value2_vector_add_exists) + ics_value5_vector_add_exists)

Constructive proof overview

Generated structural guide

Every two finite signed vectors have a constructively produced coded integer sum, including the empty vector.

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

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

Proof neighborhood

Direct dependencies

beta_pointwise_add_prefix_exists Alpha theorem; checked-use authorized DL0073 integer_vector_add_from_component_sums

Direct dependents

DL0083 integer_column_span_add_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

47 script commands · 8 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.

Named ingredients (1)
integer vector add from component sums

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

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 l
02Establish hpL10–16

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

  1. L10
    have hp : ∃ b. ∃ c. MatrixPointwiseAdd(ab,ac,eb,ec,b,c,l)Definitions: MatrixPointwiseAdd
  2. L11
    specialize beta_pointwise_add_prefix_exists (ab)
  3. L12
    specialize beta_pointwise_add_prefix_exists (ac)
  4. L13
    specialize beta_pointwise_add_prefix_exists (eb)
  5. L14
    specialize beta_pointwise_add_prefix_exists (ec)
  6. L15
    specialize beta_pointwise_add_prefix_exists (l)
  7. L16
    apply beta_pointwise_add_prefix_exists
03Separate the logical casesL17–18

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

  1. L17
    cases hp
  2. L18
    cases hp_witness
04Establish hnL19–25

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

  1. L19
    have hn : ∃ b. ∃ c. MatrixPointwiseAdd(db,dc,fb,fc,b,c,l)Definitions: MatrixPointwiseAdd
  2. L20
    specialize beta_pointwise_add_prefix_exists (db)
  3. L21
    specialize beta_pointwise_add_prefix_exists (dc)
  4. L22
    specialize beta_pointwise_add_prefix_exists (fb)
  5. L23
    specialize beta_pointwise_add_prefix_exists (fc)
  6. L24
    specialize beta_pointwise_add_prefix_exists (l)
  7. L25
    apply beta_pointwise_add_prefix_exists
05Separate the logical casesL26–27

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

  1. L26
    cases hn
  2. L27
    cases hn_witness
06Construct an explicit witnessL28–31

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

  1. L28
    exists x
  2. L29
    exists x1
  3. L30
    exists x2
  4. L31
    exists x3
07Use earlier factsL32–41

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

  1. L32
    specialize integer_vector_add_from_component_sums (ab)
  2. L33
    specialize integer_vector_add_from_component_sums (ac)
  3. L34
    specialize integer_vector_add_from_component_sums (db)
  4. L35
    specialize integer_vector_add_from_component_sums (dc)
  5. L36
    specialize integer_vector_add_from_component_sums (eb)
  6. L37
    specialize integer_vector_add_from_component_sums (ec)
  7. L38
    specialize integer_vector_add_from_component_sums (fb)
  8. L39
    specialize integer_vector_add_from_component_sums (fc)
  9. L40
    specialize integer_vector_add_from_component_sums (x)
  10. L41
    specialize integer_vector_add_from_component_sums (x1)
08Use earlier factsL42–47

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

  1. L42
    specialize integer_vector_add_from_component_sums (x2)
  2. L43
    specialize integer_vector_add_from_component_sums (x3)
  3. L44
    specialize integer_vector_add_from_component_sums (l)
  4. L45
    apply integer_vector_add_from_component_sums
  5. L46
    exact hp_witness_witness
  6. L47
    exact hn_witness_witness

Library-wide reading audit

Original exact command ledger · 47 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 l
  10. 0010have hp : exists b c. (forall ff_index_mcp_add_ics_vector_add_exists_p ff_left_mcp_add_ics_vector_add_exists_p ff_right_mcp_add_ics_vector_add_exists_p ff_target_mcp_add_ics_vector_add_exists_p. (exists mcp_gap_ics_vector_add_exists_p_bound. mcp_gap_ics_vector_add_exists_p_bound + S (ff_index_mcp_add_ics_vector_add_exists_p) = (l)) -> (((exists fs_h_mcp_ics_vector_add_exists_p_left. fs_h_mcp_ics_vector_add_exists_p_left + S (ff_left_mcp_add_ics_vector_add_exists_p) = S ((S (ff_index_mcp_add_ics_vector_add_exists_p)) * ac)) /\ exists fs_q_mcp_ics_vector_add_exists_p_left. ab = fs_q_mcp_ics_vector_add_exists_p_left * S ((S (ff_index_mcp_add_ics_vector_add_exists_p)) * ac) + (ff_left_mcp_add_ics_vector_add_exists_p))) -> (((exists fs_h_mcp_ics_vector_add_exists_p_right. fs_h_mcp_ics_vector_add_exists_p_right + S (ff_right_mcp_add_ics_vector_add_exists_p) = S ((S (ff_index_mcp_add_ics_vector_add_exists_p)) * ec)) /\ exists fs_q_mcp_ics_vector_add_exists_p_right. eb = fs_q_mcp_ics_vector_add_exists_p_right * S ((S (ff_index_mcp_add_ics_vector_add_exists_p)) * ec) + (ff_right_mcp_add_ics_vector_add_exists_p))) -> (((exists fs_h_mcp_ics_vector_add_exists_p_target. fs_h_mcp_ics_vector_add_exists_p_target + S (ff_target_mcp_add_ics_vector_add_exists_p) = S ((S (ff_index_mcp_add_ics_vector_add_exists_p)) * c)) /\ exists fs_q_mcp_ics_vector_add_exists_p_target. b = fs_q_mcp_ics_vector_add_exists_p_target * S ((S (ff_index_mcp_add_ics_vector_add_exists_p)) * c) + (ff_target_mcp_add_ics_vector_add_exists_p))) -> ff_target_mcp_add_ics_vector_add_exists_p = ff_left_mcp_add_ics_vector_add_exists_p + ff_right_mcp_add_ics_vector_add_exists_p)
  11. 0011specialize beta_pointwise_add_prefix_exists (ab)
  12. 0012specialize beta_pointwise_add_prefix_exists (ac)
  13. 0013specialize beta_pointwise_add_prefix_exists (eb)
  14. 0014specialize beta_pointwise_add_prefix_exists (ec)
  15. 0015specialize beta_pointwise_add_prefix_exists (l)
  16. 0016apply beta_pointwise_add_prefix_exists
  17. 0017cases hp
  18. 0018cases hp_witness
  19. 0019have hn : exists b c. (forall ff_index_mcp_add_ics_vector_add_exists_n ff_left_mcp_add_ics_vector_add_exists_n ff_right_mcp_add_ics_vector_add_exists_n ff_target_mcp_add_ics_vector_add_exists_n. (exists mcp_gap_ics_vector_add_exists_n_bound. mcp_gap_ics_vector_add_exists_n_bound + S (ff_index_mcp_add_ics_vector_add_exists_n) = (l)) -> (((exists fs_h_mcp_ics_vector_add_exists_n_left. fs_h_mcp_ics_vector_add_exists_n_left + S (ff_left_mcp_add_ics_vector_add_exists_n) = S ((S (ff_index_mcp_add_ics_vector_add_exists_n)) * dc)) /\ exists fs_q_mcp_ics_vector_add_exists_n_left. db = fs_q_mcp_ics_vector_add_exists_n_left * S ((S (ff_index_mcp_add_ics_vector_add_exists_n)) * dc) + (ff_left_mcp_add_ics_vector_add_exists_n))) -> (((exists fs_h_mcp_ics_vector_add_exists_n_right. fs_h_mcp_ics_vector_add_exists_n_right + S (ff_right_mcp_add_ics_vector_add_exists_n) = S ((S (ff_index_mcp_add_ics_vector_add_exists_n)) * fc)) /\ exists fs_q_mcp_ics_vector_add_exists_n_right. fb = fs_q_mcp_ics_vector_add_exists_n_right * S ((S (ff_index_mcp_add_ics_vector_add_exists_n)) * fc) + (ff_right_mcp_add_ics_vector_add_exists_n))) -> (((exists fs_h_mcp_ics_vector_add_exists_n_target. fs_h_mcp_ics_vector_add_exists_n_target + S (ff_target_mcp_add_ics_vector_add_exists_n) = S ((S (ff_index_mcp_add_ics_vector_add_exists_n)) * c)) /\ exists fs_q_mcp_ics_vector_add_exists_n_target. b = fs_q_mcp_ics_vector_add_exists_n_target * S ((S (ff_index_mcp_add_ics_vector_add_exists_n)) * c) + (ff_target_mcp_add_ics_vector_add_exists_n))) -> ff_target_mcp_add_ics_vector_add_exists_n = ff_left_mcp_add_ics_vector_add_exists_n + ff_right_mcp_add_ics_vector_add_exists_n)
  20. 0020specialize beta_pointwise_add_prefix_exists (db)
  21. 0021specialize beta_pointwise_add_prefix_exists (dc)
  22. 0022specialize beta_pointwise_add_prefix_exists (fb)
  23. 0023specialize beta_pointwise_add_prefix_exists (fc)
  24. 0024specialize beta_pointwise_add_prefix_exists (l)
  25. 0025apply beta_pointwise_add_prefix_exists
  26. 0026cases hn
  27. 0027cases hn_witness
  28. 0028exists x
  29. 0029exists x1
  30. 0030exists x2
  31. 0031exists x3
  32. 0032specialize integer_vector_add_from_component_sums (ab)
  33. 0033specialize integer_vector_add_from_component_sums (ac)
  34. 0034specialize integer_vector_add_from_component_sums (db)
  35. 0035specialize integer_vector_add_from_component_sums (dc)
  36. 0036specialize integer_vector_add_from_component_sums (eb)
  37. 0037specialize integer_vector_add_from_component_sums (ec)
  38. 0038specialize integer_vector_add_from_component_sums (fb)
  39. 0039specialize integer_vector_add_from_component_sums (fc)
  40. 0040specialize integer_vector_add_from_component_sums (x)
  41. 0041specialize integer_vector_add_from_component_sums (x1)
  42. 0042specialize integer_vector_add_from_component_sums (x2)
  43. 0043specialize integer_vector_add_from_component_sums (x3)
  44. 0044specialize integer_vector_add_from_component_sums (l)
  45. 0045apply integer_vector_add_from_component_sums
  46. 0046exact hp_witness_witness
  47. 0047exact hn_witness_witness