Five actual pointwise sum relations imply the regrouped sixth relation at every coordinate, with no assumption about canonical beta encodings.
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 cb cc db dc eb ec fb fc pb pc qb qc rb rc l. (forall ff_index_mcp_add_ics_interchange_first ff_left_mcp_add_ics_interchange_first ff_right_mcp_add_ics_interchange_first ff_target_mcp_add_ics_interchange_first. (exists mcp_gap_ics_interchange_first_bound. mcp_gap_ics_interchange_first_bound + S (ff_index_mcp_add_ics_interchange_first) = (l)) -> (((exists fs_h_mcp_ics_interchange_first_left. fs_h_mcp_ics_interchange_first_left + S (ff_left_mcp_add_ics_interchange_first) = S ((S (ff_index_mcp_add_ics_interchange_first)) * ac)) /\ exists fs_q_mcp_ics_interchange_first_left. ab = fs_q_mcp_ics_interchange_first_left * S ((S (ff_index_mcp_add_ics_interchange_first)) * ac) + (ff_left_mcp_add_ics_interchange_first))) -> (((exists fs_h_mcp_ics_interchange_first_right. fs_h_mcp_ics_interchange_first_right + S (ff_right_mcp_add_ics_interchange_first) = S ((S (ff_index_mcp_add_ics_interchange_first)) * bc)) /\ exists fs_q_mcp_ics_interchange_first_right. bb = fs_q_mcp_ics_interchange_first_right * S ((S (ff_index_mcp_add_ics_interchange_first)) * bc) + (ff_right_mcp_add_ics_interchange_first))) -> (((exists fs_h_mcp_ics_interchange_first_target. fs_h_mcp_ics_interchange_first_target + S (ff_target_mcp_add_ics_interchange_first) = S ((S (ff_index_mcp_add_ics_interchange_first)) * pc)) /\ exists fs_q_mcp_ics_interchange_first_target. pb = fs_q_mcp_ics_interchange_first_target * S ((S (ff_index_mcp_add_ics_interchange_first)) * pc) + (ff_target_mcp_add_ics_interchange_first))) -> ff_target_mcp_add_ics_interchange_first = ff_left_mcp_add_ics_interchange_first + ff_right_mcp_add_ics_interchange_first) -> (forall ff_index_mcp_add_ics_interchange_second ff_left_mcp_add_ics_interchange_second ff_right_mcp_add_ics_interchange_second ff_target_mcp_add_ics_interchange_second. (exists mcp_gap_ics_interchange_second_bound. mcp_gap_ics_interchange_second_bound + S (ff_index_mcp_add_ics_interchange_second) = (l)) -> (((exists fs_h_mcp_ics_interchange_second_left. fs_h_mcp_ics_interchange_second_left + S (ff_left_mcp_add_ics_interchange_second) = S ((S (ff_index_mcp_add_ics_interchange_second)) * cc)) /\ exists fs_q_mcp_ics_interchange_second_left. cb = fs_q_mcp_ics_interchange_second_left * S ((S (ff_index_mcp_add_ics_interchange_second)) * cc) + (ff_left_mcp_add_ics_interchange_second))) -> (((exists fs_h_mcp_ics_interchange_second_right. fs_h_mcp_ics_interchange_second_right + S (ff_right_mcp_add_ics_interchange_second) = S ((S (ff_index_mcp_add_ics_interchange_second)) * dc)) /\ exists fs_q_mcp_ics_interchange_second_right. db = fs_q_mcp_ics_interchange_second_right * S ((S (ff_index_mcp_add_ics_interchange_second)) * dc) + (ff_right_mcp_add_ics_interchange_second))) -> (((exists fs_h_mcp_ics_interchange_second_target. fs_h_mcp_ics_interchange_second_target + S (ff_target_mcp_add_ics_interchange_second) = S ((S (ff_index_mcp_add_ics_interchange_second)) * qc)) /\ exists fs_q_mcp_ics_interchange_second_target. qb = fs_q_mcp_ics_interchange_second_target * S ((S (ff_index_mcp_add_ics_interchange_second)) * qc) + (ff_target_mcp_add_ics_interchange_second))) -> ff_target_mcp_add_ics_interchange_second = ff_left_mcp_add_ics_interchange_second + ff_right_mcp_add_ics_interchange_second) -> (forall ff_index_mcp_add_ics_interchange_total ff_left_mcp_add_ics_interchange_total ff_right_mcp_add_ics_interchange_total ff_target_mcp_add_ics_interchange_total. (exists mcp_gap_ics_interchange_total_bound. mcp_gap_ics_interchange_total_bound + S (ff_index_mcp_add_ics_interchange_total) = (l)) -> (((exists fs_h_mcp_ics_interchange_total_left. fs_h_mcp_ics_interchange_total_left + S (ff_left_mcp_add_ics_interchange_total) = S ((S (ff_index_mcp_add_ics_interchange_total)) * ec)) /\ exists fs_q_mcp_ics_interchange_total_left. eb = fs_q_mcp_ics_interchange_total_left * S ((S (ff_index_mcp_add_ics_interchange_total)) * ec) + (ff_left_mcp_add_ics_interchange_total))) -> (((exists fs_h_mcp_ics_interchange_total_right. fs_h_mcp_ics_interchange_total_right + S (ff_right_mcp_add_ics_interchange_total) = S ((S (ff_index_mcp_add_ics_interchange_total)) * fc)) /\ exists fs_q_mcp_ics_interchange_total_right. fb = fs_q_mcp_ics_interchange_total_right * S ((S (ff_index_mcp_add_ics_interchange_total)) * fc) + (ff_right_mcp_add_ics_interchange_total))) -> (((exists fs_h_mcp_ics_interchange_total_target. fs_h_mcp_ics_interchange_total_target + S (ff_target_mcp_add_ics_interchange_total) = S ((S (ff_index_mcp_add_ics_interchange_total)) * rc)) /\ exists fs_q_mcp_ics_interchange_total_target. rb = fs_q_mcp_ics_interchange_total_target * S ((S (ff_index_mcp_add_ics_interchange_total)) * rc) + (ff_target_mcp_add_ics_interchange_total))) -> ff_target_mcp_add_ics_interchange_total = ff_left_mcp_add_ics_interchange_total + ff_right_mcp_add_ics_interchange_total) -> (forall ff_index_mcp_add_ics_interchange_vertical_first ff_left_mcp_add_ics_interchange_vertical_first ff_right_mcp_add_ics_interchange_vertical_first ff_target_mcp_add_ics_interchange_vertical_first. (exists mcp_gap_ics_interchange_vertical_first_bound. mcp_gap_ics_interchange_vertical_first_bound + S (ff_index_mcp_add_ics_interchange_vertical_first) = (l)) -> (((exists fs_h_mcp_ics_interchange_vertical_first_left. fs_h_mcp_ics_interchange_vertical_first_left + S (ff_left_mcp_add_ics_interchange_vertical_first) = S ((S (ff_index_mcp_add_ics_interchange_vertical_first)) * ac)) /\ exists fs_q_mcp_ics_interchange_vertical_first_left. ab = fs_q_mcp_ics_interchange_vertical_first_left * S ((S (ff_index_mcp_add_ics_interchange_vertical_first)) * ac) + (ff_left_mcp_add_ics_interchange_vertical_first))) -> (((exists fs_h_mcp_ics_interchange_vertical_first_right. fs_h_mcp_ics_interchange_vertical_first_right + S (ff_right_mcp_add_ics_interchange_vertical_first) = S ((S (ff_index_mcp_add_ics_interchange_vertical_first)) * cc)) /\ exists fs_q_mcp_ics_interchange_vertical_first_right. cb = fs_q_mcp_ics_interchange_vertical_first_right * S ((S (ff_index_mcp_add_ics_interchange_vertical_first)) * cc) + (ff_right_mcp_add_ics_interchange_vertical_first))) -> (((exists fs_h_mcp_ics_interchange_vertical_first_target. fs_h_mcp_ics_interchange_vertical_first_target + S (ff_target_mcp_add_ics_interchange_vertical_first) = S ((S (ff_index_mcp_add_ics_interchange_vertical_first)) * ec)) /\ exists fs_q_mcp_ics_interchange_vertical_first_target. eb = fs_q_mcp_ics_interchange_vertical_first_target * S ((S (ff_index_mcp_add_ics_interchange_vertical_first)) * ec) + (ff_target_mcp_add_ics_interchange_vertical_first))) -> ff_target_mcp_add_ics_interchange_vertical_first = ff_left_mcp_add_ics_interchange_vertical_first + ff_right_mcp_add_ics_interchange_vertical_first) -> (forall ff_index_mcp_add_ics_interchange_vertical_second ff_left_mcp_add_ics_interchange_vertical_second ff_right_mcp_add_ics_interchange_vertical_second ff_target_mcp_add_ics_interchange_vertical_second. (exists mcp_gap_ics_interchange_vertical_second_bound. mcp_gap_ics_interchange_vertical_second_bound + S (ff_index_mcp_add_ics_interchange_vertical_second) = (l)) -> (((exists fs_h_mcp_ics_interchange_vertical_second_left. fs_h_mcp_ics_interchange_vertical_second_left + S (ff_left_mcp_add_ics_interchange_vertical_second) = S ((S (ff_index_mcp_add_ics_interchange_vertical_second)) * bc)) /\ exists fs_q_mcp_ics_interchange_vertical_second_left. bb = fs_q_mcp_ics_interchange_vertical_second_left * S ((S (ff_index_mcp_add_ics_interchange_vertical_second)) * bc) + (ff_left_mcp_add_ics_interchange_vertical_second))) -> (((exists fs_h_mcp_ics_interchange_vertical_second_right. fs_h_mcp_ics_interchange_vertical_second_right + S (ff_right_mcp_add_ics_interchange_vertical_second) = S ((S (ff_index_mcp_add_ics_interchange_vertical_second)) * dc)) /\ exists fs_q_mcp_ics_interchange_vertical_second_right. db = fs_q_mcp_ics_interchange_vertical_second_right * S ((S (ff_index_mcp_add_ics_interchange_vertical_second)) * dc) + (ff_right_mcp_add_ics_interchange_vertical_second))) -> (((exists fs_h_mcp_ics_interchange_vertical_second_target. fs_h_mcp_ics_interchange_vertical_second_target + S (ff_target_mcp_add_ics_interchange_vertical_second) = S ((S (ff_index_mcp_add_ics_interchange_vertical_second)) * fc)) /\ exists fs_q_mcp_ics_interchange_vertical_second_target. fb = fs_q_mcp_ics_interchange_vertical_second_target * S ((S (ff_index_mcp_add_ics_interchange_vertical_second)) * fc) + (ff_target_mcp_add_ics_interchange_vertical_second))) -> ff_target_mcp_add_ics_interchange_vertical_second = ff_left_mcp_add_ics_interchange_vertical_second + ff_right_mcp_add_ics_interchange_vertical_second) -> (forall ff_index_mcp_add_ics_interchange_result ff_left_mcp_add_ics_interchange_result ff_right_mcp_add_ics_interchange_result ff_target_mcp_add_ics_interchange_result. (exists mcp_gap_ics_interchange_result_bound. mcp_gap_ics_interchange_result_bound + S (ff_index_mcp_add_ics_interchange_result) = (l)) -> (((exists fs_h_mcp_ics_interchange_result_left. fs_h_mcp_ics_interchange_result_left + S (ff_left_mcp_add_ics_interchange_result) = S ((S (ff_index_mcp_add_ics_interchange_result)) * pc)) /\ exists fs_q_mcp_ics_interchange_result_left. pb = fs_q_mcp_ics_interchange_result_left * S ((S (ff_index_mcp_add_ics_interchange_result)) * pc) + (ff_left_mcp_add_ics_interchange_result))) -> (((exists fs_h_mcp_ics_interchange_result_right. fs_h_mcp_ics_interchange_result_right + S (ff_right_mcp_add_ics_interchange_result) = S ((S (ff_index_mcp_add_ics_interchange_result)) * qc)) /\ exists fs_q_mcp_ics_interchange_result_right. qb = fs_q_mcp_ics_interchange_result_right * S ((S (ff_index_mcp_add_ics_interchange_result)) * qc) + (ff_right_mcp_add_ics_interchange_result))) -> (((exists fs_h_mcp_ics_interchange_result_target. fs_h_mcp_ics_interchange_result_target + S (ff_target_mcp_add_ics_interchange_result) = S ((S (ff_index_mcp_add_ics_interchange_result)) * rc)) /\ exists fs_q_mcp_ics_interchange_result_target. rb = fs_q_mcp_ics_interchange_result_target * S ((S (ff_index_mcp_add_ics_interchange_result)) * rc) + (ff_target_mcp_add_ics_interchange_result))) -> ff_target_mcp_add_ics_interchange_result = ff_left_mcp_add_ics_interchange_result + ff_right_mcp_add_ics_interchange_result)
Complete tactic proof in conservative notation
All 131 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.
01Fix variables and assumptionsL1–10
Work with arbitrary variables or the premises of the current implication.