SS0017

divisor_signed_sum_successor_decompose

Every successor signed sum supplies real predecessor and last-entry codes whose original SignedAdd graph gives its result.

Alpha v34 checked-use · first admitted v31 · 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.

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. ∀ l. ∀ z. SignedPrefixSum(F,S l,z) → ∃ x. ∃ y. SignedPrefixSum(F,l,x) ∧ (ArithAt(F,l,y) ∧ (∃ n. ∃ m. ∃ k. ∃ i. ∃ j. ∃ u. SignedDecode(x,n,m) ∧ (SignedDecode(y,k,i) ∧ (SignedDecode(z,j,u) ∧ n + k + u = m + i + j))))

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

Definition DAG

SignedDecode(z,p,n) · 3SignedBalance(z,p,n) · 2ArithAt(F,i,z) · 1SignedPrefixSum(F,l,z) · 2BetaAt(b,c,i,x) · 2Sum(b,c,l,z) · 2

Actual proof prerequisites

beta_sum_succ_decompose · checked external prerequisitesigned_balance_total · checked external prerequisitedivisor_signed_sum_from_componentsdivisor_signed_table_at_from_componentsgaussian_signed_add_of_balances · checked external prerequisite
Original expanded first-order statement 
forall F l z. (exists dst_positive_code_decomp_sum dst_positive_scale_decomp_sum dst_negative_code_decomp_sum dst_negative_scale_decomp_sum dst_positive_sum_decomp_sum dst_negative_sum_decomp_sum. (((F) = (((((dst_positive_code_decomp_sum) + (dst_positive_scale_decomp_sum)) * S ((dst_positive_code_decomp_sum) + (dst_positive_scale_decomp_sum)) + ((dst_positive_scale_decomp_sum) + (dst_positive_scale_decomp_sum))) + (((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) * S ((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) + ((dst_negative_scale_decomp_sum) + (dst_negative_scale_decomp_sum)))) * S ((((dst_positive_code_decomp_sum) + (dst_positive_scale_decomp_sum)) * S ((dst_positive_code_decomp_sum) + (dst_positive_scale_decomp_sum)) + ((dst_positive_scale_decomp_sum) + (dst_positive_scale_decomp_sum))) + (((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) * S ((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) + ((dst_negative_scale_decomp_sum) + (dst_negative_scale_decomp_sum)))) + ((((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) * S ((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) + ((dst_negative_scale_decomp_sum) + (dst_negative_scale_decomp_sum))) + (((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) * S ((dst_negative_code_decomp_sum) + (dst_negative_scale_decomp_sum)) + ((dst_negative_scale_decomp_sum) + (dst_negative_scale_decomp_sum)))))) /\ (((exists fs_u_dst_decomp_sumpositive fs_v_dst_decomp_sumpositive. ((((exists fs_h_dst_decomp_sumpositive_body_start. fs_h_dst_decomp_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_decomp_sumpositive)) /\ exists fs_q_dst_decomp_sumpositive_body_start. fs_u_dst_decomp_sumpositive = fs_q_dst_decomp_sumpositive_body_start * S ((S (0)) * fs_v_dst_decomp_sumpositive) + (0))) /\ ((((exists fs_h_dst_decomp_sumpositive_body_terminal. fs_h_dst_decomp_sumpositive_body_terminal + S (dst_positive_sum_decomp_sum) = S ((S (S l)) * fs_v_dst_decomp_sumpositive)) /\ exists fs_q_dst_decomp_sumpositive_body_terminal. fs_u_dst_decomp_sumpositive = fs_q_dst_decomp_sumpositive_body_terminal * S ((S (S l)) * fs_v_dst_decomp_sumpositive) + (dst_positive_sum_decomp_sum))) /\ forall fs_i_dst_decomp_sumpositive_body_steps. (exists fs_lt_dst_decomp_sumpositive_body_steps_bound. fs_lt_dst_decomp_sumpositive_body_steps_bound + S fs_i_dst_decomp_sumpositive_body_steps = S l) -> exists fs_a_dst_decomp_sumpositive_body_steps fs_r_dst_decomp_sumpositive_body_steps fs_s_dst_decomp_sumpositive_body_steps. ((((exists fs_h_dst_decomp_sumpositive_body_steps_summand. fs_h_dst_decomp_sumpositive_body_steps_summand + S (fs_a_dst_decomp_sumpositive_body_steps) = S ((S (fs_i_dst_decomp_sumpositive_body_steps)) * dst_positive_scale_decomp_sum)) /\ exists fs_q_dst_decomp_sumpositive_body_steps_summand. dst_positive_code_decomp_sum = fs_q_dst_decomp_sumpositive_body_steps_summand * S ((S (fs_i_dst_decomp_sumpositive_body_steps)) * dst_positive_scale_decomp_sum) + (fs_a_dst_decomp_sumpositive_body_steps))) /\ ((((exists fs_h_dst_decomp_sumpositive_body_steps_partial. fs_h_dst_decomp_sumpositive_body_steps_partial + S (fs_r_dst_decomp_sumpositive_body_steps) = S ((S (fs_i_dst_decomp_sumpositive_body_steps)) * fs_v_dst_decomp_sumpositive)) /\ exists fs_q_dst_decomp_sumpositive_body_steps_partial. fs_u_dst_decomp_sumpositive = fs_q_dst_decomp_sumpositive_body_steps_partial * S ((S (fs_i_dst_decomp_sumpositive_body_steps)) * fs_v_dst_decomp_sumpositive) + (fs_r_dst_decomp_sumpositive_body_steps))) /\ ((((exists fs_h_dst_decomp_sumpositive_body_steps_successor. fs_h_dst_decomp_sumpositive_body_steps_successor + S (fs_s_dst_decomp_sumpositive_body_steps) = S ((S (S fs_i_dst_decomp_sumpositive_body_steps)) * fs_v_dst_decomp_sumpositive)) /\ exists fs_q_dst_decomp_sumpositive_body_steps_successor. fs_u_dst_decomp_sumpositive = fs_q_dst_decomp_sumpositive_body_steps_successor * S ((S (S fs_i_dst_decomp_sumpositive_body_steps)) * fs_v_dst_decomp_sumpositive) + (fs_s_dst_decomp_sumpositive_body_steps))) /\ fs_s_dst_decomp_sumpositive_body_steps = fs_r_dst_decomp_sumpositive_body_steps + fs_a_dst_decomp_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_decomp_sumnegative fs_v_dst_decomp_sumnegative. ((((exists fs_h_dst_decomp_sumnegative_body_start. fs_h_dst_decomp_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_decomp_sumnegative)) /\ exists fs_q_dst_decomp_sumnegative_body_start. fs_u_dst_decomp_sumnegative = fs_q_dst_decomp_sumnegative_body_start * S ((S (0)) * fs_v_dst_decomp_sumnegative) + (0))) /\ ((((exists fs_h_dst_decomp_sumnegative_body_terminal. fs_h_dst_decomp_sumnegative_body_terminal + S (dst_negative_sum_decomp_sum) = S ((S (S l)) * fs_v_dst_decomp_sumnegative)) /\ exists fs_q_dst_decomp_sumnegative_body_terminal. fs_u_dst_decomp_sumnegative = fs_q_dst_decomp_sumnegative_body_terminal * S ((S (S l)) * fs_v_dst_decomp_sumnegative) + (dst_negative_sum_decomp_sum))) /\ forall fs_i_dst_decomp_sumnegative_body_steps. (exists fs_lt_dst_decomp_sumnegative_body_steps_bound. fs_lt_dst_decomp_sumnegative_body_steps_bound + S fs_i_dst_decomp_sumnegative_body_steps = S l) -> exists fs_a_dst_decomp_sumnegative_body_steps fs_r_dst_decomp_sumnegative_body_steps fs_s_dst_decomp_sumnegative_body_steps. ((((exists fs_h_dst_decomp_sumnegative_body_steps_summand. fs_h_dst_decomp_sumnegative_body_steps_summand + S (fs_a_dst_decomp_sumnegative_body_steps) = S ((S (fs_i_dst_decomp_sumnegative_body_steps)) * dst_negative_scale_decomp_sum)) /\ exists fs_q_dst_decomp_sumnegative_body_steps_summand. dst_negative_code_decomp_sum = fs_q_dst_decomp_sumnegative_body_steps_summand * S ((S (fs_i_dst_decomp_sumnegative_body_steps)) * dst_negative_scale_decomp_sum) + (fs_a_dst_decomp_sumnegative_body_steps))) /\ ((((exists fs_h_dst_decomp_sumnegative_body_steps_partial. fs_h_dst_decomp_sumnegative_body_steps_partial + S (fs_r_dst_decomp_sumnegative_body_steps) = S ((S (fs_i_dst_decomp_sumnegative_body_steps)) * fs_v_dst_decomp_sumnegative)) /\ exists fs_q_dst_decomp_sumnegative_body_steps_partial. fs_u_dst_decomp_sumnegative = fs_q_dst_decomp_sumnegative_body_steps_partial * S ((S (fs_i_dst_decomp_sumnegative_body_steps)) * fs_v_dst_decomp_sumnegative) + (fs_r_dst_decomp_sumnegative_body_steps))) /\ ((((exists fs_h_dst_decomp_sumnegative_body_steps_successor. fs_h_dst_decomp_sumnegative_body_steps_successor + S (fs_s_dst_decomp_sumnegative_body_steps) = S ((S (S fs_i_dst_decomp_sumnegative_body_steps)) * fs_v_dst_decomp_sumnegative)) /\ exists fs_q_dst_decomp_sumnegative_body_steps_successor. fs_u_dst_decomp_sumnegative = fs_q_dst_decomp_sumnegative_body_steps_successor * S ((S (S fs_i_dst_decomp_sumnegative_body_steps)) * fs_v_dst_decomp_sumnegative) + (fs_s_dst_decomp_sumnegative_body_steps))) /\ fs_s_dst_decomp_sumnegative_body_steps = fs_r_dst_decomp_sumnegative_body_steps + fs_a_dst_decomp_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_decomp_sumresult ge_balance_negative_decomp_sumresult. (((((z) = 2 * (ge_balance_positive_decomp_sumresult) /\ (ge_balance_negative_decomp_sumresult) = 0) \/ exists ge_signed_half_decomp_sumresultdecode. (((z) = 2 * ge_signed_half_decomp_sumresultdecode + 1 /\ (ge_balance_positive_decomp_sumresult) = 0) /\ (ge_balance_negative_decomp_sumresult) = S ge_signed_half_decomp_sumresultdecode))) /\ ((dst_positive_sum_decomp_sum) + ge_balance_negative_decomp_sumresult = (dst_negative_sum_decomp_sum) + ge_balance_positive_decomp_sumresult))))))))) -> exists a b. ((exists dst_positive_code_decomp_prefix dst_positive_scale_decomp_prefix dst_negative_code_decomp_prefix dst_negative_scale_decomp_prefix dst_positive_sum_decomp_prefix dst_negative_sum_decomp_prefix. (((F) = (((((dst_positive_code_decomp_prefix) + (dst_positive_scale_decomp_prefix)) * S ((dst_positive_code_decomp_prefix) + (dst_positive_scale_decomp_prefix)) + ((dst_positive_scale_decomp_prefix) + (dst_positive_scale_decomp_prefix))) + (((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) * S ((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) + ((dst_negative_scale_decomp_prefix) + (dst_negative_scale_decomp_prefix)))) * S ((((dst_positive_code_decomp_prefix) + (dst_positive_scale_decomp_prefix)) * S ((dst_positive_code_decomp_prefix) + (dst_positive_scale_decomp_prefix)) + ((dst_positive_scale_decomp_prefix) + (dst_positive_scale_decomp_prefix))) + (((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) * S ((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) + ((dst_negative_scale_decomp_prefix) + (dst_negative_scale_decomp_prefix)))) + ((((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) * S ((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) + ((dst_negative_scale_decomp_prefix) + (dst_negative_scale_decomp_prefix))) + (((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) * S ((dst_negative_code_decomp_prefix) + (dst_negative_scale_decomp_prefix)) + ((dst_negative_scale_decomp_prefix) + (dst_negative_scale_decomp_prefix)))))) /\ (((exists fs_u_dst_decomp_prefixpositive fs_v_dst_decomp_prefixpositive. ((((exists fs_h_dst_decomp_prefixpositive_body_start. fs_h_dst_decomp_prefixpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_decomp_prefixpositive)) /\ exists fs_q_dst_decomp_prefixpositive_body_start. fs_u_dst_decomp_prefixpositive = fs_q_dst_decomp_prefixpositive_body_start * S ((S (0)) * fs_v_dst_decomp_prefixpositive) + (0))) /\ ((((exists fs_h_dst_decomp_prefixpositive_body_terminal. fs_h_dst_decomp_prefixpositive_body_terminal + S (dst_positive_sum_decomp_prefix) = S ((S (l)) * fs_v_dst_decomp_prefixpositive)) /\ exists fs_q_dst_decomp_prefixpositive_body_terminal. fs_u_dst_decomp_prefixpositive = fs_q_dst_decomp_prefixpositive_body_terminal * S ((S (l)) * fs_v_dst_decomp_prefixpositive) + (dst_positive_sum_decomp_prefix))) /\ forall fs_i_dst_decomp_prefixpositive_body_steps. (exists fs_lt_dst_decomp_prefixpositive_body_steps_bound. fs_lt_dst_decomp_prefixpositive_body_steps_bound + S fs_i_dst_decomp_prefixpositive_body_steps = l) -> exists fs_a_dst_decomp_prefixpositive_body_steps fs_r_dst_decomp_prefixpositive_body_steps fs_s_dst_decomp_prefixpositive_body_steps. ((((exists fs_h_dst_decomp_prefixpositive_body_steps_summand. fs_h_dst_decomp_prefixpositive_body_steps_summand + S (fs_a_dst_decomp_prefixpositive_body_steps) = S ((S (fs_i_dst_decomp_prefixpositive_body_steps)) * dst_positive_scale_decomp_prefix)) /\ exists fs_q_dst_decomp_prefixpositive_body_steps_summand. dst_positive_code_decomp_prefix = fs_q_dst_decomp_prefixpositive_body_steps_summand * S ((S (fs_i_dst_decomp_prefixpositive_body_steps)) * dst_positive_scale_decomp_prefix) + (fs_a_dst_decomp_prefixpositive_body_steps))) /\ ((((exists fs_h_dst_decomp_prefixpositive_body_steps_partial. fs_h_dst_decomp_prefixpositive_body_steps_partial + S (fs_r_dst_decomp_prefixpositive_body_steps) = S ((S (fs_i_dst_decomp_prefixpositive_body_steps)) * fs_v_dst_decomp_prefixpositive)) /\ exists fs_q_dst_decomp_prefixpositive_body_steps_partial. fs_u_dst_decomp_prefixpositive = fs_q_dst_decomp_prefixpositive_body_steps_partial * S ((S (fs_i_dst_decomp_prefixpositive_body_steps)) * fs_v_dst_decomp_prefixpositive) + (fs_r_dst_decomp_prefixpositive_body_steps))) /\ ((((exists fs_h_dst_decomp_prefixpositive_body_steps_successor. fs_h_dst_decomp_prefixpositive_body_steps_successor + S (fs_s_dst_decomp_prefixpositive_body_steps) = S ((S (S fs_i_dst_decomp_prefixpositive_body_steps)) * fs_v_dst_decomp_prefixpositive)) /\ exists fs_q_dst_decomp_prefixpositive_body_steps_successor. fs_u_dst_decomp_prefixpositive = fs_q_dst_decomp_prefixpositive_body_steps_successor * S ((S (S fs_i_dst_decomp_prefixpositive_body_steps)) * fs_v_dst_decomp_prefixpositive) + (fs_s_dst_decomp_prefixpositive_body_steps))) /\ fs_s_dst_decomp_prefixpositive_body_steps = fs_r_dst_decomp_prefixpositive_body_steps + fs_a_dst_decomp_prefixpositive_body_steps)))))) /\ (((exists fs_u_dst_decomp_prefixnegative fs_v_dst_decomp_prefixnegative. ((((exists fs_h_dst_decomp_prefixnegative_body_start. fs_h_dst_decomp_prefixnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_decomp_prefixnegative)) /\ exists fs_q_dst_decomp_prefixnegative_body_start. fs_u_dst_decomp_prefixnegative = fs_q_dst_decomp_prefixnegative_body_start * S ((S (0)) * fs_v_dst_decomp_prefixnegative) + (0))) /\ ((((exists fs_h_dst_decomp_prefixnegative_body_terminal. fs_h_dst_decomp_prefixnegative_body_terminal + S (dst_negative_sum_decomp_prefix) = S ((S (l)) * fs_v_dst_decomp_prefixnegative)) /\ exists fs_q_dst_decomp_prefixnegative_body_terminal. fs_u_dst_decomp_prefixnegative = fs_q_dst_decomp_prefixnegative_body_terminal * S ((S (l)) * fs_v_dst_decomp_prefixnegative) + (dst_negative_sum_decomp_prefix))) /\ forall fs_i_dst_decomp_prefixnegative_body_steps. (exists fs_lt_dst_decomp_prefixnegative_body_steps_bound. fs_lt_dst_decomp_prefixnegative_body_steps_bound + S fs_i_dst_decomp_prefixnegative_body_steps = l) -> exists fs_a_dst_decomp_prefixnegative_body_steps fs_r_dst_decomp_prefixnegative_body_steps fs_s_dst_decomp_prefixnegative_body_steps. ((((exists fs_h_dst_decomp_prefixnegative_body_steps_summand. fs_h_dst_decomp_prefixnegative_body_steps_summand + S (fs_a_dst_decomp_prefixnegative_body_steps) = S ((S (fs_i_dst_decomp_prefixnegative_body_steps)) * dst_negative_scale_decomp_prefix)) /\ exists fs_q_dst_decomp_prefixnegative_body_steps_summand. dst_negative_code_decomp_prefix = fs_q_dst_decomp_prefixnegative_body_steps_summand * S ((S (fs_i_dst_decomp_prefixnegative_body_steps)) * dst_negative_scale_decomp_prefix) + (fs_a_dst_decomp_prefixnegative_body_steps))) /\ ((((exists fs_h_dst_decomp_prefixnegative_body_steps_partial. fs_h_dst_decomp_prefixnegative_body_steps_partial + S (fs_r_dst_decomp_prefixnegative_body_steps) = S ((S (fs_i_dst_decomp_prefixnegative_body_steps)) * fs_v_dst_decomp_prefixnegative)) /\ exists fs_q_dst_decomp_prefixnegative_body_steps_partial. fs_u_dst_decomp_prefixnegative = fs_q_dst_decomp_prefixnegative_body_steps_partial * S ((S (fs_i_dst_decomp_prefixnegative_body_steps)) * fs_v_dst_decomp_prefixnegative) + (fs_r_dst_decomp_prefixnegative_body_steps))) /\ ((((exists fs_h_dst_decomp_prefixnegative_body_steps_successor. fs_h_dst_decomp_prefixnegative_body_steps_successor + S (fs_s_dst_decomp_prefixnegative_body_steps) = S ((S (S fs_i_dst_decomp_prefixnegative_body_steps)) * fs_v_dst_decomp_prefixnegative)) /\ exists fs_q_dst_decomp_prefixnegative_body_steps_successor. fs_u_dst_decomp_prefixnegative = fs_q_dst_decomp_prefixnegative_body_steps_successor * S ((S (S fs_i_dst_decomp_prefixnegative_body_steps)) * fs_v_dst_decomp_prefixnegative) + (fs_s_dst_decomp_prefixnegative_body_steps))) /\ fs_s_dst_decomp_prefixnegative_body_steps = fs_r_dst_decomp_prefixnegative_body_steps + fs_a_dst_decomp_prefixnegative_body_steps)))))) /\ (exists ge_balance_positive_decomp_prefixresult ge_balance_negative_decomp_prefixresult. (((((a) = 2 * (ge_balance_positive_decomp_prefixresult) /\ (ge_balance_negative_decomp_prefixresult) = 0) \/ exists ge_signed_half_decomp_prefixresultdecode. (((a) = 2 * ge_signed_half_decomp_prefixresultdecode + 1 /\ (ge_balance_positive_decomp_prefixresult) = 0) /\ (ge_balance_negative_decomp_prefixresult) = S ge_signed_half_decomp_prefixresultdecode))) /\ ((dst_positive_sum_decomp_prefix) + ge_balance_negative_decomp_prefixresult = (dst_negative_sum_decomp_prefix) + ge_balance_positive_decomp_prefixresult))))))))) /\ (((exists dst_positive_code_decomp_entry dst_positive_scale_decomp_entry dst_negative_code_decomp_entry dst_negative_scale_decomp_entry dst_positive_decomp_entry dst_negative_decomp_entry. (((F) = (((((dst_positive_code_decomp_entry) + (dst_positive_scale_decomp_entry)) * S ((dst_positive_code_decomp_entry) + (dst_positive_scale_decomp_entry)) + ((dst_positive_scale_decomp_entry) + (dst_positive_scale_decomp_entry))) + (((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) * S ((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) + ((dst_negative_scale_decomp_entry) + (dst_negative_scale_decomp_entry)))) * S ((((dst_positive_code_decomp_entry) + (dst_positive_scale_decomp_entry)) * S ((dst_positive_code_decomp_entry) + (dst_positive_scale_decomp_entry)) + ((dst_positive_scale_decomp_entry) + (dst_positive_scale_decomp_entry))) + (((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) * S ((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) + ((dst_negative_scale_decomp_entry) + (dst_negative_scale_decomp_entry)))) + ((((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) * S ((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) + ((dst_negative_scale_decomp_entry) + (dst_negative_scale_decomp_entry))) + (((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) * S ((dst_negative_code_decomp_entry) + (dst_negative_scale_decomp_entry)) + ((dst_negative_scale_decomp_entry) + (dst_negative_scale_decomp_entry)))))) /\ (((((exists ff_h_pvs_decomp_entrypositive. ff_h_pvs_decomp_entrypositive + S (dst_positive_decomp_entry) = S ((S (l)) * dst_positive_scale_decomp_entry)) /\ exists ff_q_pvs_decomp_entrypositive. dst_positive_code_decomp_entry = ff_q_pvs_decomp_entrypositive * S ((S (l)) * dst_positive_scale_decomp_entry) + (dst_positive_decomp_entry))) /\ (((((exists ff_h_pvs_decomp_entrynegative. ff_h_pvs_decomp_entrynegative + S (dst_negative_decomp_entry) = S ((S (l)) * dst_negative_scale_decomp_entry)) /\ exists ff_q_pvs_decomp_entrynegative. dst_negative_code_decomp_entry = ff_q_pvs_decomp_entrynegative * S ((S (l)) * dst_negative_scale_decomp_entry) + (dst_negative_decomp_entry))) /\ (exists ge_balance_positive_decomp_entryvalue ge_balance_negative_decomp_entryvalue. (((((b) = 2 * (ge_balance_positive_decomp_entryvalue) /\ (ge_balance_negative_decomp_entryvalue) = 0) \/ exists ge_signed_half_decomp_entryvaluedecode. (((b) = 2 * ge_signed_half_decomp_entryvaluedecode + 1 /\ (ge_balance_positive_decomp_entryvalue) = 0) /\ (ge_balance_negative_decomp_entryvalue) = S ge_signed_half_decomp_entryvaluedecode))) /\ ((dst_positive_decomp_entry) + ge_balance_negative_decomp_entryvalue = (dst_negative_decomp_entry) + ge_balance_positive_decomp_entryvalue))))))))) /\ (exists dsa_ap_decomp_add dsa_an_decomp_add dsa_bp_decomp_add dsa_bn_decomp_add dsa_cp_decomp_add dsa_cn_decomp_add. (((((a) = 2 * (dsa_ap_decomp_add) /\ (dsa_an_decomp_add) = 0) \/ exists ge_signed_half_decomp_addleft. (((a) = 2 * ge_signed_half_decomp_addleft + 1 /\ (dsa_ap_decomp_add) = 0) /\ (dsa_an_decomp_add) = S ge_signed_half_decomp_addleft))) /\ ((((((b) = 2 * (dsa_bp_decomp_add) /\ (dsa_bn_decomp_add) = 0) \/ exists ge_signed_half_decomp_addright. (((b) = 2 * ge_signed_half_decomp_addright + 1 /\ (dsa_bp_decomp_add) = 0) /\ (dsa_bn_decomp_add) = S ge_signed_half_decomp_addright))) /\ ((((((z) = 2 * (dsa_cp_decomp_add) /\ (dsa_cn_decomp_add) = 0) \/ exists ge_signed_half_decomp_addoutput. (((z) = 2 * ge_signed_half_decomp_addoutput + 1 /\ (dsa_cp_decomp_add) = 0) /\ (dsa_cn_decomp_add) = S ge_signed_half_decomp_addoutput))) /\ ((dsa_ap_decomp_add + dsa_bp_decomp_add) + dsa_cn_decomp_add = (dsa_an_decomp_add + dsa_bn_decomp_add) + dsa_cp_decomp_add))))))))))

Complete tactic proof in conservative notation

All 90 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

90 script commands · 20 reading checkpoints · 4 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 (2)
divisor signed sum from componentsdivisor signed table at from components
01Fix variables and assumptionsL1–4

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

  1. L1
    intro F
  2. L2
    intro l
  3. L3
    intro z
  4. L4
    intro hs
02Separate the logical casesL5–13

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

  1. L5
    cases hs
  2. L6
    cases hs_witness
  3. L7
    cases hs_witness_witness
  4. L8
    cases hs_witness_witness_witness
  5. L9
    cases hs_witness_witness_witness_witness
  6. L10
    cases hs_witness_witness_witness_witness_witness
  7. L11
    cases hs_witness_witness_witness_witness_witness_witness
  8. L12
    cases hs_witness_witness_witness_witness_witness_witness_right
  9. L13
    cases hs_witness_witness_witness_witness_witness_witness_right_right
03Establish hpL14–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta sum succ decompose.

  1. L14
    have hp : ∃ dsa_summand_decomp_positive. ∃ dsa_partial_decomp_positive. BetaAt(x,x1,l,dsa_summand_decomp_positive) ∧ (Sum(x,x1,l,dsa_partial_decomp_positive) ∧ x4 = dsa_partial_decomp_positive + dsa_summand_decomp_positive)Definitions: BetaAt(x,x1,l,dsa_summand_decomp_positive)Sum(x,x1,l,dsa_partial_decomp_positive)Original native command in the exact edition
  2. L15
    specialize beta_sum_succ_decompose (x)
  3. L16
    specialize beta_sum_succ_decompose (x1)
  4. L17
    specialize beta_sum_succ_decompose (l)
  5. L18
    specialize beta_sum_succ_decompose (x4)
  6. L19
    apply beta_sum_succ_decompose
  7. L20
    exact hs_witness_witness_witness_witness_witness_witness_right_left
04Separate the logical casesL21–24

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

  1. L21
    cases hp
  2. L22
    cases hp_witness
  3. L23
    cases hp_witness_witness
  4. L24
    cases hp_witness_witness_right
05Establish hnL25–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta sum succ decompose.

  1. L25
    have hn : ∃ dsa_summand_decomp_negative. ∃ dsa_partial_decomp_negative. BetaAt(x2,x3,l,dsa_summand_decomp_negative) ∧ (Sum(x2,x3,l,dsa_partial_decomp_negative) ∧ x5 = dsa_partial_decomp_negative + dsa_summand_decomp_negative)Definitions: BetaAt(x2,x3,l,dsa_summand_decomp_negative)Sum(x2,x3,l,dsa_partial_decomp_negative)Original native command in the exact edition
  2. L26
    specialize beta_sum_succ_decompose (x2)
  3. L27
    specialize beta_sum_succ_decompose (x3)
  4. L28
    specialize beta_sum_succ_decompose (l)
  5. L29
    specialize beta_sum_succ_decompose (x5)
  6. L30
    apply beta_sum_succ_decompose
  7. L31
    exact hs_witness_witness_witness_witness_witness_witness_right_right_left
06Separate the logical casesL32–35

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

  1. L32
    cases hn
  2. L33
    cases hn_witness
  3. L34
    cases hn_witness_witness
  4. L35
    cases hn_witness_witness_right
07Establish haL36–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed balance total.

  1. L36
    have ha : ∃ a. SignedBalance(a,x7,x9)Definitions: SignedBalance(a,x7,x9)Original native command in the exact edition
  2. L37
    specialize signed_balance_total (x7)
  3. L38
    specialize signed_balance_total (x9)
  4. L39
    apply signed_balance_total
08Separate the logical casesL40–40

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

  1. L40
    cases ha
09Establish hbL41–44

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed balance total.

  1. L41
    have hb : ∃ b. SignedBalance(b,x6,x8)Definitions: SignedBalance(b,x6,x8)Original native command in the exact edition
  2. L42
    specialize signed_balance_total (x6)
  3. L43
    specialize signed_balance_total (x8)
  4. L44
    apply signed_balance_total
10Separate the logical casesL45–45

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

  1. L45
    cases hb
11Construct an explicit witnessL46–47

Supply the displayed value, then prove that it has the required property.

  1. L46
    exists x10
  2. L47
    exists x11
12Separate the logical casesL48–48

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

  1. L48
    split
13Use earlier factsL49–58

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L49
    specialize divisor_signed_sum_from_components (F)
  2. L50
    specialize divisor_signed_sum_from_components (x)
  3. L51
    specialize divisor_signed_sum_from_components (x1)
  4. L52
    specialize divisor_signed_sum_from_components (x2)
  5. L53
    specialize divisor_signed_sum_from_components (x3)
  6. L54
    specialize divisor_signed_sum_from_components (l)
  7. L55
    specialize divisor_signed_sum_from_components (x7)
  8. L56
    specialize divisor_signed_sum_from_components (x9)
  9. L57
    specialize divisor_signed_sum_from_components (x10)
  10. L58
    apply divisor_signed_sum_from_components
14Use earlier factsL59–62

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L59
    exact hs_witness_witness_witness_witness_witness_witness_left
  2. L60
    exact hp_witness_witness_right_left
  3. L61
    exact hn_witness_witness_right_left
  4. L62
    exact ha_witness
15Separate the logical casesL63–63

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

  1. L63
    split
16Use earlier factsL64–73

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L64
    specialize divisor_signed_table_at_from_components (F)
  2. L65
    specialize divisor_signed_table_at_from_components (x)
  3. L66
    specialize divisor_signed_table_at_from_components (x1)
  4. L67
    specialize divisor_signed_table_at_from_components (x2)
  5. L68
    specialize divisor_signed_table_at_from_components (x3)
  6. L69
    specialize divisor_signed_table_at_from_components (l)
  7. L70
    specialize divisor_signed_table_at_from_components (x6)
  8. L71
    specialize divisor_signed_table_at_from_components (x8)
  9. L72
    specialize divisor_signed_table_at_from_components (x11)
  10. L73
    apply divisor_signed_table_at_from_components
17Use earlier factsL74–83

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L74
    exact hs_witness_witness_witness_witness_witness_witness_left
  2. L75
    exact hp_witness_witness_left
  3. L76
    exact hn_witness_witness_left
  4. L77
    exact hb_witness
  5. L78
    specialize gaussian_signed_add_of_balances (x10)
  6. L79
    specialize gaussian_signed_add_of_balances (x11)
  7. L80
    specialize gaussian_signed_add_of_balances (z)
  8. L81
    specialize gaussian_signed_add_of_balances (x7)
  9. L82
    specialize gaussian_signed_add_of_balances (x9)
  10. L83
    specialize gaussian_signed_add_of_balances (x6)
18Use earlier factsL84–87

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L84
    specialize gaussian_signed_add_of_balances (x8)
  2. L85
    apply gaussian_signed_add_of_balances
  3. L86
    exact ha_witness
  4. L87
    exact hb_witness
19Calculate and transport equalitiesL88–89

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L88
    rewrite hp_witness_witness_right_right at hs_witness_witness_witness_witness_witness_witness_right_right_right
  2. L89
    rewrite hn_witness_witness_right_right at hs_witness_witness_witness_witness_witness_witness_right_right_right
20Use earlier factsL90–90

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L90
    exact hs_witness_witness_witness_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 90 lines
  1. 0001intro F
  2. 0002intro l
  3. 0003intro z
  4. 0004intro hs
  5. 0005cases hs
  6. 0006cases hs_witness
  7. 0007cases hs_witness_witness
  8. 0008cases hs_witness_witness_witness
  9. 0009cases hs_witness_witness_witness_witness
  10. 0010cases hs_witness_witness_witness_witness_witness
  11. 0011cases hs_witness_witness_witness_witness_witness_witness
  12. 0012cases hs_witness_witness_witness_witness_witness_witness_right
  13. 0013cases hs_witness_witness_witness_witness_witness_witness_right_right
  14. 0014have hp : ∃ dsa_summand_decomp_positive. ∃ dsa_partial_decomp_positive. BetaAt(x,x1,l,dsa_summand_decomp_positive) ∧ (Sum(x,x1,l,dsa_partial_decomp_positive) ∧ x4 = dsa_partial_decomp_positive + dsa_summand_decomp_positive)
  15. 0015specialize beta_sum_succ_decompose (x)
  16. 0016specialize beta_sum_succ_decompose (x1)
  17. 0017specialize beta_sum_succ_decompose (l)
  18. 0018specialize beta_sum_succ_decompose (x4)
  19. 0019apply beta_sum_succ_decompose
  20. 0020exact hs_witness_witness_witness_witness_witness_witness_right_left
  21. 0021cases hp
  22. 0022cases hp_witness
  23. 0023cases hp_witness_witness
  24. 0024cases hp_witness_witness_right
  25. 0025have hn : ∃ dsa_summand_decomp_negative. ∃ dsa_partial_decomp_negative. BetaAt(x2,x3,l,dsa_summand_decomp_negative) ∧ (Sum(x2,x3,l,dsa_partial_decomp_negative) ∧ x5 = dsa_partial_decomp_negative + dsa_summand_decomp_negative)
  26. 0026specialize beta_sum_succ_decompose (x2)
  27. 0027specialize beta_sum_succ_decompose (x3)
  28. 0028specialize beta_sum_succ_decompose (l)
  29. 0029specialize beta_sum_succ_decompose (x5)
  30. 0030apply beta_sum_succ_decompose
  31. 0031exact hs_witness_witness_witness_witness_witness_witness_right_right_left
  32. 0032cases hn
  33. 0033cases hn_witness
  34. 0034cases hn_witness_witness
  35. 0035cases hn_witness_witness_right
  36. 0036have ha : ∃ a. SignedBalance(a,x7,x9)
  37. 0037specialize signed_balance_total (x7)
  38. 0038specialize signed_balance_total (x9)
  39. 0039apply signed_balance_total
  40. 0040cases ha
  41. 0041have hb : ∃ b. SignedBalance(b,x6,x8)
  42. 0042specialize signed_balance_total (x6)
  43. 0043specialize signed_balance_total (x8)
  44. 0044apply signed_balance_total
  45. 0045cases hb
  46. 0046exists x10
  47. 0047exists x11
  48. 0048split
  49. 0049specialize divisor_signed_sum_from_components (F)
  50. 0050specialize divisor_signed_sum_from_components (x)
  51. 0051specialize divisor_signed_sum_from_components (x1)
  52. 0052specialize divisor_signed_sum_from_components (x2)
  53. 0053specialize divisor_signed_sum_from_components (x3)
  54. 0054specialize divisor_signed_sum_from_components (l)
  55. 0055specialize divisor_signed_sum_from_components (x7)
  56. 0056specialize divisor_signed_sum_from_components (x9)
  57. 0057specialize divisor_signed_sum_from_components (x10)
  58. 0058apply divisor_signed_sum_from_components
  59. 0059exact hs_witness_witness_witness_witness_witness_witness_left
  60. 0060exact hp_witness_witness_right_left
  61. 0061exact hn_witness_witness_right_left
  62. 0062exact ha_witness
  63. 0063split
  64. 0064specialize divisor_signed_table_at_from_components (F)
  65. 0065specialize divisor_signed_table_at_from_components (x)
  66. 0066specialize divisor_signed_table_at_from_components (x1)
  67. 0067specialize divisor_signed_table_at_from_components (x2)
  68. 0068specialize divisor_signed_table_at_from_components (x3)
  69. 0069specialize divisor_signed_table_at_from_components (l)
  70. 0070specialize divisor_signed_table_at_from_components (x6)
  71. 0071specialize divisor_signed_table_at_from_components (x8)
  72. 0072specialize divisor_signed_table_at_from_components (x11)
  73. 0073apply divisor_signed_table_at_from_components
  74. 0074exact hs_witness_witness_witness_witness_witness_witness_left
  75. 0075exact hp_witness_witness_left
  76. 0076exact hn_witness_witness_left
  77. 0077exact hb_witness
  78. 0078specialize gaussian_signed_add_of_balances (x10)
  79. 0079specialize gaussian_signed_add_of_balances (x11)
  80. 0080specialize gaussian_signed_add_of_balances (z)
  81. 0081specialize gaussian_signed_add_of_balances (x7)
  82. 0082specialize gaussian_signed_add_of_balances (x9)
  83. 0083specialize gaussian_signed_add_of_balances (x6)
  84. 0084specialize gaussian_signed_add_of_balances (x8)
  85. 0085apply gaussian_signed_add_of_balances
  86. 0086exact ha_witness
  87. 0087exact hb_witness
  88. 0088rewrite hp_witness_witness_right_right at hs_witness_witness_witness_witness_witness_witness_right_right_right
  89. 0089rewrite hn_witness_witness_right_right at hs_witness_witness_witness_witness_witness_witness_right_right_right
  90. 0090exact hs_witness_witness_witness_witness_witness_witness_right_right_right