DT0009

dirichlet_convolution_zero_prefix_sum

The genuine one-entry fold of an inclusive zero summand prefix is canonical zero, without restricting either input value at zero.

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.

The strict remainder is an actual inclusive prefix through k with an S k-entry fold; the future input at S k is excluded. A genuine table extension supplies the endpoint. The at-one identity inspects or constructs the real two-entry masked sum. No recurrence, inverse, or omitted summand value is assumed as a conclusion-bearing premise.

Exact theorem in conservative defined notation

∀ F. ∀ G. ∀ n. ∀ M. DirichletPrefix(F,G,n,0,M) → SignedPrefixSum(M,1,0)

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

Definition DAG

SignedPrefixSum(F,l,z) · 1DirichletPrefix(F,G,n,l,M) · 1

Actual proof prerequisites

signed_prefix_sum_zero_exists · checked external prerequisitele_zero · checked external prerequisitele_of_succ_le_succ · checked external prerequisitedirichlet_convolution_entry_omitted_value · checked external prerequisitele_refl · checked external prerequisite
Original expanded first-order statement 
forall F G n M. (((exists dst_positive_code_zero_prefixtable dst_positive_scale_zero_prefixtable dst_negative_code_zero_prefixtable dst_negative_scale_zero_prefixtable. (((M) = (((((dst_positive_code_zero_prefixtable) + (dst_positive_scale_zero_prefixtable)) * S ((dst_positive_code_zero_prefixtable) + (dst_positive_scale_zero_prefixtable)) + ((dst_positive_scale_zero_prefixtable) + (dst_positive_scale_zero_prefixtable))) + (((dst_negative_code_zero_prefixtable) + (dst_negative_scale_zero_prefixtable)) * S ((dst_negative_code_zero_prefixtable) + (dst_negative_scale_zero_prefixtable)) + ((dst_negative_scale_zero_prefixtable) + (dst_negative_scale_zero_prefixtable)))) * S ((((dst_positive_code_zero_prefixtable) + (dst_positive_scale_zero_prefixtable)) * S ((dst_positive_code_zero_prefixtable) + (dst_positive_scale_zero_prefixtable)) + ((dst_positive_scale_zero_prefixtable) + (dst_positive_scale_zero_prefixtable))) + (((dst_negative_code_zero_prefixtable) + (dst_negative_scale_zero_prefixtable)) * S ((dst_negative_code_zero_prefixtable) + (dst_negative_scale_zero_prefixtable)) + ((dst_negative_scale_zero_prefixtable) + (dst_negative_scale_zero_prefixtable)))) + ((((dst_negative_code_zero_prefixtable) + (dst_negative_scale_zero_prefixtable)) * S ((dst_negative_code_zero_prefixtable) + (dst_negative_scale_zero_prefixtable)) + ((dst_negative_scale_zero_prefixtable) + (dst_negative_scale_zero_prefixtable))) + (((dst_negative_code_zero_prefixtable) + (dst_negative_scale_zero_prefixtable)) * S ((dst_negative_code_zero_prefixtable) + (dst_negative_scale_zero_prefixtable)) + ((dst_negative_scale_zero_prefixtable) + (dst_negative_scale_zero_prefixtable)))))) /\ (forall dst_index_zero_prefixtable. (exists pvs_le_gap_zero_prefixtabledomain. pvs_le_gap_zero_prefixtabledomain + (dst_index_zero_prefixtable) = (0)) -> exists dst_positive_zero_prefixtable dst_negative_zero_prefixtable dst_value_zero_prefixtable. ((((exists ff_h_pvs_zero_prefixtableentrypositive. ff_h_pvs_zero_prefixtableentrypositive + S (dst_positive_zero_prefixtable) = S ((S (dst_index_zero_prefixtable)) * dst_positive_scale_zero_prefixtable)) /\ exists ff_q_pvs_zero_prefixtableentrypositive. dst_positive_code_zero_prefixtable = ff_q_pvs_zero_prefixtableentrypositive * S ((S (dst_index_zero_prefixtable)) * dst_positive_scale_zero_prefixtable) + (dst_positive_zero_prefixtable))) /\ (((((exists ff_h_pvs_zero_prefixtableentrynegative. ff_h_pvs_zero_prefixtableentrynegative + S (dst_negative_zero_prefixtable) = S ((S (dst_index_zero_prefixtable)) * dst_negative_scale_zero_prefixtable)) /\ exists ff_q_pvs_zero_prefixtableentrynegative. dst_negative_code_zero_prefixtable = ff_q_pvs_zero_prefixtableentrynegative * S ((S (dst_index_zero_prefixtable)) * dst_negative_scale_zero_prefixtable) + (dst_negative_zero_prefixtable))) /\ (exists ge_balance_positive_zero_prefixtableentryvalue ge_balance_negative_zero_prefixtableentryvalue. (((((dst_value_zero_prefixtable) = 2 * (ge_balance_positive_zero_prefixtableentryvalue) /\ (ge_balance_negative_zero_prefixtableentryvalue) = 0) \/ exists ge_signed_half_zero_prefixtableentryvaluedecode. (((dst_value_zero_prefixtable) = 2 * ge_signed_half_zero_prefixtableentryvaluedecode + 1 /\ (ge_balance_positive_zero_prefixtableentryvalue) = 0) /\ (ge_balance_negative_zero_prefixtableentryvalue) = S ge_signed_half_zero_prefixtableentryvaluedecode))) /\ ((dst_positive_zero_prefixtable) + ge_balance_negative_zero_prefixtableentryvalue = (dst_negative_zero_prefixtable) + ge_balance_positive_zero_prefixtableentryvalue))))))))) /\ (forall dc_index_zero_prefix dc_value_zero_prefix. (exists pvs_le_gap_zero_prefixdomain. pvs_le_gap_zero_prefixdomain + (dc_index_zero_prefix) = (0)) -> (exists dst_positive_code_zero_prefixlookup dst_positive_scale_zero_prefixlookup dst_negative_code_zero_prefixlookup dst_negative_scale_zero_prefixlookup dst_positive_zero_prefixlookup dst_negative_zero_prefixlookup. (((M) = (((((dst_positive_code_zero_prefixlookup) + (dst_positive_scale_zero_prefixlookup)) * S ((dst_positive_code_zero_prefixlookup) + (dst_positive_scale_zero_prefixlookup)) + ((dst_positive_scale_zero_prefixlookup) + (dst_positive_scale_zero_prefixlookup))) + (((dst_negative_code_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup)) * S ((dst_negative_code_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup)) + ((dst_negative_scale_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup)))) * S ((((dst_positive_code_zero_prefixlookup) + (dst_positive_scale_zero_prefixlookup)) * S ((dst_positive_code_zero_prefixlookup) + (dst_positive_scale_zero_prefixlookup)) + ((dst_positive_scale_zero_prefixlookup) + (dst_positive_scale_zero_prefixlookup))) + (((dst_negative_code_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup)) * S ((dst_negative_code_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup)) + ((dst_negative_scale_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup)))) + ((((dst_negative_code_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup)) * S ((dst_negative_code_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup)) + ((dst_negative_scale_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup))) + (((dst_negative_code_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup)) * S ((dst_negative_code_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup)) + ((dst_negative_scale_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup)))))) /\ (((((exists ff_h_pvs_zero_prefixlookuppositive. ff_h_pvs_zero_prefixlookuppositive + S (dst_positive_zero_prefixlookup) = S ((S (dc_index_zero_prefix)) * dst_positive_scale_zero_prefixlookup)) /\ exists ff_q_pvs_zero_prefixlookuppositive. dst_positive_code_zero_prefixlookup = ff_q_pvs_zero_prefixlookuppositive * S ((S (dc_index_zero_prefix)) * dst_positive_scale_zero_prefixlookup) + (dst_positive_zero_prefixlookup))) /\ (((((exists ff_h_pvs_zero_prefixlookupnegative. ff_h_pvs_zero_prefixlookupnegative + S (dst_negative_zero_prefixlookup) = S ((S (dc_index_zero_prefix)) * dst_negative_scale_zero_prefixlookup)) /\ exists ff_q_pvs_zero_prefixlookupnegative. dst_negative_code_zero_prefixlookup = ff_q_pvs_zero_prefixlookupnegative * S ((S (dc_index_zero_prefix)) * dst_negative_scale_zero_prefixlookup) + (dst_negative_zero_prefixlookup))) /\ (exists ge_balance_positive_zero_prefixlookupvalue ge_balance_negative_zero_prefixlookupvalue. (((((dc_value_zero_prefix) = 2 * (ge_balance_positive_zero_prefixlookupvalue) /\ (ge_balance_negative_zero_prefixlookupvalue) = 0) \/ exists ge_signed_half_zero_prefixlookupvaluedecode. (((dc_value_zero_prefix) = 2 * ge_signed_half_zero_prefixlookupvaluedecode + 1 /\ (ge_balance_positive_zero_prefixlookupvalue) = 0) /\ (ge_balance_negative_zero_prefixlookupvalue) = S ge_signed_half_zero_prefixlookupvaluedecode))) /\ ((dst_positive_zero_prefixlookup) + ge_balance_negative_zero_prefixlookupvalue = (dst_negative_zero_prefixlookup) + ge_balance_positive_zero_prefixlookupvalue))))))))) -> ((((~((dc_index_zero_prefix)=0)) /\ (exists dc_quotient_zero_prefixentry dc_left_zero_prefixentry dc_right_zero_prefixentry. (((n)=(dc_index_zero_prefix)*dc_quotient_zero_prefixentry) /\ (((exists dst_positive_code_zero_prefixentryleft dst_positive_scale_zero_prefixentryleft dst_negative_code_zero_prefixentryleft dst_negative_scale_zero_prefixentryleft dst_positive_zero_prefixentryleft dst_negative_zero_prefixentryleft. (((F) = (((((dst_positive_code_zero_prefixentryleft) + (dst_positive_scale_zero_prefixentryleft)) * S ((dst_positive_code_zero_prefixentryleft) + (dst_positive_scale_zero_prefixentryleft)) + ((dst_positive_scale_zero_prefixentryleft) + (dst_positive_scale_zero_prefixentryleft))) + (((dst_negative_code_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft)) * S ((dst_negative_code_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft)) + ((dst_negative_scale_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft)))) * S ((((dst_positive_code_zero_prefixentryleft) + (dst_positive_scale_zero_prefixentryleft)) * S ((dst_positive_code_zero_prefixentryleft) + (dst_positive_scale_zero_prefixentryleft)) + ((dst_positive_scale_zero_prefixentryleft) + (dst_positive_scale_zero_prefixentryleft))) + (((dst_negative_code_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft)) * S ((dst_negative_code_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft)) + ((dst_negative_scale_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft)))) + ((((dst_negative_code_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft)) * S ((dst_negative_code_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft)) + ((dst_negative_scale_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft))) + (((dst_negative_code_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft)) * S ((dst_negative_code_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft)) + ((dst_negative_scale_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft)))))) /\ (((((exists ff_h_pvs_zero_prefixentryleftpositive. ff_h_pvs_zero_prefixentryleftpositive + S (dst_positive_zero_prefixentryleft) = S ((S (dc_index_zero_prefix)) * dst_positive_scale_zero_prefixentryleft)) /\ exists ff_q_pvs_zero_prefixentryleftpositive. dst_positive_code_zero_prefixentryleft = ff_q_pvs_zero_prefixentryleftpositive * S ((S (dc_index_zero_prefix)) * dst_positive_scale_zero_prefixentryleft) + (dst_positive_zero_prefixentryleft))) /\ (((((exists ff_h_pvs_zero_prefixentryleftnegative. ff_h_pvs_zero_prefixentryleftnegative + S (dst_negative_zero_prefixentryleft) = S ((S (dc_index_zero_prefix)) * dst_negative_scale_zero_prefixentryleft)) /\ exists ff_q_pvs_zero_prefixentryleftnegative. dst_negative_code_zero_prefixentryleft = ff_q_pvs_zero_prefixentryleftnegative * S ((S (dc_index_zero_prefix)) * dst_negative_scale_zero_prefixentryleft) + (dst_negative_zero_prefixentryleft))) /\ (exists ge_balance_positive_zero_prefixentryleftvalue ge_balance_negative_zero_prefixentryleftvalue. (((((dc_left_zero_prefixentry) = 2 * (ge_balance_positive_zero_prefixentryleftvalue) /\ (ge_balance_negative_zero_prefixentryleftvalue) = 0) \/ exists ge_signed_half_zero_prefixentryleftvaluedecode. (((dc_left_zero_prefixentry) = 2 * ge_signed_half_zero_prefixentryleftvaluedecode + 1 /\ (ge_balance_positive_zero_prefixentryleftvalue) = 0) /\ (ge_balance_negative_zero_prefixentryleftvalue) = S ge_signed_half_zero_prefixentryleftvaluedecode))) /\ ((dst_positive_zero_prefixentryleft) + ge_balance_negative_zero_prefixentryleftvalue = (dst_negative_zero_prefixentryleft) + ge_balance_positive_zero_prefixentryleftvalue))))))))) /\ (((exists dst_positive_code_zero_prefixentryright dst_positive_scale_zero_prefixentryright dst_negative_code_zero_prefixentryright dst_negative_scale_zero_prefixentryright dst_positive_zero_prefixentryright dst_negative_zero_prefixentryright. (((G) = (((((dst_positive_code_zero_prefixentryright) + (dst_positive_scale_zero_prefixentryright)) * S ((dst_positive_code_zero_prefixentryright) + (dst_positive_scale_zero_prefixentryright)) + ((dst_positive_scale_zero_prefixentryright) + (dst_positive_scale_zero_prefixentryright))) + (((dst_negative_code_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright)) * S ((dst_negative_code_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright)) + ((dst_negative_scale_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright)))) * S ((((dst_positive_code_zero_prefixentryright) + (dst_positive_scale_zero_prefixentryright)) * S ((dst_positive_code_zero_prefixentryright) + (dst_positive_scale_zero_prefixentryright)) + ((dst_positive_scale_zero_prefixentryright) + (dst_positive_scale_zero_prefixentryright))) + (((dst_negative_code_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright)) * S ((dst_negative_code_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright)) + ((dst_negative_scale_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright)))) + ((((dst_negative_code_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright)) * S ((dst_negative_code_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright)) + ((dst_negative_scale_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright))) + (((dst_negative_code_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright)) * S ((dst_negative_code_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright)) + ((dst_negative_scale_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright)))))) /\ (((((exists ff_h_pvs_zero_prefixentryrightpositive. ff_h_pvs_zero_prefixentryrightpositive + S (dst_positive_zero_prefixentryright) = S ((S (dc_quotient_zero_prefixentry)) * dst_positive_scale_zero_prefixentryright)) /\ exists ff_q_pvs_zero_prefixentryrightpositive. dst_positive_code_zero_prefixentryright = ff_q_pvs_zero_prefixentryrightpositive * S ((S (dc_quotient_zero_prefixentry)) * dst_positive_scale_zero_prefixentryright) + (dst_positive_zero_prefixentryright))) /\ (((((exists ff_h_pvs_zero_prefixentryrightnegative. ff_h_pvs_zero_prefixentryrightnegative + S (dst_negative_zero_prefixentryright) = S ((S (dc_quotient_zero_prefixentry)) * dst_negative_scale_zero_prefixentryright)) /\ exists ff_q_pvs_zero_prefixentryrightnegative. dst_negative_code_zero_prefixentryright = ff_q_pvs_zero_prefixentryrightnegative * S ((S (dc_quotient_zero_prefixentry)) * dst_negative_scale_zero_prefixentryright) + (dst_negative_zero_prefixentryright))) /\ (exists ge_balance_positive_zero_prefixentryrightvalue ge_balance_negative_zero_prefixentryrightvalue. (((((dc_right_zero_prefixentry) = 2 * (ge_balance_positive_zero_prefixentryrightvalue) /\ (ge_balance_negative_zero_prefixentryrightvalue) = 0) \/ exists ge_signed_half_zero_prefixentryrightvaluedecode. (((dc_right_zero_prefixentry) = 2 * ge_signed_half_zero_prefixentryrightvaluedecode + 1 /\ (ge_balance_positive_zero_prefixentryrightvalue) = 0) /\ (ge_balance_negative_zero_prefixentryrightvalue) = S ge_signed_half_zero_prefixentryrightvaluedecode))) /\ ((dst_positive_zero_prefixentryright) + ge_balance_negative_zero_prefixentryrightvalue = (dst_negative_zero_prefixentryright) + ge_balance_positive_zero_prefixentryrightvalue))))))))) /\ (exists sto_ap_zero_prefixentryproduct sto_an_zero_prefixentryproduct sto_bp_zero_prefixentryproduct sto_bn_zero_prefixentryproduct sto_cp_zero_prefixentryproduct sto_cn_zero_prefixentryproduct. (((((dc_left_zero_prefixentry) = 2 * (sto_ap_zero_prefixentryproduct) /\ (sto_an_zero_prefixentryproduct) = 0) \/ exists ge_signed_half_zero_prefixentryproductleft. (((dc_left_zero_prefixentry) = 2 * ge_signed_half_zero_prefixentryproductleft + 1 /\ (sto_ap_zero_prefixentryproduct) = 0) /\ (sto_an_zero_prefixentryproduct) = S ge_signed_half_zero_prefixentryproductleft))) /\ ((((((dc_right_zero_prefixentry) = 2 * (sto_bp_zero_prefixentryproduct) /\ (sto_bn_zero_prefixentryproduct) = 0) \/ exists ge_signed_half_zero_prefixentryproductright. (((dc_right_zero_prefixentry) = 2 * ge_signed_half_zero_prefixentryproductright + 1 /\ (sto_bp_zero_prefixentryproduct) = 0) /\ (sto_bn_zero_prefixentryproduct) = S ge_signed_half_zero_prefixentryproductright))) /\ ((((((dc_value_zero_prefix) = 2 * (sto_cp_zero_prefixentryproduct) /\ (sto_cn_zero_prefixentryproduct) = 0) \/ exists ge_signed_half_zero_prefixentryproductoutput. (((dc_value_zero_prefix) = 2 * ge_signed_half_zero_prefixentryproductoutput + 1 /\ (sto_cp_zero_prefixentryproduct) = 0) /\ (sto_cn_zero_prefixentryproduct) = S ge_signed_half_zero_prefixentryproductoutput))) /\ ((sto_ap_zero_prefixentryproduct * sto_bp_zero_prefixentryproduct + sto_an_zero_prefixentryproduct * sto_bn_zero_prefixentryproduct) + sto_cn_zero_prefixentryproduct = (sto_ap_zero_prefixentryproduct * sto_bn_zero_prefixentryproduct + sto_an_zero_prefixentryproduct * sto_bp_zero_prefixentryproduct) + sto_cp_zero_prefixentryproduct))))))))))))))) \/ ((((dc_index_zero_prefix)=0 \/ ~(exists pvs_factor_zero_prefixentrynondivisor. (n) = (dc_index_zero_prefix) * pvs_factor_zero_prefixentrynondivisor)) /\ ((dc_value_zero_prefix)=0))))))) -> (exists dst_positive_code_zero_fold dst_positive_scale_zero_fold dst_negative_code_zero_fold dst_negative_scale_zero_fold dst_positive_sum_zero_fold dst_negative_sum_zero_fold. (((M) = (((((dst_positive_code_zero_fold) + (dst_positive_scale_zero_fold)) * S ((dst_positive_code_zero_fold) + (dst_positive_scale_zero_fold)) + ((dst_positive_scale_zero_fold) + (dst_positive_scale_zero_fold))) + (((dst_negative_code_zero_fold) + (dst_negative_scale_zero_fold)) * S ((dst_negative_code_zero_fold) + (dst_negative_scale_zero_fold)) + ((dst_negative_scale_zero_fold) + (dst_negative_scale_zero_fold)))) * S ((((dst_positive_code_zero_fold) + (dst_positive_scale_zero_fold)) * S ((dst_positive_code_zero_fold) + (dst_positive_scale_zero_fold)) + ((dst_positive_scale_zero_fold) + (dst_positive_scale_zero_fold))) + (((dst_negative_code_zero_fold) + (dst_negative_scale_zero_fold)) * S ((dst_negative_code_zero_fold) + (dst_negative_scale_zero_fold)) + ((dst_negative_scale_zero_fold) + (dst_negative_scale_zero_fold)))) + ((((dst_negative_code_zero_fold) + (dst_negative_scale_zero_fold)) * S ((dst_negative_code_zero_fold) + (dst_negative_scale_zero_fold)) + ((dst_negative_scale_zero_fold) + (dst_negative_scale_zero_fold))) + (((dst_negative_code_zero_fold) + (dst_negative_scale_zero_fold)) * S ((dst_negative_code_zero_fold) + (dst_negative_scale_zero_fold)) + ((dst_negative_scale_zero_fold) + (dst_negative_scale_zero_fold)))))) /\ (((exists fs_u_dst_zero_foldpositive fs_v_dst_zero_foldpositive. ((((exists fs_h_dst_zero_foldpositive_body_start. fs_h_dst_zero_foldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_zero_foldpositive)) /\ exists fs_q_dst_zero_foldpositive_body_start. fs_u_dst_zero_foldpositive = fs_q_dst_zero_foldpositive_body_start * S ((S (0)) * fs_v_dst_zero_foldpositive) + (0))) /\ ((((exists fs_h_dst_zero_foldpositive_body_terminal. fs_h_dst_zero_foldpositive_body_terminal + S (dst_positive_sum_zero_fold) = S ((S (1)) * fs_v_dst_zero_foldpositive)) /\ exists fs_q_dst_zero_foldpositive_body_terminal. fs_u_dst_zero_foldpositive = fs_q_dst_zero_foldpositive_body_terminal * S ((S (1)) * fs_v_dst_zero_foldpositive) + (dst_positive_sum_zero_fold))) /\ forall fs_i_dst_zero_foldpositive_body_steps. (exists fs_lt_dst_zero_foldpositive_body_steps_bound. fs_lt_dst_zero_foldpositive_body_steps_bound + S fs_i_dst_zero_foldpositive_body_steps = 1) -> exists fs_a_dst_zero_foldpositive_body_steps fs_r_dst_zero_foldpositive_body_steps fs_s_dst_zero_foldpositive_body_steps. ((((exists fs_h_dst_zero_foldpositive_body_steps_summand. fs_h_dst_zero_foldpositive_body_steps_summand + S (fs_a_dst_zero_foldpositive_body_steps) = S ((S (fs_i_dst_zero_foldpositive_body_steps)) * dst_positive_scale_zero_fold)) /\ exists fs_q_dst_zero_foldpositive_body_steps_summand. dst_positive_code_zero_fold = fs_q_dst_zero_foldpositive_body_steps_summand * S ((S (fs_i_dst_zero_foldpositive_body_steps)) * dst_positive_scale_zero_fold) + (fs_a_dst_zero_foldpositive_body_steps))) /\ ((((exists fs_h_dst_zero_foldpositive_body_steps_partial. fs_h_dst_zero_foldpositive_body_steps_partial + S (fs_r_dst_zero_foldpositive_body_steps) = S ((S (fs_i_dst_zero_foldpositive_body_steps)) * fs_v_dst_zero_foldpositive)) /\ exists fs_q_dst_zero_foldpositive_body_steps_partial. fs_u_dst_zero_foldpositive = fs_q_dst_zero_foldpositive_body_steps_partial * S ((S (fs_i_dst_zero_foldpositive_body_steps)) * fs_v_dst_zero_foldpositive) + (fs_r_dst_zero_foldpositive_body_steps))) /\ ((((exists fs_h_dst_zero_foldpositive_body_steps_successor. fs_h_dst_zero_foldpositive_body_steps_successor + S (fs_s_dst_zero_foldpositive_body_steps) = S ((S (S fs_i_dst_zero_foldpositive_body_steps)) * fs_v_dst_zero_foldpositive)) /\ exists fs_q_dst_zero_foldpositive_body_steps_successor. fs_u_dst_zero_foldpositive = fs_q_dst_zero_foldpositive_body_steps_successor * S ((S (S fs_i_dst_zero_foldpositive_body_steps)) * fs_v_dst_zero_foldpositive) + (fs_s_dst_zero_foldpositive_body_steps))) /\ fs_s_dst_zero_foldpositive_body_steps = fs_r_dst_zero_foldpositive_body_steps + fs_a_dst_zero_foldpositive_body_steps)))))) /\ (((exists fs_u_dst_zero_foldnegative fs_v_dst_zero_foldnegative. ((((exists fs_h_dst_zero_foldnegative_body_start. fs_h_dst_zero_foldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_zero_foldnegative)) /\ exists fs_q_dst_zero_foldnegative_body_start. fs_u_dst_zero_foldnegative = fs_q_dst_zero_foldnegative_body_start * S ((S (0)) * fs_v_dst_zero_foldnegative) + (0))) /\ ((((exists fs_h_dst_zero_foldnegative_body_terminal. fs_h_dst_zero_foldnegative_body_terminal + S (dst_negative_sum_zero_fold) = S ((S (1)) * fs_v_dst_zero_foldnegative)) /\ exists fs_q_dst_zero_foldnegative_body_terminal. fs_u_dst_zero_foldnegative = fs_q_dst_zero_foldnegative_body_terminal * S ((S (1)) * fs_v_dst_zero_foldnegative) + (dst_negative_sum_zero_fold))) /\ forall fs_i_dst_zero_foldnegative_body_steps. (exists fs_lt_dst_zero_foldnegative_body_steps_bound. fs_lt_dst_zero_foldnegative_body_steps_bound + S fs_i_dst_zero_foldnegative_body_steps = 1) -> exists fs_a_dst_zero_foldnegative_body_steps fs_r_dst_zero_foldnegative_body_steps fs_s_dst_zero_foldnegative_body_steps. ((((exists fs_h_dst_zero_foldnegative_body_steps_summand. fs_h_dst_zero_foldnegative_body_steps_summand + S (fs_a_dst_zero_foldnegative_body_steps) = S ((S (fs_i_dst_zero_foldnegative_body_steps)) * dst_negative_scale_zero_fold)) /\ exists fs_q_dst_zero_foldnegative_body_steps_summand. dst_negative_code_zero_fold = fs_q_dst_zero_foldnegative_body_steps_summand * S ((S (fs_i_dst_zero_foldnegative_body_steps)) * dst_negative_scale_zero_fold) + (fs_a_dst_zero_foldnegative_body_steps))) /\ ((((exists fs_h_dst_zero_foldnegative_body_steps_partial. fs_h_dst_zero_foldnegative_body_steps_partial + S (fs_r_dst_zero_foldnegative_body_steps) = S ((S (fs_i_dst_zero_foldnegative_body_steps)) * fs_v_dst_zero_foldnegative)) /\ exists fs_q_dst_zero_foldnegative_body_steps_partial. fs_u_dst_zero_foldnegative = fs_q_dst_zero_foldnegative_body_steps_partial * S ((S (fs_i_dst_zero_foldnegative_body_steps)) * fs_v_dst_zero_foldnegative) + (fs_r_dst_zero_foldnegative_body_steps))) /\ ((((exists fs_h_dst_zero_foldnegative_body_steps_successor. fs_h_dst_zero_foldnegative_body_steps_successor + S (fs_s_dst_zero_foldnegative_body_steps) = S ((S (S fs_i_dst_zero_foldnegative_body_steps)) * fs_v_dst_zero_foldnegative)) /\ exists fs_q_dst_zero_foldnegative_body_steps_successor. fs_u_dst_zero_foldnegative = fs_q_dst_zero_foldnegative_body_steps_successor * S ((S (S fs_i_dst_zero_foldnegative_body_steps)) * fs_v_dst_zero_foldnegative) + (fs_s_dst_zero_foldnegative_body_steps))) /\ fs_s_dst_zero_foldnegative_body_steps = fs_r_dst_zero_foldnegative_body_steps + fs_a_dst_zero_foldnegative_body_steps)))))) /\ (exists ge_balance_positive_zero_foldresult ge_balance_negative_zero_foldresult. (((((0) = 2 * (ge_balance_positive_zero_foldresult) /\ (ge_balance_negative_zero_foldresult) = 0) \/ exists ge_signed_half_zero_foldresultdecode. (((0) = 2 * ge_signed_half_zero_foldresultdecode + 1 /\ (ge_balance_positive_zero_foldresult) = 0) /\ (ge_balance_negative_zero_foldresult) = S ge_signed_half_zero_foldresultdecode))) /\ ((dst_positive_sum_zero_fold) + ge_balance_negative_zero_foldresult = (dst_negative_sum_zero_fold) + ge_balance_positive_zero_foldresult)))))))))

Complete tactic proof in conservative notation

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

40 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.

01Fix variables and assumptionsL1–5

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

  1. L1
    intro F
  2. L2
    intro G
  3. L3
    intro n
  4. L4
    intro M
  5. L5
    intro hm
02Separate the logical casesL6–6

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

  1. L6
    cases hm
03Use earlier factsL7–10

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

  1. L7
    specialize signed_prefix_sum_zero_exists (M)
  2. L8
    specialize signed_prefix_sum_zero_exists (1)
  3. L9
    apply signed_prefix_sum_zero_exists
  4. L10
    exact hm_left
04Fix variables and assumptionsL11–15

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

  1. L11
    intro i
  2. L12
    intro z
  3. L13
    intro hlo
  4. L14
    intro hi
  5. L15
    intro hz
05Establish hi0L16–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le zero.

  1. L16
    have hi0 : i=0
  2. L17
    specialize le_zero (i)
  3. L18
    apply le_zero
  4. L19
    specialize le_of_succ_le_succ (i)
  5. L20
    specialize le_of_succ_le_succ (0)
  6. L21
    apply le_of_succ_le_succ
  7. L22
    exact hi
  8. L23
    rewrite hi0 at hz
  9. L24
    rewrite hi0 at hz
  10. L25
    rewrite hi0 at hz
06Calculate and transport equalitiesL26–26

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

  1. L26
    rewrite hi0 at hz
07Use earlier factsL27–32

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

  1. L27
    specialize dirichlet_convolution_entry_omitted_value (F)
  2. L28
    specialize dirichlet_convolution_entry_omitted_value (G)
  3. L29
    specialize dirichlet_convolution_entry_omitted_value (n)
  4. L30
    specialize dirichlet_convolution_entry_omitted_value (0)
  5. L31
    specialize dirichlet_convolution_entry_omitted_value (z)
  6. L32
    apply dirichlet_convolution_entry_omitted_value
08Separate the logical casesL33–33

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

  1. L33
    left
09Calculate and transport equalitiesL34–34

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

  1. L34
    refl
10Use earlier factsL35–40

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

  1. L35
    specialize hm_right (0)
  2. L36
    specialize hm_right (z)
  3. L37
    apply hm_right
  4. L38
    specialize le_refl (0)
  5. L39
    apply le_refl
  6. L40
    exact hz

Library-wide reading audit

Original defined command ledger · 40 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro n
  4. 0004intro M
  5. 0005intro hm
  6. 0006cases hm
  7. 0007specialize signed_prefix_sum_zero_exists (M)
  8. 0008specialize signed_prefix_sum_zero_exists (1)
  9. 0009apply signed_prefix_sum_zero_exists
  10. 0010exact hm_left
  11. 0011intro i
  12. 0012intro z
  13. 0013intro hlo
  14. 0014intro hi
  15. 0015intro hz
  16. 0016have hi0 : i=0
  17. 0017specialize le_zero (i)
  18. 0018apply le_zero
  19. 0019specialize le_of_succ_le_succ (i)
  20. 0020specialize le_of_succ_le_succ (0)
  21. 0021apply le_of_succ_le_succ
  22. 0022exact hi
  23. 0023rewrite hi0 at hz
  24. 0024rewrite hi0 at hz
  25. 0025rewrite hi0 at hz
  26. 0026rewrite hi0 at hz
  27. 0027specialize dirichlet_convolution_entry_omitted_value (F)
  28. 0028specialize dirichlet_convolution_entry_omitted_value (G)
  29. 0029specialize dirichlet_convolution_entry_omitted_value (n)
  30. 0030specialize dirichlet_convolution_entry_omitted_value (0)
  31. 0031specialize dirichlet_convolution_entry_omitted_value (z)
  32. 0032apply dirichlet_convolution_entry_omitted_value
  33. 0033left
  34. 0034refl
  35. 0035specialize hm_right (0)
  36. 0036specialize hm_right (z)
  37. 0037apply hm_right
  38. 0038specialize le_refl (0)
  39. 0039apply le_refl
  40. 0040exact hz