DL0085

matrix_integer_vector_equality_restrict

Actual signed-integer equality restricts to every smaller finite prefix, without requiring equality of positive or negative components.

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. ∀ bb. ∀ bc. ∀ eb. ∀ ec. ∀ fb. ∀ fc. ∀ L. ∀ K. Le(K,L) → IntegerVectorEqual(ab,ac,bb,bc,eb,ec,fb,fc,L) → IntegerVectorEqual(ab,ac,bb,bc,eb,ec,fb,fc,K)

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

Definition DAG

IntegerVectorEqual(ab,ac,db,dc,eb,ec,fb,fc,l) · 2Le(a,b) · 1

Actual proof prerequisites

lt_of_lt_of_le · checked external prerequisite
Original expanded first-order statement 
forall ab ac bb bc eb ec fb fc L K. (exists mdr_gap_restriction_bound. mdr_gap_restriction_bound + (K) = (L)) -> (forall ics_index_equality_full ics_value0_equality_full ics_value1_equality_full ics_value2_equality_full ics_value3_equality_full. (exists ics_gap_equality_full_bound. ics_gap_equality_full_bound + S (ics_index_equality_full) = (L)) -> (((exists fs_h_ics_equality_full_at0. fs_h_ics_equality_full_at0 + S (ics_value0_equality_full) = S ((S (ics_index_equality_full)) * ac)) /\ exists fs_q_ics_equality_full_at0. ab = fs_q_ics_equality_full_at0 * S ((S (ics_index_equality_full)) * ac) + (ics_value0_equality_full))) -> (((exists fs_h_ics_equality_full_at1. fs_h_ics_equality_full_at1 + S (ics_value1_equality_full) = S ((S (ics_index_equality_full)) * bc)) /\ exists fs_q_ics_equality_full_at1. bb = fs_q_ics_equality_full_at1 * S ((S (ics_index_equality_full)) * bc) + (ics_value1_equality_full))) -> (((exists fs_h_ics_equality_full_at2. fs_h_ics_equality_full_at2 + S (ics_value2_equality_full) = S ((S (ics_index_equality_full)) * ec)) /\ exists fs_q_ics_equality_full_at2. eb = fs_q_ics_equality_full_at2 * S ((S (ics_index_equality_full)) * ec) + (ics_value2_equality_full))) -> (((exists fs_h_ics_equality_full_at3. fs_h_ics_equality_full_at3 + S (ics_value3_equality_full) = S ((S (ics_index_equality_full)) * fc)) /\ exists fs_q_ics_equality_full_at3. fb = fs_q_ics_equality_full_at3 * S ((S (ics_index_equality_full)) * fc) + (ics_value3_equality_full))) -> ics_value0_equality_full + ics_value3_equality_full = ics_value2_equality_full + ics_value1_equality_full) -> (forall ics_index_equality_prefix ics_value0_equality_prefix ics_value1_equality_prefix ics_value2_equality_prefix ics_value3_equality_prefix. (exists ics_gap_equality_prefix_bound. ics_gap_equality_prefix_bound + S (ics_index_equality_prefix) = (K)) -> (((exists fs_h_ics_equality_prefix_at0. fs_h_ics_equality_prefix_at0 + S (ics_value0_equality_prefix) = S ((S (ics_index_equality_prefix)) * ac)) /\ exists fs_q_ics_equality_prefix_at0. ab = fs_q_ics_equality_prefix_at0 * S ((S (ics_index_equality_prefix)) * ac) + (ics_value0_equality_prefix))) -> (((exists fs_h_ics_equality_prefix_at1. fs_h_ics_equality_prefix_at1 + S (ics_value1_equality_prefix) = S ((S (ics_index_equality_prefix)) * bc)) /\ exists fs_q_ics_equality_prefix_at1. bb = fs_q_ics_equality_prefix_at1 * S ((S (ics_index_equality_prefix)) * bc) + (ics_value1_equality_prefix))) -> (((exists fs_h_ics_equality_prefix_at2. fs_h_ics_equality_prefix_at2 + S (ics_value2_equality_prefix) = S ((S (ics_index_equality_prefix)) * ec)) /\ exists fs_q_ics_equality_prefix_at2. eb = fs_q_ics_equality_prefix_at2 * S ((S (ics_index_equality_prefix)) * ec) + (ics_value2_equality_prefix))) -> (((exists fs_h_ics_equality_prefix_at3. fs_h_ics_equality_prefix_at3 + S (ics_value3_equality_prefix) = S ((S (ics_index_equality_prefix)) * fc)) /\ exists fs_q_ics_equality_prefix_at3. fb = fs_q_ics_equality_prefix_at3 * S ((S (ics_index_equality_prefix)) * fc) + (ics_value3_equality_prefix))) -> ics_value0_equality_prefix + ics_value3_equality_prefix = ics_value2_equality_prefix + ics_value1_equality_prefix)

Complete tactic proof in conservative notation

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

38 script commands · 5 reading checkpoints · 0 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 bb
  4. L4
    intro bc
  5. L5
    intro eb
  6. L6
    intro ec
  7. L7
    intro fb
  8. L8
    intro fc
  9. L9
    intro L
  10. L10
    intro K
02Fix variables and assumptionsL11–20

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

  1. L11
    intro hbound
  2. L12
    intro hequal
  3. L13
    intro i
  4. L14
    intro a
  5. L15
    intro b
  6. L16
    intro c
  7. L17
    intro d
  8. L18
    intro hi
  9. L19
    intro ha
  10. L20
    intro hb
03Fix variables and assumptionsL21–22

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

  1. L21
    intro hc
  2. L22
    intro hd
04Use earlier factsL23–32

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

  1. L23
    specialize hequal (i)
  2. L24
    specialize hequal (a)
  3. L25
    specialize hequal (b)
  4. L26
    specialize hequal (c)
  5. L27
    specialize hequal (d)
  6. L28
    apply hequal
  7. L29
    specialize lt_of_lt_of_le (i)
  8. L30
    specialize lt_of_lt_of_le (K)
  9. L31
    specialize lt_of_lt_of_le (L)
  10. L32
    apply lt_of_lt_of_le
05Use earlier factsL33–38

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

  1. L33
    exact hi
  2. L34
    exact hbound
  3. L35
    exact ha
  4. L36
    exact hb
  5. L37
    exact hc
  6. L38
    exact hd

Library-wide reading audit

Original defined command ledger · 38 lines
  1. 0001intro ab
  2. 0002intro ac
  3. 0003intro bb
  4. 0004intro bc
  5. 0005intro eb
  6. 0006intro ec
  7. 0007intro fb
  8. 0008intro fc
  9. 0009intro L
  10. 0010intro K
  11. 0011intro hbound
  12. 0012intro hequal
  13. 0013intro i
  14. 0014intro a
  15. 0015intro b
  16. 0016intro c
  17. 0017intro d
  18. 0018intro hi
  19. 0019intro ha
  20. 0020intro hb
  21. 0021intro hc
  22. 0022intro hd
  23. 0023specialize hequal (i)
  24. 0024specialize hequal (a)
  25. 0025specialize hequal (b)
  26. 0026specialize hequal (c)
  27. 0027specialize hequal (d)
  28. 0028apply hequal
  29. 0029specialize lt_of_lt_of_le (i)
  30. 0030specialize lt_of_lt_of_le (K)
  31. 0031specialize lt_of_lt_of_le (L)
  32. 0032apply lt_of_lt_of_le
  33. 0033exact hi
  34. 0034exact hbound
  35. 0035exact ha
  36. 0036exact hb
  37. 0037exact hc
  38. 0038exact hd