Actual finite dot products add whenever their decoded multiplicands satisfy the displayed pointwise distributive equation; checked finite-sum additivity supplies the full arbitrary-length result.
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 l L M N. (exists ff_code_dot_ics_dot_first ff_scale_dot_ics_dot_first. ((forall fpmp_index_dot_ics_dot_first_pointwise fpmp_left_dot_ics_dot_first_pointwise fpmp_right_dot_ics_dot_first_pointwise fpmp_target_dot_ics_dot_first_pointwise. (exists fpmp_gap_dot_ics_dot_first_pointwise. fpmp_gap_dot_ics_dot_first_pointwise + S fpmp_index_dot_ics_dot_first_pointwise = l) -> (((exists ff_h_fpmp_dot_ics_dot_first_pointwise_left. ff_h_fpmp_dot_ics_dot_first_pointwise_left + S (fpmp_left_dot_ics_dot_first_pointwise) = S ((S (fpmp_index_dot_ics_dot_first_pointwise)) * ac)) /\ exists ff_q_fpmp_dot_ics_dot_first_pointwise_left. ab = ff_q_fpmp_dot_ics_dot_first_pointwise_left * S ((S (fpmp_index_dot_ics_dot_first_pointwise)) * ac) + (fpmp_left_dot_ics_dot_first_pointwise))) -> (((exists ff_h_fpmp_dot_ics_dot_first_pointwise_right. ff_h_fpmp_dot_ics_dot_first_pointwise_right + S (fpmp_right_dot_ics_dot_first_pointwise) = S ((S (fpmp_index_dot_ics_dot_first_pointwise)) * bc)) /\ exists ff_q_fpmp_dot_ics_dot_first_pointwise_right. bb = ff_q_fpmp_dot_ics_dot_first_pointwise_right * S ((S (fpmp_index_dot_ics_dot_first_pointwise)) * bc) + (fpmp_right_dot_ics_dot_first_pointwise))) -> (((exists ff_h_fpmp_dot_ics_dot_first_pointwise_target. ff_h_fpmp_dot_ics_dot_first_pointwise_target + S (fpmp_target_dot_ics_dot_first_pointwise) = S ((S (fpmp_index_dot_ics_dot_first_pointwise)) * ff_scale_dot_ics_dot_first)) /\ exists ff_q_fpmp_dot_ics_dot_first_pointwise_target. ff_code_dot_ics_dot_first = ff_q_fpmp_dot_ics_dot_first_pointwise_target * S ((S (fpmp_index_dot_ics_dot_first_pointwise)) * ff_scale_dot_ics_dot_first) + (fpmp_target_dot_ics_dot_first_pointwise))) -> fpmp_target_dot_ics_dot_first_pointwise = fpmp_left_dot_ics_dot_first_pointwise * fpmp_right_dot_ics_dot_first_pointwise) /\ (exists ff_u_dot_ics_dot_first_sum ff_v_dot_ics_dot_first_sum. ((((exists ff_h_dot_ics_dot_first_sum_start. ff_h_dot_ics_dot_first_sum_start + S (0) = S ((S (0)) * ff_v_dot_ics_dot_first_sum)) /\ exists ff_q_dot_ics_dot_first_sum_start. ff_u_dot_ics_dot_first_sum = ff_q_dot_ics_dot_first_sum_start * S ((S (0)) * ff_v_dot_ics_dot_first_sum) + (0))) /\ ((((exists ff_h_dot_ics_dot_first_sum_terminal. ff_h_dot_ics_dot_first_sum_terminal + S (L) = S ((S (l)) * ff_v_dot_ics_dot_first_sum)) /\ exists ff_q_dot_ics_dot_first_sum_terminal. ff_u_dot_ics_dot_first_sum = ff_q_dot_ics_dot_first_sum_terminal * S ((S (l)) * ff_v_dot_ics_dot_first_sum) + (L))) /\ forall ff_i_dot_ics_dot_first_sum. (exists ff_lt_dot_ics_dot_first_sum_bound. ff_lt_dot_ics_dot_first_sum_bound + S ff_i_dot_ics_dot_first_sum = l) -> exists ff_a_dot_ics_dot_first_sum ff_r_dot_ics_dot_first_sum ff_s_dot_ics_dot_first_sum. ((((exists ff_h_dot_ics_dot_first_sum_summand. ff_h_dot_ics_dot_first_sum_summand + S (ff_a_dot_ics_dot_first_sum) = S ((S (ff_i_dot_ics_dot_first_sum)) * ff_scale_dot_ics_dot_first)) /\ exists ff_q_dot_ics_dot_first_sum_summand. ff_code_dot_ics_dot_first = ff_q_dot_ics_dot_first_sum_summand * S ((S (ff_i_dot_ics_dot_first_sum)) * ff_scale_dot_ics_dot_first) + (ff_a_dot_ics_dot_first_sum))) /\ ((((exists ff_h_dot_ics_dot_first_sum_partial. ff_h_dot_ics_dot_first_sum_partial + S (ff_r_dot_ics_dot_first_sum) = S ((S (ff_i_dot_ics_dot_first_sum)) * ff_v_dot_ics_dot_first_sum)) /\ exists ff_q_dot_ics_dot_first_sum_partial. ff_u_dot_ics_dot_first_sum = ff_q_dot_ics_dot_first_sum_partial * S ((S (ff_i_dot_ics_dot_first_sum)) * ff_v_dot_ics_dot_first_sum) + (ff_r_dot_ics_dot_first_sum))) /\ ((((exists ff_h_dot_ics_dot_first_sum_successor. ff_h_dot_ics_dot_first_sum_successor + S (ff_s_dot_ics_dot_first_sum) = S ((S (S ff_i_dot_ics_dot_first_sum)) * ff_v_dot_ics_dot_first_sum)) /\ exists ff_q_dot_ics_dot_first_sum_successor. ff_u_dot_ics_dot_first_sum = ff_q_dot_ics_dot_first_sum_successor * S ((S (S ff_i_dot_ics_dot_first_sum)) * ff_v_dot_ics_dot_first_sum) + (ff_s_dot_ics_dot_first_sum))) /\ ff_s_dot_ics_dot_first_sum = ff_r_dot_ics_dot_first_sum + ff_a_dot_ics_dot_first_sum)))))))) -> (exists ff_code_dot_ics_dot_second ff_scale_dot_ics_dot_second. ((forall fpmp_index_dot_ics_dot_second_pointwise fpmp_left_dot_ics_dot_second_pointwise fpmp_right_dot_ics_dot_second_pointwise fpmp_target_dot_ics_dot_second_pointwise. (exists fpmp_gap_dot_ics_dot_second_pointwise. fpmp_gap_dot_ics_dot_second_pointwise + S fpmp_index_dot_ics_dot_second_pointwise = l) -> (((exists ff_h_fpmp_dot_ics_dot_second_pointwise_left. ff_h_fpmp_dot_ics_dot_second_pointwise_left + S (fpmp_left_dot_ics_dot_second_pointwise) = S ((S (fpmp_index_dot_ics_dot_second_pointwise)) * cc)) /\ exists ff_q_fpmp_dot_ics_dot_second_pointwise_left. cb = ff_q_fpmp_dot_ics_dot_second_pointwise_left * S ((S (fpmp_index_dot_ics_dot_second_pointwise)) * cc) + (fpmp_left_dot_ics_dot_second_pointwise))) -> (((exists ff_h_fpmp_dot_ics_dot_second_pointwise_right. ff_h_fpmp_dot_ics_dot_second_pointwise_right + S (fpmp_right_dot_ics_dot_second_pointwise) = S ((S (fpmp_index_dot_ics_dot_second_pointwise)) * dc)) /\ exists ff_q_fpmp_dot_ics_dot_second_pointwise_right. db = ff_q_fpmp_dot_ics_dot_second_pointwise_right * S ((S (fpmp_index_dot_ics_dot_second_pointwise)) * dc) + (fpmp_right_dot_ics_dot_second_pointwise))) -> (((exists ff_h_fpmp_dot_ics_dot_second_pointwise_target. ff_h_fpmp_dot_ics_dot_second_pointwise_target + S (fpmp_target_dot_ics_dot_second_pointwise) = S ((S (fpmp_index_dot_ics_dot_second_pointwise)) * ff_scale_dot_ics_dot_second)) /\ exists ff_q_fpmp_dot_ics_dot_second_pointwise_target. ff_code_dot_ics_dot_second = ff_q_fpmp_dot_ics_dot_second_pointwise_target * S ((S (fpmp_index_dot_ics_dot_second_pointwise)) * ff_scale_dot_ics_dot_second) + (fpmp_target_dot_ics_dot_second_pointwise))) -> fpmp_target_dot_ics_dot_second_pointwise = fpmp_left_dot_ics_dot_second_pointwise * fpmp_right_dot_ics_dot_second_pointwise) /\ (exists ff_u_dot_ics_dot_second_sum ff_v_dot_ics_dot_second_sum. ((((exists ff_h_dot_ics_dot_second_sum_start. ff_h_dot_ics_dot_second_sum_start + S (0) = S ((S (0)) * ff_v_dot_ics_dot_second_sum)) /\ exists ff_q_dot_ics_dot_second_sum_start. ff_u_dot_ics_dot_second_sum = ff_q_dot_ics_dot_second_sum_start * S ((S (0)) * ff_v_dot_ics_dot_second_sum) + (0))) /\ ((((exists ff_h_dot_ics_dot_second_sum_terminal. ff_h_dot_ics_dot_second_sum_terminal + S (M) = S ((S (l)) * ff_v_dot_ics_dot_second_sum)) /\ exists ff_q_dot_ics_dot_second_sum_terminal. ff_u_dot_ics_dot_second_sum = ff_q_dot_ics_dot_second_sum_terminal * S ((S (l)) * ff_v_dot_ics_dot_second_sum) + (M))) /\ forall ff_i_dot_ics_dot_second_sum. (exists ff_lt_dot_ics_dot_second_sum_bound. ff_lt_dot_ics_dot_second_sum_bound + S ff_i_dot_ics_dot_second_sum = l) -> exists ff_a_dot_ics_dot_second_sum ff_r_dot_ics_dot_second_sum ff_s_dot_ics_dot_second_sum. ((((exists ff_h_dot_ics_dot_second_sum_summand. ff_h_dot_ics_dot_second_sum_summand + S (ff_a_dot_ics_dot_second_sum) = S ((S (ff_i_dot_ics_dot_second_sum)) * ff_scale_dot_ics_dot_second)) /\ exists ff_q_dot_ics_dot_second_sum_summand. ff_code_dot_ics_dot_second = ff_q_dot_ics_dot_second_sum_summand * S ((S (ff_i_dot_ics_dot_second_sum)) * ff_scale_dot_ics_dot_second) + (ff_a_dot_ics_dot_second_sum))) /\ ((((exists ff_h_dot_ics_dot_second_sum_partial. ff_h_dot_ics_dot_second_sum_partial + S (ff_r_dot_ics_dot_second_sum) = S ((S (ff_i_dot_ics_dot_second_sum)) * ff_v_dot_ics_dot_second_sum)) /\ exists ff_q_dot_ics_dot_second_sum_partial. ff_u_dot_ics_dot_second_sum = ff_q_dot_ics_dot_second_sum_partial * S ((S (ff_i_dot_ics_dot_second_sum)) * ff_v_dot_ics_dot_second_sum) + (ff_r_dot_ics_dot_second_sum))) /\ ((((exists ff_h_dot_ics_dot_second_sum_successor. ff_h_dot_ics_dot_second_sum_successor + S (ff_s_dot_ics_dot_second_sum) = S ((S (S ff_i_dot_ics_dot_second_sum)) * ff_v_dot_ics_dot_second_sum)) /\ exists ff_q_dot_ics_dot_second_sum_successor. ff_u_dot_ics_dot_second_sum = ff_q_dot_ics_dot_second_sum_successor * S ((S (S ff_i_dot_ics_dot_second_sum)) * ff_v_dot_ics_dot_second_sum) + (ff_s_dot_ics_dot_second_sum))) /\ ff_s_dot_ics_dot_second_sum = ff_r_dot_ics_dot_second_sum + ff_a_dot_ics_dot_second_sum)))))))) -> (exists ff_code_dot_ics_dot_third ff_scale_dot_ics_dot_third. ((forall fpmp_index_dot_ics_dot_third_pointwise fpmp_left_dot_ics_dot_third_pointwise fpmp_right_dot_ics_dot_third_pointwise fpmp_target_dot_ics_dot_third_pointwise. (exists fpmp_gap_dot_ics_dot_third_pointwise. fpmp_gap_dot_ics_dot_third_pointwise + S fpmp_index_dot_ics_dot_third_pointwise = l) -> (((exists ff_h_fpmp_dot_ics_dot_third_pointwise_left. ff_h_fpmp_dot_ics_dot_third_pointwise_left + S (fpmp_left_dot_ics_dot_third_pointwise) = S ((S (fpmp_index_dot_ics_dot_third_pointwise)) * ec)) /\ exists ff_q_fpmp_dot_ics_dot_third_pointwise_left. eb = ff_q_fpmp_dot_ics_dot_third_pointwise_left * S ((S (fpmp_index_dot_ics_dot_third_pointwise)) * ec) + (fpmp_left_dot_ics_dot_third_pointwise))) -> (((exists ff_h_fpmp_dot_ics_dot_third_pointwise_right. ff_h_fpmp_dot_ics_dot_third_pointwise_right + S (fpmp_right_dot_ics_dot_third_pointwise) = S ((S (fpmp_index_dot_ics_dot_third_pointwise)) * fc)) /\ exists ff_q_fpmp_dot_ics_dot_third_pointwise_right. fb = ff_q_fpmp_dot_ics_dot_third_pointwise_right * S ((S (fpmp_index_dot_ics_dot_third_pointwise)) * fc) + (fpmp_right_dot_ics_dot_third_pointwise))) -> (((exists ff_h_fpmp_dot_ics_dot_third_pointwise_target. ff_h_fpmp_dot_ics_dot_third_pointwise_target + S (fpmp_target_dot_ics_dot_third_pointwise) = S ((S (fpmp_index_dot_ics_dot_third_pointwise)) * ff_scale_dot_ics_dot_third)) /\ exists ff_q_fpmp_dot_ics_dot_third_pointwise_target. ff_code_dot_ics_dot_third = ff_q_fpmp_dot_ics_dot_third_pointwise_target * S ((S (fpmp_index_dot_ics_dot_third_pointwise)) * ff_scale_dot_ics_dot_third) + (fpmp_target_dot_ics_dot_third_pointwise))) -> fpmp_target_dot_ics_dot_third_pointwise = fpmp_left_dot_ics_dot_third_pointwise * fpmp_right_dot_ics_dot_third_pointwise) /\ (exists ff_u_dot_ics_dot_third_sum ff_v_dot_ics_dot_third_sum. ((((exists ff_h_dot_ics_dot_third_sum_start. ff_h_dot_ics_dot_third_sum_start + S (0) = S ((S (0)) * ff_v_dot_ics_dot_third_sum)) /\ exists ff_q_dot_ics_dot_third_sum_start. ff_u_dot_ics_dot_third_sum = ff_q_dot_ics_dot_third_sum_start * S ((S (0)) * ff_v_dot_ics_dot_third_sum) + (0))) /\ ((((exists ff_h_dot_ics_dot_third_sum_terminal. ff_h_dot_ics_dot_third_sum_terminal + S (N) = S ((S (l)) * ff_v_dot_ics_dot_third_sum)) /\ exists ff_q_dot_ics_dot_third_sum_terminal. ff_u_dot_ics_dot_third_sum = ff_q_dot_ics_dot_third_sum_terminal * S ((S (l)) * ff_v_dot_ics_dot_third_sum) + (N))) /\ forall ff_i_dot_ics_dot_third_sum. (exists ff_lt_dot_ics_dot_third_sum_bound. ff_lt_dot_ics_dot_third_sum_bound + S ff_i_dot_ics_dot_third_sum = l) -> exists ff_a_dot_ics_dot_third_sum ff_r_dot_ics_dot_third_sum ff_s_dot_ics_dot_third_sum. ((((exists ff_h_dot_ics_dot_third_sum_summand. ff_h_dot_ics_dot_third_sum_summand + S (ff_a_dot_ics_dot_third_sum) = S ((S (ff_i_dot_ics_dot_third_sum)) * ff_scale_dot_ics_dot_third)) /\ exists ff_q_dot_ics_dot_third_sum_summand. ff_code_dot_ics_dot_third = ff_q_dot_ics_dot_third_sum_summand * S ((S (ff_i_dot_ics_dot_third_sum)) * ff_scale_dot_ics_dot_third) + (ff_a_dot_ics_dot_third_sum))) /\ ((((exists ff_h_dot_ics_dot_third_sum_partial. ff_h_dot_ics_dot_third_sum_partial + S (ff_r_dot_ics_dot_third_sum) = S ((S (ff_i_dot_ics_dot_third_sum)) * ff_v_dot_ics_dot_third_sum)) /\ exists ff_q_dot_ics_dot_third_sum_partial. ff_u_dot_ics_dot_third_sum = ff_q_dot_ics_dot_third_sum_partial * S ((S (ff_i_dot_ics_dot_third_sum)) * ff_v_dot_ics_dot_third_sum) + (ff_r_dot_ics_dot_third_sum))) /\ ((((exists ff_h_dot_ics_dot_third_sum_successor. ff_h_dot_ics_dot_third_sum_successor + S (ff_s_dot_ics_dot_third_sum) = S ((S (S ff_i_dot_ics_dot_third_sum)) * ff_v_dot_ics_dot_third_sum)) /\ exists ff_q_dot_ics_dot_third_sum_successor. ff_u_dot_ics_dot_third_sum = ff_q_dot_ics_dot_third_sum_successor * S ((S (S ff_i_dot_ics_dot_third_sum)) * ff_v_dot_ics_dot_third_sum) + (ff_s_dot_ics_dot_third_sum))) /\ ff_s_dot_ics_dot_third_sum = ff_r_dot_ics_dot_third_sum + ff_a_dot_ics_dot_third_sum)))))))) -> (forall ics_index_dot_alignment ics_value0_dot_alignment ics_value1_dot_alignment ics_value2_dot_alignment ics_value3_dot_alignment ics_value4_dot_alignment ics_value5_dot_alignment. (exists ics_gap_dot_alignment_bound. ics_gap_dot_alignment_bound + S (ics_index_dot_alignment) = (l)) -> (((exists fs_h_ics_dot_alignment_at0. fs_h_ics_dot_alignment_at0 + S (ics_value0_dot_alignment) = S ((S (ics_index_dot_alignment)) * ac)) /\ exists fs_q_ics_dot_alignment_at0. ab = fs_q_ics_dot_alignment_at0 * S ((S (ics_index_dot_alignment)) * ac) + (ics_value0_dot_alignment))) -> (((exists fs_h_ics_dot_alignment_at1. fs_h_ics_dot_alignment_at1 + S (ics_value1_dot_alignment) = S ((S (ics_index_dot_alignment)) * bc)) /\ exists fs_q_ics_dot_alignment_at1. bb = fs_q_ics_dot_alignment_at1 * S ((S (ics_index_dot_alignment)) * bc) + (ics_value1_dot_alignment))) -> (((exists fs_h_ics_dot_alignment_at2. fs_h_ics_dot_alignment_at2 + S (ics_value2_dot_alignment) = S ((S (ics_index_dot_alignment)) * cc)) /\ exists fs_q_ics_dot_alignment_at2. cb = fs_q_ics_dot_alignment_at2 * S ((S (ics_index_dot_alignment)) * cc) + (ics_value2_dot_alignment))) -> (((exists fs_h_ics_dot_alignment_at3. fs_h_ics_dot_alignment_at3 + S (ics_value3_dot_alignment) = S ((S (ics_index_dot_alignment)) * dc)) /\ exists fs_q_ics_dot_alignment_at3. db = fs_q_ics_dot_alignment_at3 * S ((S (ics_index_dot_alignment)) * dc) + (ics_value3_dot_alignment))) -> (((exists fs_h_ics_dot_alignment_at4. fs_h_ics_dot_alignment_at4 + S (ics_value4_dot_alignment) = S ((S (ics_index_dot_alignment)) * ec)) /\ exists fs_q_ics_dot_alignment_at4. eb = fs_q_ics_dot_alignment_at4 * S ((S (ics_index_dot_alignment)) * ec) + (ics_value4_dot_alignment))) -> (((exists fs_h_ics_dot_alignment_at5. fs_h_ics_dot_alignment_at5 + S (ics_value5_dot_alignment) = S ((S (ics_index_dot_alignment)) * fc)) /\ exists fs_q_ics_dot_alignment_at5. fb = fs_q_ics_dot_alignment_at5 * S ((S (ics_index_dot_alignment)) * fc) + (ics_value5_dot_alignment))) -> ics_value4_dot_alignment * ics_value5_dot_alignment = ics_value0_dot_alignment * ics_value1_dot_alignment + ics_value2_dot_alignment * ics_value3_dot_alignment) -> L + M = N
Complete tactic proof in conservative notation
All 136 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.