DL0093

matrix_integer_first_row_equality

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 3 declared prerequisites and contains 27 exact native proof lines.

Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

DL0085 matrix_integer_vector_equality_restrict le_scaled_nonzero Stable theorem; checked-use authorized succ_ne_zero Stable theorem; checked-use authorized

Direct dependents

DL0094 signed_recursive_determinant_integer_invariant

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

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.

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