Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.
Original finite natural-sum permutation invariance preserves both actual component sums, hence their canonical signed result.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
These are genuine signed-table and finite-sum foundations, not full divisor-sum cancellation or Möbius inversion. G007 remains open. The historical MatrixMinorFourCode definition is reused solely as generic nested pairing of four beta parameters; no matrix-specific hypothesis is imported. Equality is equality of represented signed values, not equality of arbitrary component codes.
forall F G pb pc nb nc qb qc mb mc r s l u v. ((F) = (((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) * S ((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) + ((((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))))) -> ((G) = (((((qb) + (qc)) * S ((qb) + (qc)) + ((qc) + (qc))) + (((mb) + (mc)) * S ((mb) + (mc)) + ((mc) + (mc)))) * S ((((qb) + (qc)) * S ((qb) + (qc)) + ((qc) + (qc))) + (((mb) + (mc)) * S ((mb) + (mc)) + ((mc) + (mc)))) + ((((mb) + (mc)) * S ((mb) + (mc)) + ((mc) + (mc))) + (((mb) + (mc)) * S ((mb) + (mc)) + ((mc) + (mc)))))) -> (forall pfp_i_sum_map_bounded. (exists pfp_gap_sum_map_boundedindex. pfp_gap_sum_map_boundedindex + S (pfp_i_sum_map_bounded) = (l)) -> exists pfp_a_sum_map_bounded. (((exists ff_h_pfp_sum_map_boundedentry. ff_h_pfp_sum_map_boundedentry + S (pfp_a_sum_map_bounded) = S ((S (pfp_i_sum_map_bounded)) * s)) /\ exists ff_q_pfp_sum_map_boundedentry. r = ff_q_pfp_sum_map_boundedentry * S ((S (pfp_i_sum_map_bounded)) * s) + (pfp_a_sum_map_bounded))) /\ (exists pfp_gap_sum_map_boundedvalue. pfp_gap_sum_map_boundedvalue + S (pfp_a_sum_map_bounded) = (l))) -> (forall pfp_i_sum_map_injective pfp_j_sum_map_injective pfp_a_sum_map_injective. (exists pfp_gap_sum_map_injectivefirst. pfp_gap_sum_map_injectivefirst + S (pfp_i_sum_map_injective) = (l)) -> (exists pfp_gap_sum_map_injectivesecond. pfp_gap_sum_map_injectivesecond + S (pfp_j_sum_map_injective) = (l)) -> (((exists ff_h_pfp_sum_map_injectiveleft. ff_h_pfp_sum_map_injectiveleft + S (pfp_a_sum_map_injective) = S ((S (pfp_i_sum_map_injective)) * s)) /\ exists ff_q_pfp_sum_map_injectiveleft. r = ff_q_pfp_sum_map_injectiveleft * S ((S (pfp_i_sum_map_injective)) * s) + (pfp_a_sum_map_injective))) -> (((exists ff_h_pfp_sum_map_injectiveright. ff_h_pfp_sum_map_injectiveright + S (pfp_a_sum_map_injective) = S ((S (pfp_j_sum_map_injective)) * s)) /\ exists ff_q_pfp_sum_map_injectiveright. r = ff_q_pfp_sum_map_injectiveright * S ((S (pfp_j_sum_map_injective)) * s) + (pfp_a_sum_map_injective))) -> pfp_i_sum_map_injective = pfp_j_sum_map_injective) -> (((forall fms_i_sum_component_compositionpositive fms_j_sum_component_compositionpositive fms_v_sum_component_compositionpositive. (exists fms_gap_sum_component_compositionpositive. fms_gap_sum_component_compositionpositive + S (fms_i_sum_component_compositionpositive) = (l)) -> (((exists fs_h_fms_sum_component_compositionpositive_index. fs_h_fms_sum_component_compositionpositive_index + S (fms_j_sum_component_compositionpositive) = S ((S (fms_i_sum_component_compositionpositive)) * s)) /\ exists fs_q_fms_sum_component_compositionpositive_index. r = fs_q_fms_sum_component_compositionpositive_index * S ((S (fms_i_sum_component_compositionpositive)) * s) + (fms_j_sum_component_compositionpositive))) -> (((exists fs_h_fms_sum_component_compositionpositive_source. fs_h_fms_sum_component_compositionpositive_source + S (fms_v_sum_component_compositionpositive) = S ((S (fms_j_sum_component_compositionpositive)) * pc)) /\ exists fs_q_fms_sum_component_compositionpositive_source. pb = fs_q_fms_sum_component_compositionpositive_source * S ((S (fms_j_sum_component_compositionpositive)) * pc) + (fms_v_sum_component_compositionpositive))) -> (((exists fs_h_fms_sum_component_compositionpositive_target. fs_h_fms_sum_component_compositionpositive_target + S (fms_v_sum_component_compositionpositive) = S ((S (fms_i_sum_component_compositionpositive)) * qc)) /\ exists fs_q_fms_sum_component_compositionpositive_target. qb = fs_q_fms_sum_component_compositionpositive_target * S ((S (fms_i_sum_component_compositionpositive)) * qc) + (fms_v_sum_component_compositionpositive)))) /\ (forall fms_i_sum_component_compositionnegative fms_j_sum_component_compositionnegative fms_v_sum_component_compositionnegative. (exists fms_gap_sum_component_compositionnegative. fms_gap_sum_component_compositionnegative + S (fms_i_sum_component_compositionnegative) = (l)) -> (((exists fs_h_fms_sum_component_compositionnegative_index. fs_h_fms_sum_component_compositionnegative_index + S (fms_j_sum_component_compositionnegative) = S ((S (fms_i_sum_component_compositionnegative)) * s)) /\ exists fs_q_fms_sum_component_compositionnegative_index. r = fs_q_fms_sum_component_compositionnegative_index * S ((S (fms_i_sum_component_compositionnegative)) * s) + (fms_j_sum_component_compositionnegative))) -> (((exists fs_h_fms_sum_component_compositionnegative_source. fs_h_fms_sum_component_compositionnegative_source + S (fms_v_sum_component_compositionnegative) = S ((S (fms_j_sum_component_compositionnegative)) * nc)) /\ exists fs_q_fms_sum_component_compositionnegative_source. nb = fs_q_fms_sum_component_compositionnegative_source * S ((S (fms_j_sum_component_compositionnegative)) * nc) + (fms_v_sum_component_compositionnegative))) -> (((exists fs_h_fms_sum_component_compositionnegative_target. fs_h_fms_sum_component_compositionnegative_target + S (fms_v_sum_component_compositionnegative) = S ((S (fms_i_sum_component_compositionnegative)) * mc)) /\ exists fs_q_fms_sum_component_compositionnegative_target. mb = fs_q_fms_sum_component_compositionnegative_target * S ((S (fms_i_sum_component_compositionnegative)) * mc) + (fms_v_sum_component_compositionnegative)))))) -> (exists dst_positive_code_sum_source dst_positive_scale_sum_source dst_negative_code_sum_source dst_negative_scale_sum_source dst_positive_sum_sum_source dst_negative_sum_sum_source. (((F) = (((((dst_positive_code_sum_source) + (dst_positive_scale_sum_source)) * S ((dst_positive_code_sum_source) + (dst_positive_scale_sum_source)) + ((dst_positive_scale_sum_source) + (dst_positive_scale_sum_source))) + (((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) * S ((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) + ((dst_negative_scale_sum_source) + (dst_negative_scale_sum_source)))) * S ((((dst_positive_code_sum_source) + (dst_positive_scale_sum_source)) * S ((dst_positive_code_sum_source) + (dst_positive_scale_sum_source)) + ((dst_positive_scale_sum_source) + (dst_positive_scale_sum_source))) + (((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) * S ((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) + ((dst_negative_scale_sum_source) + (dst_negative_scale_sum_source)))) + ((((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) * S ((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) + ((dst_negative_scale_sum_source) + (dst_negative_scale_sum_source))) + (((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) * S ((dst_negative_code_sum_source) + (dst_negative_scale_sum_source)) + ((dst_negative_scale_sum_source) + (dst_negative_scale_sum_source)))))) /\ (((exists fs_u_dst_sum_sourcepositive fs_v_dst_sum_sourcepositive. ((((exists fs_h_dst_sum_sourcepositive_body_start. fs_h_dst_sum_sourcepositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_sourcepositive)) /\ exists fs_q_dst_sum_sourcepositive_body_start. fs_u_dst_sum_sourcepositive = fs_q_dst_sum_sourcepositive_body_start * S ((S (0)) * fs_v_dst_sum_sourcepositive) + (0))) /\ ((((exists fs_h_dst_sum_sourcepositive_body_terminal. fs_h_dst_sum_sourcepositive_body_terminal + S (dst_positive_sum_sum_source) = S ((S (l)) * fs_v_dst_sum_sourcepositive)) /\ exists fs_q_dst_sum_sourcepositive_body_terminal. fs_u_dst_sum_sourcepositive = fs_q_dst_sum_sourcepositive_body_terminal * S ((S (l)) * fs_v_dst_sum_sourcepositive) + (dst_positive_sum_sum_source))) /\ forall fs_i_dst_sum_sourcepositive_body_steps. (exists fs_lt_dst_sum_sourcepositive_body_steps_bound. fs_lt_dst_sum_sourcepositive_body_steps_bound + S fs_i_dst_sum_sourcepositive_body_steps = l) -> exists fs_a_dst_sum_sourcepositive_body_steps fs_r_dst_sum_sourcepositive_body_steps fs_s_dst_sum_sourcepositive_body_steps. ((((exists fs_h_dst_sum_sourcepositive_body_steps_summand. fs_h_dst_sum_sourcepositive_body_steps_summand + S (fs_a_dst_sum_sourcepositive_body_steps) = S ((S (fs_i_dst_sum_sourcepositive_body_steps)) * dst_positive_scale_sum_source)) /\ exists fs_q_dst_sum_sourcepositive_body_steps_summand. dst_positive_code_sum_source = fs_q_dst_sum_sourcepositive_body_steps_summand * S ((S (fs_i_dst_sum_sourcepositive_body_steps)) * dst_positive_scale_sum_source) + (fs_a_dst_sum_sourcepositive_body_steps))) /\ ((((exists fs_h_dst_sum_sourcepositive_body_steps_partial. fs_h_dst_sum_sourcepositive_body_steps_partial + S (fs_r_dst_sum_sourcepositive_body_steps) = S ((S (fs_i_dst_sum_sourcepositive_body_steps)) * fs_v_dst_sum_sourcepositive)) /\ exists fs_q_dst_sum_sourcepositive_body_steps_partial. fs_u_dst_sum_sourcepositive = fs_q_dst_sum_sourcepositive_body_steps_partial * S ((S (fs_i_dst_sum_sourcepositive_body_steps)) * fs_v_dst_sum_sourcepositive) + (fs_r_dst_sum_sourcepositive_body_steps))) /\ ((((exists fs_h_dst_sum_sourcepositive_body_steps_successor. fs_h_dst_sum_sourcepositive_body_steps_successor + S (fs_s_dst_sum_sourcepositive_body_steps) = S ((S (S fs_i_dst_sum_sourcepositive_body_steps)) * fs_v_dst_sum_sourcepositive)) /\ exists fs_q_dst_sum_sourcepositive_body_steps_successor. fs_u_dst_sum_sourcepositive = fs_q_dst_sum_sourcepositive_body_steps_successor * S ((S (S fs_i_dst_sum_sourcepositive_body_steps)) * fs_v_dst_sum_sourcepositive) + (fs_s_dst_sum_sourcepositive_body_steps))) /\ fs_s_dst_sum_sourcepositive_body_steps = fs_r_dst_sum_sourcepositive_body_steps + fs_a_dst_sum_sourcepositive_body_steps)))))) /\ (((exists fs_u_dst_sum_sourcenegative fs_v_dst_sum_sourcenegative. ((((exists fs_h_dst_sum_sourcenegative_body_start. fs_h_dst_sum_sourcenegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_sourcenegative)) /\ exists fs_q_dst_sum_sourcenegative_body_start. fs_u_dst_sum_sourcenegative = fs_q_dst_sum_sourcenegative_body_start * S ((S (0)) * fs_v_dst_sum_sourcenegative) + (0))) /\ ((((exists fs_h_dst_sum_sourcenegative_body_terminal. fs_h_dst_sum_sourcenegative_body_terminal + S (dst_negative_sum_sum_source) = S ((S (l)) * fs_v_dst_sum_sourcenegative)) /\ exists fs_q_dst_sum_sourcenegative_body_terminal. fs_u_dst_sum_sourcenegative = fs_q_dst_sum_sourcenegative_body_terminal * S ((S (l)) * fs_v_dst_sum_sourcenegative) + (dst_negative_sum_sum_source))) /\ forall fs_i_dst_sum_sourcenegative_body_steps. (exists fs_lt_dst_sum_sourcenegative_body_steps_bound. fs_lt_dst_sum_sourcenegative_body_steps_bound + S fs_i_dst_sum_sourcenegative_body_steps = l) -> exists fs_a_dst_sum_sourcenegative_body_steps fs_r_dst_sum_sourcenegative_body_steps fs_s_dst_sum_sourcenegative_body_steps. ((((exists fs_h_dst_sum_sourcenegative_body_steps_summand. fs_h_dst_sum_sourcenegative_body_steps_summand + S (fs_a_dst_sum_sourcenegative_body_steps) = S ((S (fs_i_dst_sum_sourcenegative_body_steps)) * dst_negative_scale_sum_source)) /\ exists fs_q_dst_sum_sourcenegative_body_steps_summand. dst_negative_code_sum_source = fs_q_dst_sum_sourcenegative_body_steps_summand * S ((S (fs_i_dst_sum_sourcenegative_body_steps)) * dst_negative_scale_sum_source) + (fs_a_dst_sum_sourcenegative_body_steps))) /\ ((((exists fs_h_dst_sum_sourcenegative_body_steps_partial. fs_h_dst_sum_sourcenegative_body_steps_partial + S (fs_r_dst_sum_sourcenegative_body_steps) = S ((S (fs_i_dst_sum_sourcenegative_body_steps)) * fs_v_dst_sum_sourcenegative)) /\ exists fs_q_dst_sum_sourcenegative_body_steps_partial. fs_u_dst_sum_sourcenegative = fs_q_dst_sum_sourcenegative_body_steps_partial * S ((S (fs_i_dst_sum_sourcenegative_body_steps)) * fs_v_dst_sum_sourcenegative) + (fs_r_dst_sum_sourcenegative_body_steps))) /\ ((((exists fs_h_dst_sum_sourcenegative_body_steps_successor. fs_h_dst_sum_sourcenegative_body_steps_successor + S (fs_s_dst_sum_sourcenegative_body_steps) = S ((S (S fs_i_dst_sum_sourcenegative_body_steps)) * fs_v_dst_sum_sourcenegative)) /\ exists fs_q_dst_sum_sourcenegative_body_steps_successor. fs_u_dst_sum_sourcenegative = fs_q_dst_sum_sourcenegative_body_steps_successor * S ((S (S fs_i_dst_sum_sourcenegative_body_steps)) * fs_v_dst_sum_sourcenegative) + (fs_s_dst_sum_sourcenegative_body_steps))) /\ fs_s_dst_sum_sourcenegative_body_steps = fs_r_dst_sum_sourcenegative_body_steps + fs_a_dst_sum_sourcenegative_body_steps)))))) /\ (exists ge_balance_positive_sum_sourceresult ge_balance_negative_sum_sourceresult. (((((u) = 2 * (ge_balance_positive_sum_sourceresult) /\ (ge_balance_negative_sum_sourceresult) = 0) \/ exists ge_signed_half_sum_sourceresultdecode. (((u) = 2 * ge_signed_half_sum_sourceresultdecode + 1 /\ (ge_balance_positive_sum_sourceresult) = 0) /\ (ge_balance_negative_sum_sourceresult) = S ge_signed_half_sum_sourceresultdecode))) /\ ((dst_positive_sum_sum_source) + ge_balance_negative_sum_sourceresult = (dst_negative_sum_sum_source) + ge_balance_positive_sum_sourceresult))))))))) -> (exists dst_positive_code_sum_target dst_positive_scale_sum_target dst_negative_code_sum_target dst_negative_scale_sum_target dst_positive_sum_sum_target dst_negative_sum_sum_target. (((G) = (((((dst_positive_code_sum_target) + (dst_positive_scale_sum_target)) * S ((dst_positive_code_sum_target) + (dst_positive_scale_sum_target)) + ((dst_positive_scale_sum_target) + (dst_positive_scale_sum_target))) + (((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) * S ((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) + ((dst_negative_scale_sum_target) + (dst_negative_scale_sum_target)))) * S ((((dst_positive_code_sum_target) + (dst_positive_scale_sum_target)) * S ((dst_positive_code_sum_target) + (dst_positive_scale_sum_target)) + ((dst_positive_scale_sum_target) + (dst_positive_scale_sum_target))) + (((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) * S ((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) + ((dst_negative_scale_sum_target) + (dst_negative_scale_sum_target)))) + ((((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) * S ((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) + ((dst_negative_scale_sum_target) + (dst_negative_scale_sum_target))) + (((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) * S ((dst_negative_code_sum_target) + (dst_negative_scale_sum_target)) + ((dst_negative_scale_sum_target) + (dst_negative_scale_sum_target)))))) /\ (((exists fs_u_dst_sum_targetpositive fs_v_dst_sum_targetpositive. ((((exists fs_h_dst_sum_targetpositive_body_start. fs_h_dst_sum_targetpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_targetpositive)) /\ exists fs_q_dst_sum_targetpositive_body_start. fs_u_dst_sum_targetpositive = fs_q_dst_sum_targetpositive_body_start * S ((S (0)) * fs_v_dst_sum_targetpositive) + (0))) /\ ((((exists fs_h_dst_sum_targetpositive_body_terminal. fs_h_dst_sum_targetpositive_body_terminal + S (dst_positive_sum_sum_target) = S ((S (l)) * fs_v_dst_sum_targetpositive)) /\ exists fs_q_dst_sum_targetpositive_body_terminal. fs_u_dst_sum_targetpositive = fs_q_dst_sum_targetpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_targetpositive) + (dst_positive_sum_sum_target))) /\ forall fs_i_dst_sum_targetpositive_body_steps. (exists fs_lt_dst_sum_targetpositive_body_steps_bound. fs_lt_dst_sum_targetpositive_body_steps_bound + S fs_i_dst_sum_targetpositive_body_steps = l) -> exists fs_a_dst_sum_targetpositive_body_steps fs_r_dst_sum_targetpositive_body_steps fs_s_dst_sum_targetpositive_body_steps. ((((exists fs_h_dst_sum_targetpositive_body_steps_summand. fs_h_dst_sum_targetpositive_body_steps_summand + S (fs_a_dst_sum_targetpositive_body_steps) = S ((S (fs_i_dst_sum_targetpositive_body_steps)) * dst_positive_scale_sum_target)) /\ exists fs_q_dst_sum_targetpositive_body_steps_summand. dst_positive_code_sum_target = fs_q_dst_sum_targetpositive_body_steps_summand * S ((S (fs_i_dst_sum_targetpositive_body_steps)) * dst_positive_scale_sum_target) + (fs_a_dst_sum_targetpositive_body_steps))) /\ ((((exists fs_h_dst_sum_targetpositive_body_steps_partial. fs_h_dst_sum_targetpositive_body_steps_partial + S (fs_r_dst_sum_targetpositive_body_steps) = S ((S (fs_i_dst_sum_targetpositive_body_steps)) * fs_v_dst_sum_targetpositive)) /\ exists fs_q_dst_sum_targetpositive_body_steps_partial. fs_u_dst_sum_targetpositive = fs_q_dst_sum_targetpositive_body_steps_partial * S ((S (fs_i_dst_sum_targetpositive_body_steps)) * fs_v_dst_sum_targetpositive) + (fs_r_dst_sum_targetpositive_body_steps))) /\ ((((exists fs_h_dst_sum_targetpositive_body_steps_successor. fs_h_dst_sum_targetpositive_body_steps_successor + S (fs_s_dst_sum_targetpositive_body_steps) = S ((S (S fs_i_dst_sum_targetpositive_body_steps)) * fs_v_dst_sum_targetpositive)) /\ exists fs_q_dst_sum_targetpositive_body_steps_successor. fs_u_dst_sum_targetpositive = fs_q_dst_sum_targetpositive_body_steps_successor * S ((S (S fs_i_dst_sum_targetpositive_body_steps)) * fs_v_dst_sum_targetpositive) + (fs_s_dst_sum_targetpositive_body_steps))) /\ fs_s_dst_sum_targetpositive_body_steps = fs_r_dst_sum_targetpositive_body_steps + fs_a_dst_sum_targetpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_targetnegative fs_v_dst_sum_targetnegative. ((((exists fs_h_dst_sum_targetnegative_body_start. fs_h_dst_sum_targetnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_targetnegative)) /\ exists fs_q_dst_sum_targetnegative_body_start. fs_u_dst_sum_targetnegative = fs_q_dst_sum_targetnegative_body_start * S ((S (0)) * fs_v_dst_sum_targetnegative) + (0))) /\ ((((exists fs_h_dst_sum_targetnegative_body_terminal. fs_h_dst_sum_targetnegative_body_terminal + S (dst_negative_sum_sum_target) = S ((S (l)) * fs_v_dst_sum_targetnegative)) /\ exists fs_q_dst_sum_targetnegative_body_terminal. fs_u_dst_sum_targetnegative = fs_q_dst_sum_targetnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_targetnegative) + (dst_negative_sum_sum_target))) /\ forall fs_i_dst_sum_targetnegative_body_steps. (exists fs_lt_dst_sum_targetnegative_body_steps_bound. fs_lt_dst_sum_targetnegative_body_steps_bound + S fs_i_dst_sum_targetnegative_body_steps = l) -> exists fs_a_dst_sum_targetnegative_body_steps fs_r_dst_sum_targetnegative_body_steps fs_s_dst_sum_targetnegative_body_steps. ((((exists fs_h_dst_sum_targetnegative_body_steps_summand. fs_h_dst_sum_targetnegative_body_steps_summand + S (fs_a_dst_sum_targetnegative_body_steps) = S ((S (fs_i_dst_sum_targetnegative_body_steps)) * dst_negative_scale_sum_target)) /\ exists fs_q_dst_sum_targetnegative_body_steps_summand. dst_negative_code_sum_target = fs_q_dst_sum_targetnegative_body_steps_summand * S ((S (fs_i_dst_sum_targetnegative_body_steps)) * dst_negative_scale_sum_target) + (fs_a_dst_sum_targetnegative_body_steps))) /\ ((((exists fs_h_dst_sum_targetnegative_body_steps_partial. fs_h_dst_sum_targetnegative_body_steps_partial + S (fs_r_dst_sum_targetnegative_body_steps) = S ((S (fs_i_dst_sum_targetnegative_body_steps)) * fs_v_dst_sum_targetnegative)) /\ exists fs_q_dst_sum_targetnegative_body_steps_partial. fs_u_dst_sum_targetnegative = fs_q_dst_sum_targetnegative_body_steps_partial * S ((S (fs_i_dst_sum_targetnegative_body_steps)) * fs_v_dst_sum_targetnegative) + (fs_r_dst_sum_targetnegative_body_steps))) /\ ((((exists fs_h_dst_sum_targetnegative_body_steps_successor. fs_h_dst_sum_targetnegative_body_steps_successor + S (fs_s_dst_sum_targetnegative_body_steps) = S ((S (S fs_i_dst_sum_targetnegative_body_steps)) * fs_v_dst_sum_targetnegative)) /\ exists fs_q_dst_sum_targetnegative_body_steps_successor. fs_u_dst_sum_targetnegative = fs_q_dst_sum_targetnegative_body_steps_successor * S ((S (S fs_i_dst_sum_targetnegative_body_steps)) * fs_v_dst_sum_targetnegative) + (fs_s_dst_sum_targetnegative_body_steps))) /\ fs_s_dst_sum_targetnegative_body_steps = fs_r_dst_sum_targetnegative_body_steps + fs_a_dst_sum_targetnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_targetresult ge_balance_negative_sum_targetresult. (((((v) = 2 * (ge_balance_positive_sum_targetresult) /\ (ge_balance_negative_sum_targetresult) = 0) \/ exists ge_signed_half_sum_targetresultdecode. (((v) = 2 * ge_signed_half_sum_targetresultdecode + 1 /\ (ge_balance_positive_sum_targetresult) = 0) /\ (ge_balance_negative_sum_targetresult) = S ge_signed_half_sum_targetresultdecode))) /\ ((dst_positive_sum_sum_target) + ge_balance_negative_sum_targetresult = (dst_negative_sum_sum_target) + ge_balance_positive_sum_targetresult))))))))) -> u = v
Complete tactic proof in conservative notation
All 96 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.