Integer-vector addition respects genuine signed-difference equality of both inputs, not merely recoding of equal natural components.
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 db dc eb ec fb fc pb pc nb nc qb qc mb mc rb rc sb sc l. (forall ics_index_add_transport_first ics_value0_add_transport_first ics_value1_add_transport_first ics_value2_add_transport_first ics_value3_add_transport_first. (exists ics_gap_add_transport_first_bound. ics_gap_add_transport_first_bound + S (ics_index_add_transport_first) = (l)) -> (((exists fs_h_ics_add_transport_first_at0. fs_h_ics_add_transport_first_at0 + S (ics_value0_add_transport_first) = S ((S (ics_index_add_transport_first)) * ac)) /\ exists fs_q_ics_add_transport_first_at0. ab = fs_q_ics_add_transport_first_at0 * S ((S (ics_index_add_transport_first)) * ac) + (ics_value0_add_transport_first))) -> (((exists fs_h_ics_add_transport_first_at1. fs_h_ics_add_transport_first_at1 + S (ics_value1_add_transport_first) = S ((S (ics_index_add_transport_first)) * dc)) /\ exists fs_q_ics_add_transport_first_at1. db = fs_q_ics_add_transport_first_at1 * S ((S (ics_index_add_transport_first)) * dc) + (ics_value1_add_transport_first))) -> (((exists fs_h_ics_add_transport_first_at2. fs_h_ics_add_transport_first_at2 + S (ics_value2_add_transport_first) = S ((S (ics_index_add_transport_first)) * pc)) /\ exists fs_q_ics_add_transport_first_at2. pb = fs_q_ics_add_transport_first_at2 * S ((S (ics_index_add_transport_first)) * pc) + (ics_value2_add_transport_first))) -> (((exists fs_h_ics_add_transport_first_at3. fs_h_ics_add_transport_first_at3 + S (ics_value3_add_transport_first) = S ((S (ics_index_add_transport_first)) * nc)) /\ exists fs_q_ics_add_transport_first_at3. nb = fs_q_ics_add_transport_first_at3 * S ((S (ics_index_add_transport_first)) * nc) + (ics_value3_add_transport_first))) -> ics_value0_add_transport_first + ics_value3_add_transport_first = ics_value2_add_transport_first + ics_value1_add_transport_first) -> (forall ics_index_add_transport_second ics_value0_add_transport_second ics_value1_add_transport_second ics_value2_add_transport_second ics_value3_add_transport_second. (exists ics_gap_add_transport_second_bound. ics_gap_add_transport_second_bound + S (ics_index_add_transport_second) = (l)) -> (((exists fs_h_ics_add_transport_second_at0. fs_h_ics_add_transport_second_at0 + S (ics_value0_add_transport_second) = S ((S (ics_index_add_transport_second)) * ec)) /\ exists fs_q_ics_add_transport_second_at0. eb = fs_q_ics_add_transport_second_at0 * S ((S (ics_index_add_transport_second)) * ec) + (ics_value0_add_transport_second))) -> (((exists fs_h_ics_add_transport_second_at1. fs_h_ics_add_transport_second_at1 + S (ics_value1_add_transport_second) = S ((S (ics_index_add_transport_second)) * fc)) /\ exists fs_q_ics_add_transport_second_at1. fb = fs_q_ics_add_transport_second_at1 * S ((S (ics_index_add_transport_second)) * fc) + (ics_value1_add_transport_second))) -> (((exists fs_h_ics_add_transport_second_at2. fs_h_ics_add_transport_second_at2 + S (ics_value2_add_transport_second) = S ((S (ics_index_add_transport_second)) * qc)) /\ exists fs_q_ics_add_transport_second_at2. qb = fs_q_ics_add_transport_second_at2 * S ((S (ics_index_add_transport_second)) * qc) + (ics_value2_add_transport_second))) -> (((exists fs_h_ics_add_transport_second_at3. fs_h_ics_add_transport_second_at3 + S (ics_value3_add_transport_second) = S ((S (ics_index_add_transport_second)) * mc)) /\ exists fs_q_ics_add_transport_second_at3. mb = fs_q_ics_add_transport_second_at3 * S ((S (ics_index_add_transport_second)) * mc) + (ics_value3_add_transport_second))) -> ics_value0_add_transport_second + ics_value3_add_transport_second = ics_value2_add_transport_second + ics_value1_add_transport_second) -> (forall ics_index_add_transport_source ics_value0_add_transport_source ics_value1_add_transport_source ics_value2_add_transport_source ics_value3_add_transport_source ics_value4_add_transport_source ics_value5_add_transport_source. (exists ics_gap_add_transport_source_bound. ics_gap_add_transport_source_bound + S (ics_index_add_transport_source) = (l)) -> (((exists fs_h_ics_add_transport_source_at0. fs_h_ics_add_transport_source_at0 + S (ics_value0_add_transport_source) = S ((S (ics_index_add_transport_source)) * ac)) /\ exists fs_q_ics_add_transport_source_at0. ab = fs_q_ics_add_transport_source_at0 * S ((S (ics_index_add_transport_source)) * ac) + (ics_value0_add_transport_source))) -> (((exists fs_h_ics_add_transport_source_at1. fs_h_ics_add_transport_source_at1 + S (ics_value1_add_transport_source) = S ((S (ics_index_add_transport_source)) * dc)) /\ exists fs_q_ics_add_transport_source_at1. db = fs_q_ics_add_transport_source_at1 * S ((S (ics_index_add_transport_source)) * dc) + (ics_value1_add_transport_source))) -> (((exists fs_h_ics_add_transport_source_at2. fs_h_ics_add_transport_source_at2 + S (ics_value2_add_transport_source) = S ((S (ics_index_add_transport_source)) * ec)) /\ exists fs_q_ics_add_transport_source_at2. eb = fs_q_ics_add_transport_source_at2 * S ((S (ics_index_add_transport_source)) * ec) + (ics_value2_add_transport_source))) -> (((exists fs_h_ics_add_transport_source_at3. fs_h_ics_add_transport_source_at3 + S (ics_value3_add_transport_source) = S ((S (ics_index_add_transport_source)) * fc)) /\ exists fs_q_ics_add_transport_source_at3. fb = fs_q_ics_add_transport_source_at3 * S ((S (ics_index_add_transport_source)) * fc) + (ics_value3_add_transport_source))) -> (((exists fs_h_ics_add_transport_source_at4. fs_h_ics_add_transport_source_at4 + S (ics_value4_add_transport_source) = S ((S (ics_index_add_transport_source)) * rc)) /\ exists fs_q_ics_add_transport_source_at4. rb = fs_q_ics_add_transport_source_at4 * S ((S (ics_index_add_transport_source)) * rc) + (ics_value4_add_transport_source))) -> (((exists fs_h_ics_add_transport_source_at5. fs_h_ics_add_transport_source_at5 + S (ics_value5_add_transport_source) = S ((S (ics_index_add_transport_source)) * sc)) /\ exists fs_q_ics_add_transport_source_at5. sb = fs_q_ics_add_transport_source_at5 * S ((S (ics_index_add_transport_source)) * sc) + (ics_value5_add_transport_source))) -> ics_value4_add_transport_source + (ics_value1_add_transport_source + ics_value3_add_transport_source) = (ics_value0_add_transport_source + ics_value2_add_transport_source) + ics_value5_add_transport_source) -> (forall ics_index_add_transport_result ics_value0_add_transport_result ics_value1_add_transport_result ics_value2_add_transport_result ics_value3_add_transport_result ics_value4_add_transport_result ics_value5_add_transport_result. (exists ics_gap_add_transport_result_bound. ics_gap_add_transport_result_bound + S (ics_index_add_transport_result) = (l)) -> (((exists fs_h_ics_add_transport_result_at0. fs_h_ics_add_transport_result_at0 + S (ics_value0_add_transport_result) = S ((S (ics_index_add_transport_result)) * pc)) /\ exists fs_q_ics_add_transport_result_at0. pb = fs_q_ics_add_transport_result_at0 * S ((S (ics_index_add_transport_result)) * pc) + (ics_value0_add_transport_result))) -> (((exists fs_h_ics_add_transport_result_at1. fs_h_ics_add_transport_result_at1 + S (ics_value1_add_transport_result) = S ((S (ics_index_add_transport_result)) * nc)) /\ exists fs_q_ics_add_transport_result_at1. nb = fs_q_ics_add_transport_result_at1 * S ((S (ics_index_add_transport_result)) * nc) + (ics_value1_add_transport_result))) -> (((exists fs_h_ics_add_transport_result_at2. fs_h_ics_add_transport_result_at2 + S (ics_value2_add_transport_result) = S ((S (ics_index_add_transport_result)) * qc)) /\ exists fs_q_ics_add_transport_result_at2. qb = fs_q_ics_add_transport_result_at2 * S ((S (ics_index_add_transport_result)) * qc) + (ics_value2_add_transport_result))) -> (((exists fs_h_ics_add_transport_result_at3. fs_h_ics_add_transport_result_at3 + S (ics_value3_add_transport_result) = S ((S (ics_index_add_transport_result)) * mc)) /\ exists fs_q_ics_add_transport_result_at3. mb = fs_q_ics_add_transport_result_at3 * S ((S (ics_index_add_transport_result)) * mc) + (ics_value3_add_transport_result))) -> (((exists fs_h_ics_add_transport_result_at4. fs_h_ics_add_transport_result_at4 + S (ics_value4_add_transport_result) = S ((S (ics_index_add_transport_result)) * rc)) /\ exists fs_q_ics_add_transport_result_at4. rb = fs_q_ics_add_transport_result_at4 * S ((S (ics_index_add_transport_result)) * rc) + (ics_value4_add_transport_result))) -> (((exists fs_h_ics_add_transport_result_at5. fs_h_ics_add_transport_result_at5 + S (ics_value5_add_transport_result) = S ((S (ics_index_add_transport_result)) * sc)) /\ exists fs_q_ics_add_transport_result_at5. sb = fs_q_ics_add_transport_result_at5 * S ((S (ics_index_add_transport_result)) * sc) + (ics_value5_add_transport_result))) -> ics_value4_add_transport_result + (ics_value1_add_transport_result + ics_value3_add_transport_result) = (ics_value0_add_transport_result + ics_value2_add_transport_result) + ics_value5_add_transport_result)
Complete tactic proof in conservative notation
All 115 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.