DL006F

integer_vector_equal_transitive

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

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

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 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)

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 66 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

Direct dependents

DL0078 integer_matrix_vector_product_transport

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

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.

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 : exists value. (((exists fs_h_ics_equal_middle_p. fs_h_ics_equal_middle_p + S (value) = S ((S (i)) * ec)) /\ exists fs_q_ics_equal_middle_p. eb = fs_q_ics_equal_middle_p * S ((S (i)) * ec) + (value)))
  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 : exists value. (((exists fs_h_ics_equal_middle_n. fs_h_ics_equal_middle_n + S (value) = S ((S (i)) * fc)) /\ exists fs_q_ics_equal_middle_n. fb = fs_q_ics_equal_middle_n * S ((S (i)) * fc) + (value)))
  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 exact 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 : exists value. (((exists fs_h_ics_equal_middle_p. fs_h_ics_equal_middle_p + S (value) = S ((S (i)) * ec)) /\ exists fs_q_ics_equal_middle_p. eb = fs_q_ics_equal_middle_p * S ((S (i)) * ec) + (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 : exists value. (((exists fs_h_ics_equal_middle_n. fs_h_ics_equal_middle_n + S (value) = S ((S (i)) * fc)) /\ exists fs_q_ics_equal_middle_n. fb = fs_q_ics_equal_middle_n * S ((S (i)) * fc) + (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