DL0093

matrix_integer_first_row_equality

Actual integer equality of a nonempty square matrix entails equality of its complete genuine first row.

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. ∀ q. IntegerMatrixEntrywiseEqual(ab,ac,bb,bc,eb,ec,fb,fc,S q,S q) → IntegerVectorEqual(ab,ac,bb,bc,eb,ec,fb,fc,S q)

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

Definition DAG

IntegerVectorEqual(ab,ac,db,dc,eb,ec,fb,fc,l) · 1IntegerMatrixEntrywiseEqual(ab,ac,bb,bc,eb,ec,fb,fc,r,w) · 1

Actual proof prerequisites

matrix_integer_vector_equality_restrictle_scaled_nonzero · checked external prerequisitesucc_ne_zero · checked external prerequisite
Original expanded first-order statement 
forall ab ac bb bc eb ec fb fc q. (forall ics_index_parent_matrix_equal ics_value0_parent_matrix_equal ics_value1_parent_matrix_equal ics_value2_parent_matrix_equal ics_value3_parent_matrix_equal. (exists ics_gap_parent_matrix_equal_bound. ics_gap_parent_matrix_equal_bound + S (ics_index_parent_matrix_equal) = ((S q) * (S q))) -> (((exists fs_h_ics_parent_matrix_equal_at0. fs_h_ics_parent_matrix_equal_at0 + S (ics_value0_parent_matrix_equal) = S ((S (ics_index_parent_matrix_equal)) * ac)) /\ exists fs_q_ics_parent_matrix_equal_at0. ab = fs_q_ics_parent_matrix_equal_at0 * S ((S (ics_index_parent_matrix_equal)) * ac) + (ics_value0_parent_matrix_equal))) -> (((exists fs_h_ics_parent_matrix_equal_at1. fs_h_ics_parent_matrix_equal_at1 + S (ics_value1_parent_matrix_equal) = S ((S (ics_index_parent_matrix_equal)) * bc)) /\ exists fs_q_ics_parent_matrix_equal_at1. bb = fs_q_ics_parent_matrix_equal_at1 * S ((S (ics_index_parent_matrix_equal)) * bc) + (ics_value1_parent_matrix_equal))) -> (((exists fs_h_ics_parent_matrix_equal_at2. fs_h_ics_parent_matrix_equal_at2 + S (ics_value2_parent_matrix_equal) = S ((S (ics_index_parent_matrix_equal)) * ec)) /\ exists fs_q_ics_parent_matrix_equal_at2. eb = fs_q_ics_parent_matrix_equal_at2 * S ((S (ics_index_parent_matrix_equal)) * ec) + (ics_value2_parent_matrix_equal))) -> (((exists fs_h_ics_parent_matrix_equal_at3. fs_h_ics_parent_matrix_equal_at3 + S (ics_value3_parent_matrix_equal) = S ((S (ics_index_parent_matrix_equal)) * fc)) /\ exists fs_q_ics_parent_matrix_equal_at3. fb = fs_q_ics_parent_matrix_equal_at3 * S ((S (ics_index_parent_matrix_equal)) * fc) + (ics_value3_parent_matrix_equal))) -> ics_value0_parent_matrix_equal + ics_value3_parent_matrix_equal = ics_value2_parent_matrix_equal + ics_value1_parent_matrix_equal) -> (forall ics_index_first_row_equal ics_value0_first_row_equal ics_value1_first_row_equal ics_value2_first_row_equal ics_value3_first_row_equal. (exists ics_gap_first_row_equal_bound. ics_gap_first_row_equal_bound + S (ics_index_first_row_equal) = (S q)) -> (((exists fs_h_ics_first_row_equal_at0. fs_h_ics_first_row_equal_at0 + S (ics_value0_first_row_equal) = S ((S (ics_index_first_row_equal)) * ac)) /\ exists fs_q_ics_first_row_equal_at0. ab = fs_q_ics_first_row_equal_at0 * S ((S (ics_index_first_row_equal)) * ac) + (ics_value0_first_row_equal))) -> (((exists fs_h_ics_first_row_equal_at1. fs_h_ics_first_row_equal_at1 + S (ics_value1_first_row_equal) = S ((S (ics_index_first_row_equal)) * bc)) /\ exists fs_q_ics_first_row_equal_at1. bb = fs_q_ics_first_row_equal_at1 * S ((S (ics_index_first_row_equal)) * bc) + (ics_value1_first_row_equal))) -> (((exists fs_h_ics_first_row_equal_at2. fs_h_ics_first_row_equal_at2 + S (ics_value2_first_row_equal) = S ((S (ics_index_first_row_equal)) * ec)) /\ exists fs_q_ics_first_row_equal_at2. eb = fs_q_ics_first_row_equal_at2 * S ((S (ics_index_first_row_equal)) * ec) + (ics_value2_first_row_equal))) -> (((exists fs_h_ics_first_row_equal_at3. fs_h_ics_first_row_equal_at3 + S (ics_value3_first_row_equal) = S ((S (ics_index_first_row_equal)) * fc)) /\ exists fs_q_ics_first_row_equal_at3. fb = fs_q_ics_first_row_equal_at3 * S ((S (ics_index_first_row_equal)) * fc) + (ics_value3_first_row_equal))) -> ics_value0_first_row_equal + ics_value3_first_row_equal = ics_value2_first_row_equal + ics_value1_first_row_equal)

Complete tactic proof in conservative notation

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

27 script commands · 3 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.

Named ingredients (1)
matrix integer vector equality restrict
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 q
  10. L10
    intro hequal
02Use earlier factsL11–20

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

  1. L11
    specialize matrix_integer_vector_equality_restrict (ab)
  2. L12
    specialize matrix_integer_vector_equality_restrict (ac)
  3. L13
    specialize matrix_integer_vector_equality_restrict (bb)
  4. L14
    specialize matrix_integer_vector_equality_restrict (bc)
  5. L15
    specialize matrix_integer_vector_equality_restrict (eb)
  6. L16
    specialize matrix_integer_vector_equality_restrict (ec)
  7. L17
    specialize matrix_integer_vector_equality_restrict (fb)
  8. L18
    specialize matrix_integer_vector_equality_restrict (fc)
  9. L19
    specialize matrix_integer_vector_equality_restrict ((S q) * (S q))
  10. L20
    specialize matrix_integer_vector_equality_restrict (S q)
03Use earlier factsL21–27

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

  1. L21
    apply matrix_integer_vector_equality_restrict
  2. L22
    specialize le_scaled_nonzero (S q)
  3. L23
    specialize le_scaled_nonzero (S q)
  4. L24
    apply le_scaled_nonzero
  5. L25
    specialize succ_ne_zero (q)
  6. L26
    apply succ_ne_zero
  7. L27
    exact hequal

Library-wide reading audit

Original defined command ledger · 27 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 q
  10. 0010intro hequal
  11. 0011specialize matrix_integer_vector_equality_restrict (ab)
  12. 0012specialize matrix_integer_vector_equality_restrict (ac)
  13. 0013specialize matrix_integer_vector_equality_restrict (bb)
  14. 0014specialize matrix_integer_vector_equality_restrict (bc)
  15. 0015specialize matrix_integer_vector_equality_restrict (eb)
  16. 0016specialize matrix_integer_vector_equality_restrict (ec)
  17. 0017specialize matrix_integer_vector_equality_restrict (fb)
  18. 0018specialize matrix_integer_vector_equality_restrict (fc)
  19. 0019specialize matrix_integer_vector_equality_restrict ((S q) * (S q))
  20. 0020specialize matrix_integer_vector_equality_restrict (S q)
  21. 0021apply matrix_integer_vector_equality_restrict
  22. 0022specialize le_scaled_nonzero (S q)
  23. 0023specialize le_scaled_nonzero (S q)
  24. 0024apply le_scaled_nonzero
  25. 0025specialize succ_ne_zero (q)
  26. 0026apply succ_ne_zero
  27. 0027exact hequal