Genuine cofactor minors of integer-equal matrices are integer-equal, even when every positive/negative code and representative differs.
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.
forall ab ac bb bc eb ec fb fc ub uc vb vc Ub Uc Vb Vc q j. (forall ics_index_signed_minor_parent ics_value0_signed_minor_parent ics_value1_signed_minor_parent ics_value2_signed_minor_parent ics_value3_signed_minor_parent. (exists ics_gap_signed_minor_parent_bound. ics_gap_signed_minor_parent_bound + S (ics_index_signed_minor_parent) = ((S q) * (S q))) -> (((exists fs_h_ics_signed_minor_parent_at0. fs_h_ics_signed_minor_parent_at0 + S (ics_value0_signed_minor_parent) = S ((S (ics_index_signed_minor_parent)) * ac)) /\ exists fs_q_ics_signed_minor_parent_at0. ab = fs_q_ics_signed_minor_parent_at0 * S ((S (ics_index_signed_minor_parent)) * ac) + (ics_value0_signed_minor_parent))) -> (((exists fs_h_ics_signed_minor_parent_at1. fs_h_ics_signed_minor_parent_at1 + S (ics_value1_signed_minor_parent) = S ((S (ics_index_signed_minor_parent)) * bc)) /\ exists fs_q_ics_signed_minor_parent_at1. bb = fs_q_ics_signed_minor_parent_at1 * S ((S (ics_index_signed_minor_parent)) * bc) + (ics_value1_signed_minor_parent))) -> (((exists fs_h_ics_signed_minor_parent_at2. fs_h_ics_signed_minor_parent_at2 + S (ics_value2_signed_minor_parent) = S ((S (ics_index_signed_minor_parent)) * ec)) /\ exists fs_q_ics_signed_minor_parent_at2. eb = fs_q_ics_signed_minor_parent_at2 * S ((S (ics_index_signed_minor_parent)) * ec) + (ics_value2_signed_minor_parent))) -> (((exists fs_h_ics_signed_minor_parent_at3. fs_h_ics_signed_minor_parent_at3 + S (ics_value3_signed_minor_parent) = S ((S (ics_index_signed_minor_parent)) * fc)) /\ exists fs_q_ics_signed_minor_parent_at3. fb = fs_q_ics_signed_minor_parent_at3 * S ((S (ics_index_signed_minor_parent)) * fc) + (ics_value3_signed_minor_parent))) -> ics_value0_signed_minor_parent + ics_value3_signed_minor_parent = ics_value2_signed_minor_parent + ics_value1_signed_minor_parent) -> (((forall ff_index_mdm_prefix_mdr_signed_minor_first_positive. (exists ff_gap_mdm_lt_mdr_signed_minor_first_positive_index_bound. ff_gap_mdm_lt_mdr_signed_minor_first_positive_index_bound + S (ff_index_mdm_prefix_mdr_signed_minor_first_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_signed_minor_first_positive ff_column_mdm_prefix_mdr_signed_minor_first_positive ff_value_mdm_prefix_mdr_signed_minor_first_positive. (ff_index_mdm_prefix_mdr_signed_minor_first_positive = (q) * ff_row_mdm_prefix_mdr_signed_minor_first_positive + ff_column_mdm_prefix_mdr_signed_minor_first_positive /\ ((exists ff_gap_mdm_lt_mdr_signed_minor_first_positive_column_bound. ff_gap_mdm_lt_mdr_signed_minor_first_positive_column_bound + S (ff_column_mdm_prefix_mdr_signed_minor_first_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_signed_minor_first_positive_cell ff_column_mdm_cell_mdr_signed_minor_first_positive_cell. (((((exists ff_gap_mdm_lt_mdr_signed_minor_first_positive_cell_row_before. ff_gap_mdm_lt_mdr_signed_minor_first_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_signed_minor_first_positive) = (0)) /\ ff_row_mdm_cell_mdr_signed_minor_first_positive_cell = ff_row_mdm_prefix_mdr_signed_minor_first_positive) \/ ((exists ff_gap_mdm_le_mdr_signed_minor_first_positive_cell_row_after. ff_gap_mdm_le_mdr_signed_minor_first_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_signed_minor_first_positive)) /\ ff_row_mdm_cell_mdr_signed_minor_first_positive_cell = S ff_row_mdm_prefix_mdr_signed_minor_first_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_signed_minor_first_positive_cell_column_before. ff_gap_mdm_lt_mdr_signed_minor_first_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_signed_minor_first_positive) = (j)) /\ ff_column_mdm_cell_mdr_signed_minor_first_positive_cell = ff_column_mdm_prefix_mdr_signed_minor_first_positive) \/ ((exists ff_gap_mdm_le_mdr_signed_minor_first_positive_cell_column_after. ff_gap_mdm_le_mdr_signed_minor_first_positive_cell_column_after + (j) = (ff_column_mdm_prefix_mdr_signed_minor_first_positive)) /\ ff_column_mdm_cell_mdr_signed_minor_first_positive_cell = S ff_column_mdm_prefix_mdr_signed_minor_first_positive))) /\ (((exists ff_h_mdm_mdr_signed_minor_first_positive_cell_source. ff_h_mdm_mdr_signed_minor_first_positive_cell_source + S (ff_value_mdm_prefix_mdr_signed_minor_first_positive) = S ((S ((ff_row_mdm_cell_mdr_signed_minor_first_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_signed_minor_first_positive_cell))) * ac)) /\ exists ff_q_mdm_mdr_signed_minor_first_positive_cell_source. ab = ff_q_mdm_mdr_signed_minor_first_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_signed_minor_first_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_signed_minor_first_positive_cell))) * ac) + (ff_value_mdm_prefix_mdr_signed_minor_first_positive)))))) /\ (((exists ff_h_mdm_mdr_signed_minor_first_positive_target. ff_h_mdm_mdr_signed_minor_first_positive_target + S (ff_value_mdm_prefix_mdr_signed_minor_first_positive) = S ((S (ff_index_mdm_prefix_mdr_signed_minor_first_positive)) * uc)) /\ exists ff_q_mdm_mdr_signed_minor_first_positive_target. ub = ff_q_mdm_mdr_signed_minor_first_positive_target * S ((S (ff_index_mdm_prefix_mdr_signed_minor_first_positive)) * uc) + (ff_value_mdm_prefix_mdr_signed_minor_first_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_signed_minor_first_negative. (exists ff_gap_mdm_lt_mdr_signed_minor_first_negative_index_bound. ff_gap_mdm_lt_mdr_signed_minor_first_negative_index_bound + S (ff_index_mdm_prefix_mdr_signed_minor_first_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_signed_minor_first_negative ff_column_mdm_prefix_mdr_signed_minor_first_negative ff_value_mdm_prefix_mdr_signed_minor_first_negative. (ff_index_mdm_prefix_mdr_signed_minor_first_negative = (q) * ff_row_mdm_prefix_mdr_signed_minor_first_negative + ff_column_mdm_prefix_mdr_signed_minor_first_negative /\ ((exists ff_gap_mdm_lt_mdr_signed_minor_first_negative_column_bound. ff_gap_mdm_lt_mdr_signed_minor_first_negative_column_bound + S (ff_column_mdm_prefix_mdr_signed_minor_first_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_signed_minor_first_negative_cell ff_column_mdm_cell_mdr_signed_minor_first_negative_cell. (((((exists ff_gap_mdm_lt_mdr_signed_minor_first_negative_cell_row_before. ff_gap_mdm_lt_mdr_signed_minor_first_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_signed_minor_first_negative) = (0)) /\ ff_row_mdm_cell_mdr_signed_minor_first_negative_cell = ff_row_mdm_prefix_mdr_signed_minor_first_negative) \/ ((exists ff_gap_mdm_le_mdr_signed_minor_first_negative_cell_row_after. ff_gap_mdm_le_mdr_signed_minor_first_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_signed_minor_first_negative)) /\ ff_row_mdm_cell_mdr_signed_minor_first_negative_cell = S ff_row_mdm_prefix_mdr_signed_minor_first_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_signed_minor_first_negative_cell_column_before. ff_gap_mdm_lt_mdr_signed_minor_first_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_signed_minor_first_negative) = (j)) /\ ff_column_mdm_cell_mdr_signed_minor_first_negative_cell = ff_column_mdm_prefix_mdr_signed_minor_first_negative) \/ ((exists ff_gap_mdm_le_mdr_signed_minor_first_negative_cell_column_after. ff_gap_mdm_le_mdr_signed_minor_first_negative_cell_column_after + (j) = (ff_column_mdm_prefix_mdr_signed_minor_first_negative)) /\ ff_column_mdm_cell_mdr_signed_minor_first_negative_cell = S ff_column_mdm_prefix_mdr_signed_minor_first_negative))) /\ (((exists ff_h_mdm_mdr_signed_minor_first_negative_cell_source. ff_h_mdm_mdr_signed_minor_first_negative_cell_source + S (ff_value_mdm_prefix_mdr_signed_minor_first_negative) = S ((S ((ff_row_mdm_cell_mdr_signed_minor_first_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_signed_minor_first_negative_cell))) * bc)) /\ exists ff_q_mdm_mdr_signed_minor_first_negative_cell_source. bb = ff_q_mdm_mdr_signed_minor_first_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_signed_minor_first_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_signed_minor_first_negative_cell))) * bc) + (ff_value_mdm_prefix_mdr_signed_minor_first_negative)))))) /\ (((exists ff_h_mdm_mdr_signed_minor_first_negative_target. ff_h_mdm_mdr_signed_minor_first_negative_target + S (ff_value_mdm_prefix_mdr_signed_minor_first_negative) = S ((S (ff_index_mdm_prefix_mdr_signed_minor_first_negative)) * vc)) /\ exists ff_q_mdm_mdr_signed_minor_first_negative_target. vb = ff_q_mdm_mdr_signed_minor_first_negative_target * S ((S (ff_index_mdm_prefix_mdr_signed_minor_first_negative)) * vc) + (ff_value_mdm_prefix_mdr_signed_minor_first_negative))))))))) -> (((forall ff_index_mdm_prefix_mdr_signed_minor_second_positive. (exists ff_gap_mdm_lt_mdr_signed_minor_second_positive_index_bound. ff_gap_mdm_lt_mdr_signed_minor_second_positive_index_bound + S (ff_index_mdm_prefix_mdr_signed_minor_second_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_signed_minor_second_positive ff_column_mdm_prefix_mdr_signed_minor_second_positive ff_value_mdm_prefix_mdr_signed_minor_second_positive. (ff_index_mdm_prefix_mdr_signed_minor_second_positive = (q) * ff_row_mdm_prefix_mdr_signed_minor_second_positive + ff_column_mdm_prefix_mdr_signed_minor_second_positive /\ ((exists ff_gap_mdm_lt_mdr_signed_minor_second_positive_column_bound. ff_gap_mdm_lt_mdr_signed_minor_second_positive_column_bound + S (ff_column_mdm_prefix_mdr_signed_minor_second_positive) = (q)) /\ ((exists ff_row_mdm_cell_mdr_signed_minor_second_positive_cell ff_column_mdm_cell_mdr_signed_minor_second_positive_cell. (((((exists ff_gap_mdm_lt_mdr_signed_minor_second_positive_cell_row_before. ff_gap_mdm_lt_mdr_signed_minor_second_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_signed_minor_second_positive) = (0)) /\ ff_row_mdm_cell_mdr_signed_minor_second_positive_cell = ff_row_mdm_prefix_mdr_signed_minor_second_positive) \/ ((exists ff_gap_mdm_le_mdr_signed_minor_second_positive_cell_row_after. ff_gap_mdm_le_mdr_signed_minor_second_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_signed_minor_second_positive)) /\ ff_row_mdm_cell_mdr_signed_minor_second_positive_cell = S ff_row_mdm_prefix_mdr_signed_minor_second_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_signed_minor_second_positive_cell_column_before. ff_gap_mdm_lt_mdr_signed_minor_second_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_signed_minor_second_positive) = (j)) /\ ff_column_mdm_cell_mdr_signed_minor_second_positive_cell = ff_column_mdm_prefix_mdr_signed_minor_second_positive) \/ ((exists ff_gap_mdm_le_mdr_signed_minor_second_positive_cell_column_after. ff_gap_mdm_le_mdr_signed_minor_second_positive_cell_column_after + (j) = (ff_column_mdm_prefix_mdr_signed_minor_second_positive)) /\ ff_column_mdm_cell_mdr_signed_minor_second_positive_cell = S ff_column_mdm_prefix_mdr_signed_minor_second_positive))) /\ (((exists ff_h_mdm_mdr_signed_minor_second_positive_cell_source. ff_h_mdm_mdr_signed_minor_second_positive_cell_source + S (ff_value_mdm_prefix_mdr_signed_minor_second_positive) = S ((S ((ff_row_mdm_cell_mdr_signed_minor_second_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_signed_minor_second_positive_cell))) * ec)) /\ exists ff_q_mdm_mdr_signed_minor_second_positive_cell_source. eb = ff_q_mdm_mdr_signed_minor_second_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_signed_minor_second_positive_cell) * (S (q)) + (ff_column_mdm_cell_mdr_signed_minor_second_positive_cell))) * ec) + (ff_value_mdm_prefix_mdr_signed_minor_second_positive)))))) /\ (((exists ff_h_mdm_mdr_signed_minor_second_positive_target. ff_h_mdm_mdr_signed_minor_second_positive_target + S (ff_value_mdm_prefix_mdr_signed_minor_second_positive) = S ((S (ff_index_mdm_prefix_mdr_signed_minor_second_positive)) * Uc)) /\ exists ff_q_mdm_mdr_signed_minor_second_positive_target. Ub = ff_q_mdm_mdr_signed_minor_second_positive_target * S ((S (ff_index_mdm_prefix_mdr_signed_minor_second_positive)) * Uc) + (ff_value_mdm_prefix_mdr_signed_minor_second_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_signed_minor_second_negative. (exists ff_gap_mdm_lt_mdr_signed_minor_second_negative_index_bound. ff_gap_mdm_lt_mdr_signed_minor_second_negative_index_bound + S (ff_index_mdm_prefix_mdr_signed_minor_second_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mdr_signed_minor_second_negative ff_column_mdm_prefix_mdr_signed_minor_second_negative ff_value_mdm_prefix_mdr_signed_minor_second_negative. (ff_index_mdm_prefix_mdr_signed_minor_second_negative = (q) * ff_row_mdm_prefix_mdr_signed_minor_second_negative + ff_column_mdm_prefix_mdr_signed_minor_second_negative /\ ((exists ff_gap_mdm_lt_mdr_signed_minor_second_negative_column_bound. ff_gap_mdm_lt_mdr_signed_minor_second_negative_column_bound + S (ff_column_mdm_prefix_mdr_signed_minor_second_negative) = (q)) /\ ((exists ff_row_mdm_cell_mdr_signed_minor_second_negative_cell ff_column_mdm_cell_mdr_signed_minor_second_negative_cell. (((((exists ff_gap_mdm_lt_mdr_signed_minor_second_negative_cell_row_before. ff_gap_mdm_lt_mdr_signed_minor_second_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_signed_minor_second_negative) = (0)) /\ ff_row_mdm_cell_mdr_signed_minor_second_negative_cell = ff_row_mdm_prefix_mdr_signed_minor_second_negative) \/ ((exists ff_gap_mdm_le_mdr_signed_minor_second_negative_cell_row_after. ff_gap_mdm_le_mdr_signed_minor_second_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_signed_minor_second_negative)) /\ ff_row_mdm_cell_mdr_signed_minor_second_negative_cell = S ff_row_mdm_prefix_mdr_signed_minor_second_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_signed_minor_second_negative_cell_column_before. ff_gap_mdm_lt_mdr_signed_minor_second_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_signed_minor_second_negative) = (j)) /\ ff_column_mdm_cell_mdr_signed_minor_second_negative_cell = ff_column_mdm_prefix_mdr_signed_minor_second_negative) \/ ((exists ff_gap_mdm_le_mdr_signed_minor_second_negative_cell_column_after. ff_gap_mdm_le_mdr_signed_minor_second_negative_cell_column_after + (j) = (ff_column_mdm_prefix_mdr_signed_minor_second_negative)) /\ ff_column_mdm_cell_mdr_signed_minor_second_negative_cell = S ff_column_mdm_prefix_mdr_signed_minor_second_negative))) /\ (((exists ff_h_mdm_mdr_signed_minor_second_negative_cell_source. ff_h_mdm_mdr_signed_minor_second_negative_cell_source + S (ff_value_mdm_prefix_mdr_signed_minor_second_negative) = S ((S ((ff_row_mdm_cell_mdr_signed_minor_second_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_signed_minor_second_negative_cell))) * fc)) /\ exists ff_q_mdm_mdr_signed_minor_second_negative_cell_source. fb = ff_q_mdm_mdr_signed_minor_second_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_signed_minor_second_negative_cell) * (S (q)) + (ff_column_mdm_cell_mdr_signed_minor_second_negative_cell))) * fc) + (ff_value_mdm_prefix_mdr_signed_minor_second_negative)))))) /\ (((exists ff_h_mdm_mdr_signed_minor_second_negative_target. ff_h_mdm_mdr_signed_minor_second_negative_target + S (ff_value_mdm_prefix_mdr_signed_minor_second_negative) = S ((S (ff_index_mdm_prefix_mdr_signed_minor_second_negative)) * Vc)) /\ exists ff_q_mdm_mdr_signed_minor_second_negative_target. Vb = ff_q_mdm_mdr_signed_minor_second_negative_target * S ((S (ff_index_mdm_prefix_mdr_signed_minor_second_negative)) * Vc) + (ff_value_mdm_prefix_mdr_signed_minor_second_negative))))))))) -> (forall ics_index_signed_minor_equal ics_value0_signed_minor_equal ics_value1_signed_minor_equal ics_value2_signed_minor_equal ics_value3_signed_minor_equal. (exists ics_gap_signed_minor_equal_bound. ics_gap_signed_minor_equal_bound + S (ics_index_signed_minor_equal) = ((q) * (q))) -> (((exists fs_h_ics_signed_minor_equal_at0. fs_h_ics_signed_minor_equal_at0 + S (ics_value0_signed_minor_equal) = S ((S (ics_index_signed_minor_equal)) * uc)) /\ exists fs_q_ics_signed_minor_equal_at0. ub = fs_q_ics_signed_minor_equal_at0 * S ((S (ics_index_signed_minor_equal)) * uc) + (ics_value0_signed_minor_equal))) -> (((exists fs_h_ics_signed_minor_equal_at1. fs_h_ics_signed_minor_equal_at1 + S (ics_value1_signed_minor_equal) = S ((S (ics_index_signed_minor_equal)) * vc)) /\ exists fs_q_ics_signed_minor_equal_at1. vb = fs_q_ics_signed_minor_equal_at1 * S ((S (ics_index_signed_minor_equal)) * vc) + (ics_value1_signed_minor_equal))) -> (((exists fs_h_ics_signed_minor_equal_at2. fs_h_ics_signed_minor_equal_at2 + S (ics_value2_signed_minor_equal) = S ((S (ics_index_signed_minor_equal)) * Uc)) /\ exists fs_q_ics_signed_minor_equal_at2. Ub = fs_q_ics_signed_minor_equal_at2 * S ((S (ics_index_signed_minor_equal)) * Uc) + (ics_value2_signed_minor_equal))) -> (((exists fs_h_ics_signed_minor_equal_at3. fs_h_ics_signed_minor_equal_at3 + S (ics_value3_signed_minor_equal) = S ((S (ics_index_signed_minor_equal)) * Vc)) /\ exists fs_q_ics_signed_minor_equal_at3. Vb = fs_q_ics_signed_minor_equal_at3 * S ((S (ics_index_signed_minor_equal)) * Vc) + (ics_value3_signed_minor_equal))) -> ics_value0_signed_minor_equal + ics_value3_signed_minor_equal = ics_value2_signed_minor_equal + ics_value1_signed_minor_equal)
Complete tactic proof in conservative notation
All 140 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.
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.
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix integer square index width nonzero.
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix recursive quotient row bound.