DL006F

integer_vector_equal_transitive

Integer-vector equality is genuinely transitive across independently coded, noncanonical intermediate signed entries.

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

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

Definition DAG

IntegerVectorEqual(ab,ac,db,dc,eb,ec,fb,fc,l) · 3BetaAt(b,c,i,x) · 2

Actual proof prerequisites

beta_at_exists · checked external prerequisiteinteger_span_pair_equal_transitive
Original expanded first-order statement 
forall ab ac db dc eb ec fb fc pb pc nb nc l. (forall ics_index_equal_trans_first ics_value0_equal_trans_first ics_value1_equal_trans_first ics_value2_equal_trans_first ics_value3_equal_trans_first. (exists ics_gap_equal_trans_first_bound. ics_gap_equal_trans_first_bound + S (ics_index_equal_trans_first) = (l)) -> (((exists fs_h_ics_equal_trans_first_at0. fs_h_ics_equal_trans_first_at0 + S (ics_value0_equal_trans_first) = S ((S (ics_index_equal_trans_first)) * ac)) /\ exists fs_q_ics_equal_trans_first_at0. ab = fs_q_ics_equal_trans_first_at0 * S ((S (ics_index_equal_trans_first)) * ac) + (ics_value0_equal_trans_first))) -> (((exists fs_h_ics_equal_trans_first_at1. fs_h_ics_equal_trans_first_at1 + S (ics_value1_equal_trans_first) = S ((S (ics_index_equal_trans_first)) * dc)) /\ exists fs_q_ics_equal_trans_first_at1. db = fs_q_ics_equal_trans_first_at1 * S ((S (ics_index_equal_trans_first)) * dc) + (ics_value1_equal_trans_first))) -> (((exists fs_h_ics_equal_trans_first_at2. fs_h_ics_equal_trans_first_at2 + S (ics_value2_equal_trans_first) = S ((S (ics_index_equal_trans_first)) * ec)) /\ exists fs_q_ics_equal_trans_first_at2. eb = fs_q_ics_equal_trans_first_at2 * S ((S (ics_index_equal_trans_first)) * ec) + (ics_value2_equal_trans_first))) -> (((exists fs_h_ics_equal_trans_first_at3. fs_h_ics_equal_trans_first_at3 + S (ics_value3_equal_trans_first) = S ((S (ics_index_equal_trans_first)) * fc)) /\ exists fs_q_ics_equal_trans_first_at3. fb = fs_q_ics_equal_trans_first_at3 * S ((S (ics_index_equal_trans_first)) * fc) + (ics_value3_equal_trans_first))) -> ics_value0_equal_trans_first + ics_value3_equal_trans_first = ics_value2_equal_trans_first + ics_value1_equal_trans_first) -> (forall ics_index_equal_trans_second ics_value0_equal_trans_second ics_value1_equal_trans_second ics_value2_equal_trans_second ics_value3_equal_trans_second. (exists ics_gap_equal_trans_second_bound. ics_gap_equal_trans_second_bound + S (ics_index_equal_trans_second) = (l)) -> (((exists fs_h_ics_equal_trans_second_at0. fs_h_ics_equal_trans_second_at0 + S (ics_value0_equal_trans_second) = S ((S (ics_index_equal_trans_second)) * ec)) /\ exists fs_q_ics_equal_trans_second_at0. eb = fs_q_ics_equal_trans_second_at0 * S ((S (ics_index_equal_trans_second)) * ec) + (ics_value0_equal_trans_second))) -> (((exists fs_h_ics_equal_trans_second_at1. fs_h_ics_equal_trans_second_at1 + S (ics_value1_equal_trans_second) = S ((S (ics_index_equal_trans_second)) * fc)) /\ exists fs_q_ics_equal_trans_second_at1. fb = fs_q_ics_equal_trans_second_at1 * S ((S (ics_index_equal_trans_second)) * fc) + (ics_value1_equal_trans_second))) -> (((exists fs_h_ics_equal_trans_second_at2. fs_h_ics_equal_trans_second_at2 + S (ics_value2_equal_trans_second) = S ((S (ics_index_equal_trans_second)) * pc)) /\ exists fs_q_ics_equal_trans_second_at2. pb = fs_q_ics_equal_trans_second_at2 * S ((S (ics_index_equal_trans_second)) * pc) + (ics_value2_equal_trans_second))) -> (((exists fs_h_ics_equal_trans_second_at3. fs_h_ics_equal_trans_second_at3 + S (ics_value3_equal_trans_second) = S ((S (ics_index_equal_trans_second)) * nc)) /\ exists fs_q_ics_equal_trans_second_at3. nb = fs_q_ics_equal_trans_second_at3 * S ((S (ics_index_equal_trans_second)) * nc) + (ics_value3_equal_trans_second))) -> ics_value0_equal_trans_second + ics_value3_equal_trans_second = ics_value2_equal_trans_second + ics_value1_equal_trans_second) -> (forall ics_index_equal_trans_result ics_value0_equal_trans_result ics_value1_equal_trans_result ics_value2_equal_trans_result ics_value3_equal_trans_result. (exists ics_gap_equal_trans_result_bound. ics_gap_equal_trans_result_bound + S (ics_index_equal_trans_result) = (l)) -> (((exists fs_h_ics_equal_trans_result_at0. fs_h_ics_equal_trans_result_at0 + S (ics_value0_equal_trans_result) = S ((S (ics_index_equal_trans_result)) * ac)) /\ exists fs_q_ics_equal_trans_result_at0. ab = fs_q_ics_equal_trans_result_at0 * S ((S (ics_index_equal_trans_result)) * ac) + (ics_value0_equal_trans_result))) -> (((exists fs_h_ics_equal_trans_result_at1. fs_h_ics_equal_trans_result_at1 + S (ics_value1_equal_trans_result) = S ((S (ics_index_equal_trans_result)) * dc)) /\ exists fs_q_ics_equal_trans_result_at1. db = fs_q_ics_equal_trans_result_at1 * S ((S (ics_index_equal_trans_result)) * dc) + (ics_value1_equal_trans_result))) -> (((exists fs_h_ics_equal_trans_result_at2. fs_h_ics_equal_trans_result_at2 + S (ics_value2_equal_trans_result) = S ((S (ics_index_equal_trans_result)) * pc)) /\ exists fs_q_ics_equal_trans_result_at2. pb = fs_q_ics_equal_trans_result_at2 * S ((S (ics_index_equal_trans_result)) * pc) + (ics_value2_equal_trans_result))) -> (((exists fs_h_ics_equal_trans_result_at3. fs_h_ics_equal_trans_result_at3 + S (ics_value3_equal_trans_result) = S ((S (ics_index_equal_trans_result)) * nc)) /\ exists fs_q_ics_equal_trans_result_at3. nb = fs_q_ics_equal_trans_result_at3 * S ((S (ics_index_equal_trans_result)) * nc) + (ics_value3_equal_trans_result))) -> ics_value0_equal_trans_result + ics_value3_equal_trans_result = ics_value2_equal_trans_result + ics_value1_equal_trans_result)

Complete tactic proof in conservative notation

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

66 script commands · 10 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 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 l
  4. L14
    intro hfirst
  5. L15
    intro hsecond
  6. L16
    intro i
  7. L17
    intro a
  8. L18
    intro b
  9. L19
    intro e
  10. L20
    intro f
03Fix variables and assumptionsL21–25

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

  1. L21
    intro hi
  2. L22
    intro ha
  3. L23
    intro hb
  4. L24
    intro he
  5. L25
    intro hf
04Establish hmiddlepL26–30

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

  1. L26
    have hmiddlep : ∃ value. BetaAt(eb,ec,i,value)Definitions: BetaAt(eb,ec,i,value)Original native command in the exact edition
  2. L27
    specialize beta_at_exists (eb)
  3. L28
    specialize beta_at_exists (ec)
  4. L29
    specialize beta_at_exists (i)
  5. L30
    apply beta_at_exists
05Separate the logical casesL31–31

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

  1. L31
    cases hmiddlep
06Establish hmiddlenL32–36

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

  1. L32
    have hmiddlen : ∃ value. BetaAt(fb,fc,i,value)Definitions: BetaAt(fb,fc,i,value)Original native command in the exact edition
  2. L33
    specialize beta_at_exists (fb)
  3. L34
    specialize beta_at_exists (fc)
  4. L35
    specialize beta_at_exists (i)
  5. L36
    apply beta_at_exists
07Separate the logical casesL37–37

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

  1. L37
    cases hmiddlen
08Use earlier factsL38–47

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

  1. L38
    specialize integer_span_pair_equal_transitive (a)
  2. L39
    specialize integer_span_pair_equal_transitive (b)
  3. L40
    specialize integer_span_pair_equal_transitive (x)
  4. L41
    specialize integer_span_pair_equal_transitive (x1)
  5. L42
    specialize integer_span_pair_equal_transitive (e)
  6. L43
    specialize integer_span_pair_equal_transitive (f)
  7. L44
    apply integer_span_pair_equal_transitive
  8. L45
    specialize hfirst (i)
  9. L46
    specialize hfirst (a)
  10. L47
    specialize hfirst (b)
09Use earlier factsL48–57

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

  1. L48
    specialize hfirst (x)
  2. L49
    specialize hfirst (x1)
  3. L50
    apply hfirst
  4. L51
    exact hi
  5. L52
    exact ha
  6. L53
    exact hb
  7. L54
    exact hmiddlep_witness
  8. L55
    exact hmiddlen_witness
  9. L56
    specialize hsecond (i)
  10. L57
    specialize hsecond (x)
10Use earlier factsL58–66

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

  1. L58
    specialize hsecond (x1)
  2. L59
    specialize hsecond (e)
  3. L60
    specialize hsecond (f)
  4. L61
    apply hsecond
  5. L62
    exact hi
  6. L63
    exact hmiddlep_witness
  7. L64
    exact hmiddlen_witness
  8. L65
    exact he
  9. L66
    exact hf

Library-wide reading audit

Original defined command ledger · 66 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 l
  14. 0014intro hfirst
  15. 0015intro hsecond
  16. 0016intro i
  17. 0017intro a
  18. 0018intro b
  19. 0019intro e
  20. 0020intro f
  21. 0021intro hi
  22. 0022intro ha
  23. 0023intro hb
  24. 0024intro he
  25. 0025intro hf
  26. 0026have hmiddlep : ∃ value. BetaAt(eb,ec,i,value)
  27. 0027specialize beta_at_exists (eb)
  28. 0028specialize beta_at_exists (ec)
  29. 0029specialize beta_at_exists (i)
  30. 0030apply beta_at_exists
  31. 0031cases hmiddlep
  32. 0032have hmiddlen : ∃ value. BetaAt(fb,fc,i,value)
  33. 0033specialize beta_at_exists (fb)
  34. 0034specialize beta_at_exists (fc)
  35. 0035specialize beta_at_exists (i)
  36. 0036apply beta_at_exists
  37. 0037cases hmiddlen
  38. 0038specialize integer_span_pair_equal_transitive (a)
  39. 0039specialize integer_span_pair_equal_transitive (b)
  40. 0040specialize integer_span_pair_equal_transitive (x)
  41. 0041specialize integer_span_pair_equal_transitive (x1)
  42. 0042specialize integer_span_pair_equal_transitive (e)
  43. 0043specialize integer_span_pair_equal_transitive (f)
  44. 0044apply integer_span_pair_equal_transitive
  45. 0045specialize hfirst (i)
  46. 0046specialize hfirst (a)
  47. 0047specialize hfirst (b)
  48. 0048specialize hfirst (x)
  49. 0049specialize hfirst (x1)
  50. 0050apply hfirst
  51. 0051exact hi
  52. 0052exact ha
  53. 0053exact hb
  54. 0054exact hmiddlep_witness
  55. 0055exact hmiddlen_witness
  56. 0056specialize hsecond (i)
  57. 0057specialize hsecond (x)
  58. 0058specialize hsecond (x1)
  59. 0059specialize hsecond (e)
  60. 0060specialize hsecond (f)
  61. 0061apply hsecond
  62. 0062exact hi
  63. 0063exact hmiddlep_witness
  64. 0064exact hmiddlen_witness
  65. 0065exact he
  66. 0066exact hf