SS0014 — divisor_signed_sum_extensional

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

These are actual signed-table and finite-sum foundations. Equality compares represented signed values, not arbitrary encodings. MatrixMinorFourCode is reused solely as generic nested pairing, without a matrix hypothesis. Full finite signed G007 is established separately in the Möbius-inversion family.

Exact theorem in conservative defined notation

∀ F. ∀ G. ∀ l. ∀ a. ∀ b. ArithTableEqual(F,G,l) → SignedPrefixSum(F,l,a) → SignedPrefixSum(G,l,b) → a = b

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

SignedPrefixSum(F,l,z) · 2 ArithTableEqual(F,G,l) · 1

Actual proof prerequisites

divisor_signed_table_equality_component_balance matrix_integer_signed_sum_balance · checked external prerequisite signed_balance_extensional · checked external prerequisite add_comm · checked external prerequisite

Original expanded first-order statement

forall F G l a b. (forall dst_index_sum_ext_entries dst_first_sum_ext_entries dst_second_sum_ext_entries. (exists pvs_gap_sum_ext_entriesbound. pvs_gap_sum_ext_entriesbound + S (dst_index_sum_ext_entries) = (l)) -> (exists dst_positive_code_sum_ext_entriesfirst dst_positive_scale_sum_ext_entriesfirst dst_negative_code_sum_ext_entriesfirst dst_negative_scale_sum_ext_entriesfirst dst_positive_sum_ext_entriesfirst dst_negative_sum_ext_entriesfirst. (((F) = (((((dst_positive_code_sum_ext_entriesfirst) + (dst_positive_scale_sum_ext_entriesfirst)) * S ((dst_positive_code_sum_ext_entriesfirst) + (dst_positive_scale_sum_ext_entriesfirst)) + ((dst_positive_scale_sum_ext_entriesfirst) + (dst_positive_scale_sum_ext_entriesfirst))) + (((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) * S ((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) + ((dst_negative_scale_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)))) * S ((((dst_positive_code_sum_ext_entriesfirst) + (dst_positive_scale_sum_ext_entriesfirst)) * S ((dst_positive_code_sum_ext_entriesfirst) + (dst_positive_scale_sum_ext_entriesfirst)) + ((dst_positive_scale_sum_ext_entriesfirst) + (dst_positive_scale_sum_ext_entriesfirst))) + (((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) * S ((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) + ((dst_negative_scale_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)))) + ((((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) * S ((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) + ((dst_negative_scale_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst))) + (((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) * S ((dst_negative_code_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)) + ((dst_negative_scale_sum_ext_entriesfirst) + (dst_negative_scale_sum_ext_entriesfirst)))))) /\ (((((exists ff_h_pvs_sum_ext_entriesfirstpositive. ff_h_pvs_sum_ext_entriesfirstpositive + S (dst_positive_sum_ext_entriesfirst) = S ((S (dst_index_sum_ext_entries)) * dst_positive_scale_sum_ext_entriesfirst)) /\ exists ff_q_pvs_sum_ext_entriesfirstpositive. dst_positive_code_sum_ext_entriesfirst = ff_q_pvs_sum_ext_entriesfirstpositive * S ((S (dst_index_sum_ext_entries)) * dst_positive_scale_sum_ext_entriesfirst) + (dst_positive_sum_ext_entriesfirst))) /\ (((((exists ff_h_pvs_sum_ext_entriesfirstnegative. ff_h_pvs_sum_ext_entriesfirstnegative + S (dst_negative_sum_ext_entriesfirst) = S ((S (dst_index_sum_ext_entries)) * dst_negative_scale_sum_ext_entriesfirst)) /\ exists ff_q_pvs_sum_ext_entriesfirstnegative. dst_negative_code_sum_ext_entriesfirst = ff_q_pvs_sum_ext_entriesfirstnegative * S ((S (dst_index_sum_ext_entries)) * dst_negative_scale_sum_ext_entriesfirst) + (dst_negative_sum_ext_entriesfirst))) /\ (exists ge_balance_positive_sum_ext_entriesfirstvalue ge_balance_negative_sum_ext_entriesfirstvalue. (((((dst_first_sum_ext_entries) = 2 * (ge_balance_positive_sum_ext_entriesfirstvalue) /\ (ge_balance_negative_sum_ext_entriesfirstvalue) = 0) \/ exists ge_signed_half_sum_ext_entriesfirstvaluedecode. (((dst_first_sum_ext_entries) = 2 * ge_signed_half_sum_ext_entriesfirstvaluedecode + 1 /\ (ge_balance_positive_sum_ext_entriesfirstvalue) = 0) /\ (ge_balance_negative_sum_ext_entriesfirstvalue) = S ge_signed_half_sum_ext_entriesfirstvaluedecode))) /\ ((dst_positive_sum_ext_entriesfirst) + ge_balance_negative_sum_ext_entriesfirstvalue = (dst_negative_sum_ext_entriesfirst) + ge_balance_positive_sum_ext_entriesfirstvalue))))))))) -> (exists dst_positive_code_sum_ext_entriessecond dst_positive_scale_sum_ext_entriessecond dst_negative_code_sum_ext_entriessecond dst_negative_scale_sum_ext_entriessecond dst_positive_sum_ext_entriessecond dst_negative_sum_ext_entriessecond. (((G) = (((((dst_positive_code_sum_ext_entriessecond) + (dst_positive_scale_sum_ext_entriessecond)) * S ((dst_positive_code_sum_ext_entriessecond) + (dst_positive_scale_sum_ext_entriessecond)) + ((dst_positive_scale_sum_ext_entriessecond) + (dst_positive_scale_sum_ext_entriessecond))) + (((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) * S ((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) + ((dst_negative_scale_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)))) * S ((((dst_positive_code_sum_ext_entriessecond) + (dst_positive_scale_sum_ext_entriessecond)) * S ((dst_positive_code_sum_ext_entriessecond) + (dst_positive_scale_sum_ext_entriessecond)) + ((dst_positive_scale_sum_ext_entriessecond) + (dst_positive_scale_sum_ext_entriessecond))) + (((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) * S ((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) + ((dst_negative_scale_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)))) + ((((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) * S ((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) + ((dst_negative_scale_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond))) + (((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) * S ((dst_negative_code_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)) + ((dst_negative_scale_sum_ext_entriessecond) + (dst_negative_scale_sum_ext_entriessecond)))))) /\ (((((exists ff_h_pvs_sum_ext_entriessecondpositive. ff_h_pvs_sum_ext_entriessecondpositive + S (dst_positive_sum_ext_entriessecond) = S ((S (dst_index_sum_ext_entries)) * dst_positive_scale_sum_ext_entriessecond)) /\ exists ff_q_pvs_sum_ext_entriessecondpositive. dst_positive_code_sum_ext_entriessecond = ff_q_pvs_sum_ext_entriessecondpositive * S ((S (dst_index_sum_ext_entries)) * dst_positive_scale_sum_ext_entriessecond) + (dst_positive_sum_ext_entriessecond))) /\ (((((exists ff_h_pvs_sum_ext_entriessecondnegative. ff_h_pvs_sum_ext_entriessecondnegative + S (dst_negative_sum_ext_entriessecond) = S ((S (dst_index_sum_ext_entries)) * dst_negative_scale_sum_ext_entriessecond)) /\ exists ff_q_pvs_sum_ext_entriessecondnegative. dst_negative_code_sum_ext_entriessecond = ff_q_pvs_sum_ext_entriessecondnegative * S ((S (dst_index_sum_ext_entries)) * dst_negative_scale_sum_ext_entriessecond) + (dst_negative_sum_ext_entriessecond))) /\ (exists ge_balance_positive_sum_ext_entriessecondvalue ge_balance_negative_sum_ext_entriessecondvalue. (((((dst_second_sum_ext_entries) = 2 * (ge_balance_positive_sum_ext_entriessecondvalue) /\ (ge_balance_negative_sum_ext_entriessecondvalue) = 0) \/ exists ge_signed_half_sum_ext_entriessecondvaluedecode. (((dst_second_sum_ext_entries) = 2 * ge_signed_half_sum_ext_entriessecondvaluedecode + 1 /\ (ge_balance_positive_sum_ext_entriessecondvalue) = 0) /\ (ge_balance_negative_sum_ext_entriessecondvalue) = S ge_signed_half_sum_ext_entriessecondvaluedecode))) /\ ((dst_positive_sum_ext_entriessecond) + ge_balance_negative_sum_ext_entriessecondvalue = (dst_negative_sum_ext_entriessecond) + ge_balance_positive_sum_ext_entriessecondvalue))))))))) -> dst_first_sum_ext_entries = dst_second_sum_ext_entries) -> (exists dst_positive_code_sum_ext_first dst_positive_scale_sum_ext_first dst_negative_code_sum_ext_first dst_negative_scale_sum_ext_first dst_positive_sum_sum_ext_first dst_negative_sum_sum_ext_first. (((F) = (((((dst_positive_code_sum_ext_first) + (dst_positive_scale_sum_ext_first)) * S ((dst_positive_code_sum_ext_first) + (dst_positive_scale_sum_ext_first)) + ((dst_positive_scale_sum_ext_first) + (dst_positive_scale_sum_ext_first))) + (((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) * S ((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) + ((dst_negative_scale_sum_ext_first) + (dst_negative_scale_sum_ext_first)))) * S ((((dst_positive_code_sum_ext_first) + (dst_positive_scale_sum_ext_first)) * S ((dst_positive_code_sum_ext_first) + (dst_positive_scale_sum_ext_first)) + ((dst_positive_scale_sum_ext_first) + (dst_positive_scale_sum_ext_first))) + (((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) * S ((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) + ((dst_negative_scale_sum_ext_first) + (dst_negative_scale_sum_ext_first)))) + ((((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) * S ((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) + ((dst_negative_scale_sum_ext_first) + (dst_negative_scale_sum_ext_first))) + (((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) * S ((dst_negative_code_sum_ext_first) + (dst_negative_scale_sum_ext_first)) + ((dst_negative_scale_sum_ext_first) + (dst_negative_scale_sum_ext_first)))))) /\ (((exists fs_u_dst_sum_ext_firstpositive fs_v_dst_sum_ext_firstpositive. ((((exists fs_h_dst_sum_ext_firstpositive_body_start. fs_h_dst_sum_ext_firstpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_ext_firstpositive)) /\ exists fs_q_dst_sum_ext_firstpositive_body_start. fs_u_dst_sum_ext_firstpositive = fs_q_dst_sum_ext_firstpositive_body_start * S ((S (0)) * fs_v_dst_sum_ext_firstpositive) + (0))) /\ ((((exists fs_h_dst_sum_ext_firstpositive_body_terminal. fs_h_dst_sum_ext_firstpositive_body_terminal + S (dst_positive_sum_sum_ext_first) = S ((S (l)) * fs_v_dst_sum_ext_firstpositive)) /\ exists fs_q_dst_sum_ext_firstpositive_body_terminal. fs_u_dst_sum_ext_firstpositive = fs_q_dst_sum_ext_firstpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_ext_firstpositive) + (dst_positive_sum_sum_ext_first))) /\ forall fs_i_dst_sum_ext_firstpositive_body_steps. (exists fs_lt_dst_sum_ext_firstpositive_body_steps_bound. fs_lt_dst_sum_ext_firstpositive_body_steps_bound + S fs_i_dst_sum_ext_firstpositive_body_steps = l) -> exists fs_a_dst_sum_ext_firstpositive_body_steps fs_r_dst_sum_ext_firstpositive_body_steps fs_s_dst_sum_ext_firstpositive_body_steps. ((((exists fs_h_dst_sum_ext_firstpositive_body_steps_summand. fs_h_dst_sum_ext_firstpositive_body_steps_summand + S (fs_a_dst_sum_ext_firstpositive_body_steps) = S ((S (fs_i_dst_sum_ext_firstpositive_body_steps)) * dst_positive_scale_sum_ext_first)) /\ exists fs_q_dst_sum_ext_firstpositive_body_steps_summand. dst_positive_code_sum_ext_first = fs_q_dst_sum_ext_firstpositive_body_steps_summand * S ((S (fs_i_dst_sum_ext_firstpositive_body_steps)) * dst_positive_scale_sum_ext_first) + (fs_a_dst_sum_ext_firstpositive_body_steps))) /\ ((((exists fs_h_dst_sum_ext_firstpositive_body_steps_partial. fs_h_dst_sum_ext_firstpositive_body_steps_partial + S (fs_r_dst_sum_ext_firstpositive_body_steps) = S ((S (fs_i_dst_sum_ext_firstpositive_body_steps)) * fs_v_dst_sum_ext_firstpositive)) /\ exists fs_q_dst_sum_ext_firstpositive_body_steps_partial. fs_u_dst_sum_ext_firstpositive = fs_q_dst_sum_ext_firstpositive_body_steps_partial * S ((S (fs_i_dst_sum_ext_firstpositive_body_steps)) * fs_v_dst_sum_ext_firstpositive) + (fs_r_dst_sum_ext_firstpositive_body_steps))) /\ ((((exists fs_h_dst_sum_ext_firstpositive_body_steps_successor. fs_h_dst_sum_ext_firstpositive_body_steps_successor + S (fs_s_dst_sum_ext_firstpositive_body_steps) = S ((S (S fs_i_dst_sum_ext_firstpositive_body_steps)) * fs_v_dst_sum_ext_firstpositive)) /\ exists fs_q_dst_sum_ext_firstpositive_body_steps_successor. fs_u_dst_sum_ext_firstpositive = fs_q_dst_sum_ext_firstpositive_body_steps_successor * S ((S (S fs_i_dst_sum_ext_firstpositive_body_steps)) * fs_v_dst_sum_ext_firstpositive) + (fs_s_dst_sum_ext_firstpositive_body_steps))) /\ fs_s_dst_sum_ext_firstpositive_body_steps = fs_r_dst_sum_ext_firstpositive_body_steps + fs_a_dst_sum_ext_firstpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_ext_firstnegative fs_v_dst_sum_ext_firstnegative. ((((exists fs_h_dst_sum_ext_firstnegative_body_start. fs_h_dst_sum_ext_firstnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_ext_firstnegative)) /\ exists fs_q_dst_sum_ext_firstnegative_body_start. fs_u_dst_sum_ext_firstnegative = fs_q_dst_sum_ext_firstnegative_body_start * S ((S (0)) * fs_v_dst_sum_ext_firstnegative) + (0))) /\ ((((exists fs_h_dst_sum_ext_firstnegative_body_terminal. fs_h_dst_sum_ext_firstnegative_body_terminal + S (dst_negative_sum_sum_ext_first) = S ((S (l)) * fs_v_dst_sum_ext_firstnegative)) /\ exists fs_q_dst_sum_ext_firstnegative_body_terminal. fs_u_dst_sum_ext_firstnegative = fs_q_dst_sum_ext_firstnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_ext_firstnegative) + (dst_negative_sum_sum_ext_first))) /\ forall fs_i_dst_sum_ext_firstnegative_body_steps. (exists fs_lt_dst_sum_ext_firstnegative_body_steps_bound. fs_lt_dst_sum_ext_firstnegative_body_steps_bound + S fs_i_dst_sum_ext_firstnegative_body_steps = l) -> exists fs_a_dst_sum_ext_firstnegative_body_steps fs_r_dst_sum_ext_firstnegative_body_steps fs_s_dst_sum_ext_firstnegative_body_steps. ((((exists fs_h_dst_sum_ext_firstnegative_body_steps_summand. fs_h_dst_sum_ext_firstnegative_body_steps_summand + S (fs_a_dst_sum_ext_firstnegative_body_steps) = S ((S (fs_i_dst_sum_ext_firstnegative_body_steps)) * dst_negative_scale_sum_ext_first)) /\ exists fs_q_dst_sum_ext_firstnegative_body_steps_summand. dst_negative_code_sum_ext_first = fs_q_dst_sum_ext_firstnegative_body_steps_summand * S ((S (fs_i_dst_sum_ext_firstnegative_body_steps)) * dst_negative_scale_sum_ext_first) + (fs_a_dst_sum_ext_firstnegative_body_steps))) /\ ((((exists fs_h_dst_sum_ext_firstnegative_body_steps_partial. fs_h_dst_sum_ext_firstnegative_body_steps_partial + S (fs_r_dst_sum_ext_firstnegative_body_steps) = S ((S (fs_i_dst_sum_ext_firstnegative_body_steps)) * fs_v_dst_sum_ext_firstnegative)) /\ exists fs_q_dst_sum_ext_firstnegative_body_steps_partial. fs_u_dst_sum_ext_firstnegative = fs_q_dst_sum_ext_firstnegative_body_steps_partial * S ((S (fs_i_dst_sum_ext_firstnegative_body_steps)) * fs_v_dst_sum_ext_firstnegative) + (fs_r_dst_sum_ext_firstnegative_body_steps))) /\ ((((exists fs_h_dst_sum_ext_firstnegative_body_steps_successor. fs_h_dst_sum_ext_firstnegative_body_steps_successor + S (fs_s_dst_sum_ext_firstnegative_body_steps) = S ((S (S fs_i_dst_sum_ext_firstnegative_body_steps)) * fs_v_dst_sum_ext_firstnegative)) /\ exists fs_q_dst_sum_ext_firstnegative_body_steps_successor. fs_u_dst_sum_ext_firstnegative = fs_q_dst_sum_ext_firstnegative_body_steps_successor * S ((S (S fs_i_dst_sum_ext_firstnegative_body_steps)) * fs_v_dst_sum_ext_firstnegative) + (fs_s_dst_sum_ext_firstnegative_body_steps))) /\ fs_s_dst_sum_ext_firstnegative_body_steps = fs_r_dst_sum_ext_firstnegative_body_steps + fs_a_dst_sum_ext_firstnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_ext_firstresult ge_balance_negative_sum_ext_firstresult. (((((a) = 2 * (ge_balance_positive_sum_ext_firstresult) /\ (ge_balance_negative_sum_ext_firstresult) = 0) \/ exists ge_signed_half_sum_ext_firstresultdecode. (((a) = 2 * ge_signed_half_sum_ext_firstresultdecode + 1 /\ (ge_balance_positive_sum_ext_firstresult) = 0) /\ (ge_balance_negative_sum_ext_firstresult) = S ge_signed_half_sum_ext_firstresultdecode))) /\ ((dst_positive_sum_sum_ext_first) + ge_balance_negative_sum_ext_firstresult = (dst_negative_sum_sum_ext_first) + ge_balance_positive_sum_ext_firstresult))))))))) -> (exists dst_positive_code_sum_ext_second dst_positive_scale_sum_ext_second dst_negative_code_sum_ext_second dst_negative_scale_sum_ext_second dst_positive_sum_sum_ext_second dst_negative_sum_sum_ext_second. (((G) = (((((dst_positive_code_sum_ext_second) + (dst_positive_scale_sum_ext_second)) * S ((dst_positive_code_sum_ext_second) + (dst_positive_scale_sum_ext_second)) + ((dst_positive_scale_sum_ext_second) + (dst_positive_scale_sum_ext_second))) + (((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) * S ((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) + ((dst_negative_scale_sum_ext_second) + (dst_negative_scale_sum_ext_second)))) * S ((((dst_positive_code_sum_ext_second) + (dst_positive_scale_sum_ext_second)) * S ((dst_positive_code_sum_ext_second) + (dst_positive_scale_sum_ext_second)) + ((dst_positive_scale_sum_ext_second) + (dst_positive_scale_sum_ext_second))) + (((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) * S ((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) + ((dst_negative_scale_sum_ext_second) + (dst_negative_scale_sum_ext_second)))) + ((((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) * S ((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) + ((dst_negative_scale_sum_ext_second) + (dst_negative_scale_sum_ext_second))) + (((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) * S ((dst_negative_code_sum_ext_second) + (dst_negative_scale_sum_ext_second)) + ((dst_negative_scale_sum_ext_second) + (dst_negative_scale_sum_ext_second)))))) /\ (((exists fs_u_dst_sum_ext_secondpositive fs_v_dst_sum_ext_secondpositive. ((((exists fs_h_dst_sum_ext_secondpositive_body_start. fs_h_dst_sum_ext_secondpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_ext_secondpositive)) /\ exists fs_q_dst_sum_ext_secondpositive_body_start. fs_u_dst_sum_ext_secondpositive = fs_q_dst_sum_ext_secondpositive_body_start * S ((S (0)) * fs_v_dst_sum_ext_secondpositive) + (0))) /\ ((((exists fs_h_dst_sum_ext_secondpositive_body_terminal. fs_h_dst_sum_ext_secondpositive_body_terminal + S (dst_positive_sum_sum_ext_second) = S ((S (l)) * fs_v_dst_sum_ext_secondpositive)) /\ exists fs_q_dst_sum_ext_secondpositive_body_terminal. fs_u_dst_sum_ext_secondpositive = fs_q_dst_sum_ext_secondpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_ext_secondpositive) + (dst_positive_sum_sum_ext_second))) /\ forall fs_i_dst_sum_ext_secondpositive_body_steps. (exists fs_lt_dst_sum_ext_secondpositive_body_steps_bound. fs_lt_dst_sum_ext_secondpositive_body_steps_bound + S fs_i_dst_sum_ext_secondpositive_body_steps = l) -> exists fs_a_dst_sum_ext_secondpositive_body_steps fs_r_dst_sum_ext_secondpositive_body_steps fs_s_dst_sum_ext_secondpositive_body_steps. ((((exists fs_h_dst_sum_ext_secondpositive_body_steps_summand. fs_h_dst_sum_ext_secondpositive_body_steps_summand + S (fs_a_dst_sum_ext_secondpositive_body_steps) = S ((S (fs_i_dst_sum_ext_secondpositive_body_steps)) * dst_positive_scale_sum_ext_second)) /\ exists fs_q_dst_sum_ext_secondpositive_body_steps_summand. dst_positive_code_sum_ext_second = fs_q_dst_sum_ext_secondpositive_body_steps_summand * S ((S (fs_i_dst_sum_ext_secondpositive_body_steps)) * dst_positive_scale_sum_ext_second) + (fs_a_dst_sum_ext_secondpositive_body_steps))) /\ ((((exists fs_h_dst_sum_ext_secondpositive_body_steps_partial. fs_h_dst_sum_ext_secondpositive_body_steps_partial + S (fs_r_dst_sum_ext_secondpositive_body_steps) = S ((S (fs_i_dst_sum_ext_secondpositive_body_steps)) * fs_v_dst_sum_ext_secondpositive)) /\ exists fs_q_dst_sum_ext_secondpositive_body_steps_partial. fs_u_dst_sum_ext_secondpositive = fs_q_dst_sum_ext_secondpositive_body_steps_partial * S ((S (fs_i_dst_sum_ext_secondpositive_body_steps)) * fs_v_dst_sum_ext_secondpositive) + (fs_r_dst_sum_ext_secondpositive_body_steps))) /\ ((((exists fs_h_dst_sum_ext_secondpositive_body_steps_successor. fs_h_dst_sum_ext_secondpositive_body_steps_successor + S (fs_s_dst_sum_ext_secondpositive_body_steps) = S ((S (S fs_i_dst_sum_ext_secondpositive_body_steps)) * fs_v_dst_sum_ext_secondpositive)) /\ exists fs_q_dst_sum_ext_secondpositive_body_steps_successor. fs_u_dst_sum_ext_secondpositive = fs_q_dst_sum_ext_secondpositive_body_steps_successor * S ((S (S fs_i_dst_sum_ext_secondpositive_body_steps)) * fs_v_dst_sum_ext_secondpositive) + (fs_s_dst_sum_ext_secondpositive_body_steps))) /\ fs_s_dst_sum_ext_secondpositive_body_steps = fs_r_dst_sum_ext_secondpositive_body_steps + fs_a_dst_sum_ext_secondpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_ext_secondnegative fs_v_dst_sum_ext_secondnegative. ((((exists fs_h_dst_sum_ext_secondnegative_body_start. fs_h_dst_sum_ext_secondnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_ext_secondnegative)) /\ exists fs_q_dst_sum_ext_secondnegative_body_start. fs_u_dst_sum_ext_secondnegative = fs_q_dst_sum_ext_secondnegative_body_start * S ((S (0)) * fs_v_dst_sum_ext_secondnegative) + (0))) /\ ((((exists fs_h_dst_sum_ext_secondnegative_body_terminal. fs_h_dst_sum_ext_secondnegative_body_terminal + S (dst_negative_sum_sum_ext_second) = S ((S (l)) * fs_v_dst_sum_ext_secondnegative)) /\ exists fs_q_dst_sum_ext_secondnegative_body_terminal. fs_u_dst_sum_ext_secondnegative = fs_q_dst_sum_ext_secondnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_ext_secondnegative) + (dst_negative_sum_sum_ext_second))) /\ forall fs_i_dst_sum_ext_secondnegative_body_steps. (exists fs_lt_dst_sum_ext_secondnegative_body_steps_bound. fs_lt_dst_sum_ext_secondnegative_body_steps_bound + S fs_i_dst_sum_ext_secondnegative_body_steps = l) -> exists fs_a_dst_sum_ext_secondnegative_body_steps fs_r_dst_sum_ext_secondnegative_body_steps fs_s_dst_sum_ext_secondnegative_body_steps. ((((exists fs_h_dst_sum_ext_secondnegative_body_steps_summand. fs_h_dst_sum_ext_secondnegative_body_steps_summand + S (fs_a_dst_sum_ext_secondnegative_body_steps) = S ((S (fs_i_dst_sum_ext_secondnegative_body_steps)) * dst_negative_scale_sum_ext_second)) /\ exists fs_q_dst_sum_ext_secondnegative_body_steps_summand. dst_negative_code_sum_ext_second = fs_q_dst_sum_ext_secondnegative_body_steps_summand * S ((S (fs_i_dst_sum_ext_secondnegative_body_steps)) * dst_negative_scale_sum_ext_second) + (fs_a_dst_sum_ext_secondnegative_body_steps))) /\ ((((exists fs_h_dst_sum_ext_secondnegative_body_steps_partial. fs_h_dst_sum_ext_secondnegative_body_steps_partial + S (fs_r_dst_sum_ext_secondnegative_body_steps) = S ((S (fs_i_dst_sum_ext_secondnegative_body_steps)) * fs_v_dst_sum_ext_secondnegative)) /\ exists fs_q_dst_sum_ext_secondnegative_body_steps_partial. fs_u_dst_sum_ext_secondnegative = fs_q_dst_sum_ext_secondnegative_body_steps_partial * S ((S (fs_i_dst_sum_ext_secondnegative_body_steps)) * fs_v_dst_sum_ext_secondnegative) + (fs_r_dst_sum_ext_secondnegative_body_steps))) /\ ((((exists fs_h_dst_sum_ext_secondnegative_body_steps_successor. fs_h_dst_sum_ext_secondnegative_body_steps_successor + S (fs_s_dst_sum_ext_secondnegative_body_steps) = S ((S (S fs_i_dst_sum_ext_secondnegative_body_steps)) * fs_v_dst_sum_ext_secondnegative)) /\ exists fs_q_dst_sum_ext_secondnegative_body_steps_successor. fs_u_dst_sum_ext_secondnegative = fs_q_dst_sum_ext_secondnegative_body_steps_successor * S ((S (S fs_i_dst_sum_ext_secondnegative_body_steps)) * fs_v_dst_sum_ext_secondnegative) + (fs_s_dst_sum_ext_secondnegative_body_steps))) /\ fs_s_dst_sum_ext_secondnegative_body_steps = fs_r_dst_sum_ext_secondnegative_body_steps + fs_a_dst_sum_ext_secondnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_ext_secondresult ge_balance_negative_sum_ext_secondresult. (((((b) = 2 * (ge_balance_positive_sum_ext_secondresult) /\ (ge_balance_negative_sum_ext_secondresult) = 0) \/ exists ge_signed_half_sum_ext_secondresultdecode. (((b) = 2 * ge_signed_half_sum_ext_secondresultdecode + 1 /\ (ge_balance_positive_sum_ext_secondresult) = 0) /\ (ge_balance_negative_sum_ext_secondresult) = S ge_signed_half_sum_ext_secondresultdecode))) /\ ((dst_positive_sum_sum_ext_second) + ge_balance_negative_sum_ext_secondresult = (dst_negative_sum_sum_ext_second) + ge_balance_positive_sum_ext_secondresult))))))))) -> a = b

Complete tactic proof in conservative notation

All 72 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.

Read the argument

Proof checkpoints

72 script commands · 10 reading checkpoints · 1 local claims

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.

Named ingredients (1)

divisor signed table equality component balance

01Fix variables and assumptionsL1–8

Work with arbitrary variables or the premises of the current implication.

L1
intro F
L2
intro G
L3
intro l
L4
intro a
L5
intro b
L6
intro hequal
L7
intro ha
L8
intro hb

02Separate the logical casesL9–18

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L9
cases ha
L10
cases ha_witness
L11
cases ha_witness_witness
L12
cases ha_witness_witness_witness
L13
cases ha_witness_witness_witness_witness
L14
cases ha_witness_witness_witness_witness_witness
L15
cases ha_witness_witness_witness_witness_witness_witness
L16
cases ha_witness_witness_witness_witness_witness_witness_right
L17
cases ha_witness_witness_witness_witness_witness_witness_right_right
L18
cases hb

03Separate the logical casesL19–26

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L19
cases hb_witness
L20
cases hb_witness_witness
L21
cases hb_witness_witness_witness
L22
cases hb_witness_witness_witness_witness
L23
cases hb_witness_witness_witness_witness_witness
L24
cases hb_witness_witness_witness_witness_witness_witness
L25
cases hb_witness_witness_witness_witness_witness_witness_right
L26
cases hb_witness_witness_witness_witness_witness_witness_right_right

04Establish hbalanceL27–36

Establish this local claim before using it. It is not an additional assumption.

L27
have hbalance : x4 + x11 = x10 + x5
L28
specialize matrix_integer_signed_sum_balance (x)
L29
specialize matrix_integer_signed_sum_balance (x1)
L30
specialize matrix_integer_signed_sum_balance (x2)
L31
specialize matrix_integer_signed_sum_balance (x3)
L32
specialize matrix_integer_signed_sum_balance (x6)
L33
specialize matrix_integer_signed_sum_balance (x7)
L34
specialize matrix_integer_signed_sum_balance (x8)
L35
specialize matrix_integer_signed_sum_balance (x9)
L36
specialize matrix_integer_signed_sum_balance (l)

05Use earlier factsL37–46