DL0070

integer_vector_equal_negated

Swapping positive and negative components preserves actual integer-vector equality, independently of the chosen pair representatives.

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. IntegerVectorEqual(ab,ac,db,dc,eb,ec,fb,fc,l) → IntegerVectorEqual(db,dc,ab,ac,fb,fc,eb,ec,l)

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

Definition DAG

IntegerVectorEqual(ab,ac,db,dc,eb,ec,fb,fc,l) · 2

Actual proof prerequisites

add_comm · checked external prerequisiteeq_symm · checked external prerequisite
Original expanded first-order statement 
forall ab ac db dc eb ec fb fc l. (forall ics_index_equal_neg_source ics_value0_equal_neg_source ics_value1_equal_neg_source ics_value2_equal_neg_source ics_value3_equal_neg_source. (exists ics_gap_equal_neg_source_bound. ics_gap_equal_neg_source_bound + S (ics_index_equal_neg_source) = (l)) -> (((exists fs_h_ics_equal_neg_source_at0. fs_h_ics_equal_neg_source_at0 + S (ics_value0_equal_neg_source) = S ((S (ics_index_equal_neg_source)) * ac)) /\ exists fs_q_ics_equal_neg_source_at0. ab = fs_q_ics_equal_neg_source_at0 * S ((S (ics_index_equal_neg_source)) * ac) + (ics_value0_equal_neg_source))) -> (((exists fs_h_ics_equal_neg_source_at1. fs_h_ics_equal_neg_source_at1 + S (ics_value1_equal_neg_source) = S ((S (ics_index_equal_neg_source)) * dc)) /\ exists fs_q_ics_equal_neg_source_at1. db = fs_q_ics_equal_neg_source_at1 * S ((S (ics_index_equal_neg_source)) * dc) + (ics_value1_equal_neg_source))) -> (((exists fs_h_ics_equal_neg_source_at2. fs_h_ics_equal_neg_source_at2 + S (ics_value2_equal_neg_source) = S ((S (ics_index_equal_neg_source)) * ec)) /\ exists fs_q_ics_equal_neg_source_at2. eb = fs_q_ics_equal_neg_source_at2 * S ((S (ics_index_equal_neg_source)) * ec) + (ics_value2_equal_neg_source))) -> (((exists fs_h_ics_equal_neg_source_at3. fs_h_ics_equal_neg_source_at3 + S (ics_value3_equal_neg_source) = S ((S (ics_index_equal_neg_source)) * fc)) /\ exists fs_q_ics_equal_neg_source_at3. fb = fs_q_ics_equal_neg_source_at3 * S ((S (ics_index_equal_neg_source)) * fc) + (ics_value3_equal_neg_source))) -> ics_value0_equal_neg_source + ics_value3_equal_neg_source = ics_value2_equal_neg_source + ics_value1_equal_neg_source) -> (forall ics_index_equal_neg_result ics_value0_equal_neg_result ics_value1_equal_neg_result ics_value2_equal_neg_result ics_value3_equal_neg_result. (exists ics_gap_equal_neg_result_bound. ics_gap_equal_neg_result_bound + S (ics_index_equal_neg_result) = (l)) -> (((exists fs_h_ics_equal_neg_result_at0. fs_h_ics_equal_neg_result_at0 + S (ics_value0_equal_neg_result) = S ((S (ics_index_equal_neg_result)) * dc)) /\ exists fs_q_ics_equal_neg_result_at0. db = fs_q_ics_equal_neg_result_at0 * S ((S (ics_index_equal_neg_result)) * dc) + (ics_value0_equal_neg_result))) -> (((exists fs_h_ics_equal_neg_result_at1. fs_h_ics_equal_neg_result_at1 + S (ics_value1_equal_neg_result) = S ((S (ics_index_equal_neg_result)) * ac)) /\ exists fs_q_ics_equal_neg_result_at1. ab = fs_q_ics_equal_neg_result_at1 * S ((S (ics_index_equal_neg_result)) * ac) + (ics_value1_equal_neg_result))) -> (((exists fs_h_ics_equal_neg_result_at2. fs_h_ics_equal_neg_result_at2 + S (ics_value2_equal_neg_result) = S ((S (ics_index_equal_neg_result)) * fc)) /\ exists fs_q_ics_equal_neg_result_at2. fb = fs_q_ics_equal_neg_result_at2 * S ((S (ics_index_equal_neg_result)) * fc) + (ics_value2_equal_neg_result))) -> (((exists fs_h_ics_equal_neg_result_at3. fs_h_ics_equal_neg_result_at3 + S (ics_value3_equal_neg_result) = S ((S (ics_index_equal_neg_result)) * ec)) /\ exists fs_q_ics_equal_neg_result_at3. eb = fs_q_ics_equal_neg_result_at3 * S ((S (ics_index_equal_neg_result)) * ec) + (ics_value3_equal_neg_result))) -> ics_value0_equal_neg_result + ics_value3_equal_neg_result = ics_value2_equal_neg_result + ics_value1_equal_neg_result)

Complete tactic proof in conservative notation

All 40 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

40 script commands · 8 reading checkpoints · 1 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.

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 l
  10. L10
    intro hequal
02Fix variables and assumptionsL11–20

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

  1. L11
    intro i
  2. L12
    intro a
  3. L13
    intro b
  4. L14
    intro c
  5. L15
    intro d
  6. L16
    intro hi
  7. L17
    intro ha
  8. L18
    intro hb
  9. L19
    intro hc
  10. L20
    intro hd
03Establish hsourceL21–30

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

  1. L21
    have hsource : b + c = d + a
  2. L22
    specialize hequal (i)
  3. L23
    specialize hequal (b)
  4. L24
    specialize hequal (a)
  5. L25
    specialize hequal (d)
  6. L26
    specialize hequal (c)
  7. L27
    apply hequal
  8. L28
    exact hi
  9. L29
    exact hb
  10. L30
    exact ha
04Use earlier factsL31–32

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

  1. L31
    exact hd
  2. L32
    exact hc
05Calculate and transport equalitiesL33–33

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

  1. L33
    trans d + a
06Use earlier factsL34–34

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

  1. L34
    apply add_comm
07Calculate and transport equalitiesL35–35

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

  1. L35
    trans b + c
08Use earlier factsL36–40

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

  1. L36
    specialize eq_symm (b + c)
  2. L37
    specialize eq_symm (d + a)
  3. L38
    apply eq_symm
  4. L39
    exact hsource
  5. L40
    apply add_comm

Library-wide reading audit

Original defined command ledger · 40 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. 0010intro hequal
  11. 0011intro i
  12. 0012intro a
  13. 0013intro b
  14. 0014intro c
  15. 0015intro d
  16. 0016intro hi
  17. 0017intro ha
  18. 0018intro hb
  19. 0019intro hc
  20. 0020intro hd
  21. 0021have hsource : b + c = d + a
  22. 0022specialize hequal (i)
  23. 0023specialize hequal (b)
  24. 0024specialize hequal (a)
  25. 0025specialize hequal (d)
  26. 0026specialize hequal (c)
  27. 0027apply hequal
  28. 0028exact hi
  29. 0029exact hb
  30. 0030exact ha
  31. 0031exact hd
  32. 0032exact hc
  33. 0033trans d + a
  34. 0034apply add_comm
  35. 0035trans b + c
  36. 0036specialize eq_symm (b + c)
  37. 0037specialize eq_symm (d + a)
  38. 0038apply eq_symm
  39. 0039exact hsource
  40. 0040apply add_comm