A complete actual selected-submatrix code remains valid under equality-preserving selector recoding.
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 b c w rb rc cb cc q Rb Rc Cb Cc ub uc. (forall mdr_i_prefix_rows mdr_a_prefix_rows. (exists mdr_gap_prefix_rowsb. mdr_gap_prefix_rowsb + S (mdr_i_prefix_rows) = (q)) -> (((exists ff_h_mdr_prefix_rowso. ff_h_mdr_prefix_rowso + S (mdr_a_prefix_rows) = S ((S (mdr_i_prefix_rows)) * rc)) /\ exists ff_q_mdr_prefix_rowso. rb = ff_q_mdr_prefix_rowso * S ((S (mdr_i_prefix_rows)) * rc) + (mdr_a_prefix_rows))) -> (((exists ff_h_mdr_prefix_rowsn. ff_h_mdr_prefix_rowsn + S (mdr_a_prefix_rows) = S ((S (mdr_i_prefix_rows)) * Rc)) /\ exists ff_q_mdr_prefix_rowsn. Rb = ff_q_mdr_prefix_rowsn * S ((S (mdr_i_prefix_rows)) * Rc) + (mdr_a_prefix_rows)))) -> (forall mdr_i_prefix_columns mdr_a_prefix_columns. (exists mdr_gap_prefix_columnsb. mdr_gap_prefix_columnsb + S (mdr_i_prefix_columns) = (q)) -> (((exists ff_h_mdr_prefix_columnso. ff_h_mdr_prefix_columnso + S (mdr_a_prefix_columns) = S ((S (mdr_i_prefix_columns)) * cc)) /\ exists ff_q_mdr_prefix_columnso. cb = ff_q_mdr_prefix_columnso * S ((S (mdr_i_prefix_columns)) * cc) + (mdr_a_prefix_columns))) -> (((exists ff_h_mdr_prefix_columnsn. ff_h_mdr_prefix_columnsn + S (mdr_a_prefix_columns) = S ((S (mdr_i_prefix_columns)) * Cc)) /\ exists ff_q_mdr_prefix_columnsn. Cb = ff_q_mdr_prefix_columnsn * S ((S (mdr_i_prefix_columns)) * Cc) + (mdr_a_prefix_columns)))) -> (forall mdr_i_selected_prefix_source. (exists mdr_gap_selected_prefix_sourcebound. mdr_gap_selected_prefix_sourcebound + S (mdr_i_selected_prefix_source) = (q * q)) -> exists mdr_a_selected_prefix_source. (((exists mdr_r_selected_prefix_sourcepoint mdr_s_selected_prefix_sourcepoint mdr_u_selected_prefix_sourcepoint mdr_v_selected_prefix_sourcepoint. ((mdr_i_selected_prefix_source = (q) * mdr_r_selected_prefix_sourcepoint + mdr_s_selected_prefix_sourcepoint) /\ ((exists mdr_gap_selected_prefix_sourcepointcolumn. mdr_gap_selected_prefix_sourcepointcolumn + S (mdr_s_selected_prefix_sourcepoint) = (q)) /\ ((((exists ff_h_mdr_selected_prefix_sourcepointrow_index. ff_h_mdr_selected_prefix_sourcepointrow_index + S (mdr_u_selected_prefix_sourcepoint) = S ((S (mdr_r_selected_prefix_sourcepoint)) * rc)) /\ exists ff_q_mdr_selected_prefix_sourcepointrow_index. rb = ff_q_mdr_selected_prefix_sourcepointrow_index * S ((S (mdr_r_selected_prefix_sourcepoint)) * rc) + (mdr_u_selected_prefix_sourcepoint))) /\ ((((exists ff_h_mdr_selected_prefix_sourcepointcolumn_index. ff_h_mdr_selected_prefix_sourcepointcolumn_index + S (mdr_v_selected_prefix_sourcepoint) = S ((S (mdr_s_selected_prefix_sourcepoint)) * cc)) /\ exists ff_q_mdr_selected_prefix_sourcepointcolumn_index. cb = ff_q_mdr_selected_prefix_sourcepointcolumn_index * S ((S (mdr_s_selected_prefix_sourcepoint)) * cc) + (mdr_v_selected_prefix_sourcepoint))) /\ (((exists ff_h_mdr_selected_prefix_sourcepointsource. ff_h_mdr_selected_prefix_sourcepointsource + S (mdr_a_selected_prefix_source) = S ((S ((mdr_u_selected_prefix_sourcepoint) * (w) + (mdr_v_selected_prefix_sourcepoint))) * c)) /\ exists ff_q_mdr_selected_prefix_sourcepointsource. b = ff_q_mdr_selected_prefix_sourcepointsource * S ((S ((mdr_u_selected_prefix_sourcepoint) * (w) + (mdr_v_selected_prefix_sourcepoint))) * c) + (mdr_a_selected_prefix_source)))))))) /\ (((exists ff_h_mdr_selected_prefix_sourceoutput. ff_h_mdr_selected_prefix_sourceoutput + S (mdr_a_selected_prefix_source) = S ((S (mdr_i_selected_prefix_source)) * uc)) /\ exists ff_q_mdr_selected_prefix_sourceoutput. ub = ff_q_mdr_selected_prefix_sourceoutput * S ((S (mdr_i_selected_prefix_source)) * uc) + (mdr_a_selected_prefix_source)))))) -> (forall mdr_i_selected_prefix_target. (exists mdr_gap_selected_prefix_targetbound. mdr_gap_selected_prefix_targetbound + S (mdr_i_selected_prefix_target) = (q * q)) -> exists mdr_a_selected_prefix_target. (((exists mdr_r_selected_prefix_targetpoint mdr_s_selected_prefix_targetpoint mdr_u_selected_prefix_targetpoint mdr_v_selected_prefix_targetpoint. ((mdr_i_selected_prefix_target = (q) * mdr_r_selected_prefix_targetpoint + mdr_s_selected_prefix_targetpoint) /\ ((exists mdr_gap_selected_prefix_targetpointcolumn. mdr_gap_selected_prefix_targetpointcolumn + S (mdr_s_selected_prefix_targetpoint) = (q)) /\ ((((exists ff_h_mdr_selected_prefix_targetpointrow_index. ff_h_mdr_selected_prefix_targetpointrow_index + S (mdr_u_selected_prefix_targetpoint) = S ((S (mdr_r_selected_prefix_targetpoint)) * Rc)) /\ exists ff_q_mdr_selected_prefix_targetpointrow_index. Rb = ff_q_mdr_selected_prefix_targetpointrow_index * S ((S (mdr_r_selected_prefix_targetpoint)) * Rc) + (mdr_u_selected_prefix_targetpoint))) /\ ((((exists ff_h_mdr_selected_prefix_targetpointcolumn_index. ff_h_mdr_selected_prefix_targetpointcolumn_index + S (mdr_v_selected_prefix_targetpoint) = S ((S (mdr_s_selected_prefix_targetpoint)) * Cc)) /\ exists ff_q_mdr_selected_prefix_targetpointcolumn_index. Cb = ff_q_mdr_selected_prefix_targetpointcolumn_index * S ((S (mdr_s_selected_prefix_targetpoint)) * Cc) + (mdr_v_selected_prefix_targetpoint))) /\ (((exists ff_h_mdr_selected_prefix_targetpointsource. ff_h_mdr_selected_prefix_targetpointsource + S (mdr_a_selected_prefix_target) = S ((S ((mdr_u_selected_prefix_targetpoint) * (w) + (mdr_v_selected_prefix_targetpoint))) * c)) /\ exists ff_q_mdr_selected_prefix_targetpointsource. b = ff_q_mdr_selected_prefix_targetpointsource * S ((S ((mdr_u_selected_prefix_targetpoint) * (w) + (mdr_v_selected_prefix_targetpoint))) * c) + (mdr_a_selected_prefix_target)))))))) /\ (((exists ff_h_mdr_selected_prefix_targetoutput. ff_h_mdr_selected_prefix_targetoutput + S (mdr_a_selected_prefix_target) = S ((S (mdr_i_selected_prefix_target)) * uc)) /\ exists ff_q_mdr_selected_prefix_targetoutput. ub = ff_q_mdr_selected_prefix_targetoutput * S ((S (mdr_i_selected_prefix_target)) * uc) + (mdr_a_selected_prefix_target))))))
Complete tactic proof in conservative notation
All 47 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.