DL0074

integer_vector_add_exists

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

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

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.

This branch proves the finite determinant/rank/span substrate. It does not claim Smith or Hermite normal form, lattice index equals determinant, determinant multiplicativity, lattice reduction, or geometry-of-numbers theorems.

Exact theorem in conservative defined notation

∀ ab. ∀ ac. ∀ db. ∀ dc. ∀ eb. ∀ ec. ∀ fb. ∀ fc. ∀ l. ∃ pb. ∃ pc. ∃ nb. ∃ nc. IntegerVectorAdd(ab,ac,db,dc,eb,ec,fb,fc,pb,pc,nb,nc,l)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

MatrixPointwiseAdd(mb,mc,sb,sc,tb,tc,l) · 2IntegerVectorAdd(ab,ac,db,dc,eb,ec,fb,fc,pb,pc,nb,nc,l) · 1

Actual proof prerequisites

beta_pointwise_add_prefix_exists · checked external prerequisiteinteger_vector_add_from_component_sums
Original expanded first-order 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)

Complete tactic proof in conservative notation

All 47 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
integer vector add from component sums
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(ab,ac,eb,ec,b,c,l)Original native command in the exact edition
  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(db,dc,fb,fc,b,c,l)Original native command in the exact edition
  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 defined 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 : ∃ b. ∃ c. MatrixPointwiseAdd(ab,ac,eb,ec,b,c,l)
  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 : ∃ b. ∃ c. MatrixPointwiseAdd(db,dc,fb,fc,b,c,l)
  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