DC0026 — dirichlet_convolution_prefix_zero_tail

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

Exact expanded first-order arithmetic statement

forall F G n L M. ~(n=0) -> (((exists dst_positive_code_prefix_tail_sourcetable dst_positive_scale_prefix_tail_sourcetable dst_negative_code_prefix_tail_sourcetable dst_negative_scale_prefix_tail_sourcetable. (((M) = (((((dst_positive_code_prefix_tail_sourcetable) + (dst_positive_scale_prefix_tail_sourcetable)) * S ((dst_positive_code_prefix_tail_sourcetable) + (dst_positive_scale_prefix_tail_sourcetable)) + ((dst_positive_scale_prefix_tail_sourcetable) + (dst_positive_scale_prefix_tail_sourcetable))) + (((dst_negative_code_prefix_tail_sourcetable) + (dst_negative_scale_prefix_tail_sourcetable)) * S ((dst_negative_code_prefix_tail_sourcetable) + (dst_negative_scale_prefix_tail_sourcetable)) + ((dst_negative_scale_prefix_tail_sourcetable) + (dst_negative_scale_prefix_tail_sourcetable)))) * S ((((dst_positive_code_prefix_tail_sourcetable) + (dst_positive_scale_prefix_tail_sourcetable)) * S ((dst_positive_code_prefix_tail_sourcetable) + (dst_positive_scale_prefix_tail_sourcetable)) + ((dst_positive_scale_prefix_tail_sourcetable) + (dst_positive_scale_prefix_tail_sourcetable))) + (((dst_negative_code_prefix_tail_sourcetable) + (dst_negative_scale_prefix_tail_sourcetable)) * S ((dst_negative_code_prefix_tail_sourcetable) + (dst_negative_scale_prefix_tail_sourcetable)) + ((dst_negative_scale_prefix_tail_sourcetable) + (dst_negative_scale_prefix_tail_sourcetable)))) + ((((dst_negative_code_prefix_tail_sourcetable) + (dst_negative_scale_prefix_tail_sourcetable)) * S ((dst_negative_code_prefix_tail_sourcetable) + (dst_negative_scale_prefix_tail_sourcetable)) + ((dst_negative_scale_prefix_tail_sourcetable) + (dst_negative_scale_prefix_tail_sourcetable))) + (((dst_negative_code_prefix_tail_sourcetable) + (dst_negative_scale_prefix_tail_sourcetable)) * S ((dst_negative_code_prefix_tail_sourcetable) + (dst_negative_scale_prefix_tail_sourcetable)) + ((dst_negative_scale_prefix_tail_sourcetable) + (dst_negative_scale_prefix_tail_sourcetable)))))) /\ (forall dst_index_prefix_tail_sourcetable. (exists pvs_le_gap_prefix_tail_sourcetabledomain. pvs_le_gap_prefix_tail_sourcetabledomain + (dst_index_prefix_tail_sourcetable) = (L)) -> exists dst_positive_prefix_tail_sourcetable dst_negative_prefix_tail_sourcetable dst_value_prefix_tail_sourcetable. ((((exists ff_h_pvs_prefix_tail_sourcetableentrypositive. ff_h_pvs_prefix_tail_sourcetableentrypositive + S (dst_positive_prefix_tail_sourcetable) = S ((S (dst_index_prefix_tail_sourcetable)) * dst_positive_scale_prefix_tail_sourcetable)) /\ exists ff_q_pvs_prefix_tail_sourcetableentrypositive. dst_positive_code_prefix_tail_sourcetable = ff_q_pvs_prefix_tail_sourcetableentrypositive * S ((S (dst_index_prefix_tail_sourcetable)) * dst_positive_scale_prefix_tail_sourcetable) + (dst_positive_prefix_tail_sourcetable))) /\ (((((exists ff_h_pvs_prefix_tail_sourcetableentrynegative. ff_h_pvs_prefix_tail_sourcetableentrynegative + S (dst_negative_prefix_tail_sourcetable) = S ((S (dst_index_prefix_tail_sourcetable)) * dst_negative_scale_prefix_tail_sourcetable)) /\ exists ff_q_pvs_prefix_tail_sourcetableentrynegative. dst_negative_code_prefix_tail_sourcetable = ff_q_pvs_prefix_tail_sourcetableentrynegative * S ((S (dst_index_prefix_tail_sourcetable)) * dst_negative_scale_prefix_tail_sourcetable) + (dst_negative_prefix_tail_sourcetable))) /\ (exists ge_balance_positive_prefix_tail_sourcetableentryvalue ge_balance_negative_prefix_tail_sourcetableentryvalue. (((((dst_value_prefix_tail_sourcetable) = 2 * (ge_balance_positive_prefix_tail_sourcetableentryvalue) /\ (ge_balance_negative_prefix_tail_sourcetableentryvalue) = 0) \/ exists ge_signed_half_prefix_tail_sourcetableentryvaluedecode. (((dst_value_prefix_tail_sourcetable) = 2 * ge_signed_half_prefix_tail_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_prefix_tail_sourcetableentryvalue) = 0) /\ (ge_balance_negative_prefix_tail_sourcetableentryvalue) = S ge_signed_half_prefix_tail_sourcetableentryvaluedecode))) /\ ((dst_positive_prefix_tail_sourcetable) + ge_balance_negative_prefix_tail_sourcetableentryvalue = (dst_negative_prefix_tail_sourcetable) + ge_balance_positive_prefix_tail_sourcetableentryvalue))))))))) /\ (forall dc_index_prefix_tail_source dc_value_prefix_tail_source. (exists pvs_le_gap_prefix_tail_sourcedomain. pvs_le_gap_prefix_tail_sourcedomain + (dc_index_prefix_tail_source) = (L)) -> (exists dst_positive_code_prefix_tail_sourcelookup dst_positive_scale_prefix_tail_sourcelookup dst_negative_code_prefix_tail_sourcelookup dst_negative_scale_prefix_tail_sourcelookup dst_positive_prefix_tail_sourcelookup dst_negative_prefix_tail_sourcelookup. (((M) = (((((dst_positive_code_prefix_tail_sourcelookup) + (dst_positive_scale_prefix_tail_sourcelookup)) * S ((dst_positive_code_prefix_tail_sourcelookup) + (dst_positive_scale_prefix_tail_sourcelookup)) + ((dst_positive_scale_prefix_tail_sourcelookup) + (dst_positive_scale_prefix_tail_sourcelookup))) + (((dst_negative_code_prefix_tail_sourcelookup) + (dst_negative_scale_prefix_tail_sourcelookup)) * S ((dst_negative_code_prefix_tail_sourcelookup) + (dst_negative_scale_prefix_tail_sourcelookup)) + ((dst_negative_scale_prefix_tail_sourcelookup) + (dst_negative_scale_prefix_tail_sourcelookup)))) * S ((((dst_positive_code_prefix_tail_sourcelookup) + (dst_positive_scale_prefix_tail_sourcelookup)) * S ((dst_positive_code_prefix_tail_sourcelookup) + (dst_positive_scale_prefix_tail_sourcelookup)) + ((dst_positive_scale_prefix_tail_sourcelookup) + (dst_positive_scale_prefix_tail_sourcelookup))) + (((dst_negative_code_prefix_tail_sourcelookup) + (dst_negative_scale_prefix_tail_sourcelookup)) * S ((dst_negative_code_prefix_tail_sourcelookup) + (dst_negative_scale_prefix_tail_sourcelookup)) + ((dst_negative_scale_prefix_tail_sourcelookup) + (dst_negative_scale_prefix_tail_sourcelookup)))) + ((((dst_negative_code_prefix_tail_sourcelookup) + (dst_negative_scale_prefix_tail_sourcelookup)) * S ((dst_negative_code_prefix_tail_sourcelookup) + (dst_negative_scale_prefix_tail_sourcelookup)) + ((dst_negative_scale_prefix_tail_sourcelookup) + (dst_negative_scale_prefix_tail_sourcelookup))) + (((dst_negative_code_prefix_tail_sourcelookup) + (dst_negative_scale_prefix_tail_sourcelookup)) * S ((dst_negative_code_prefix_tail_sourcelookup) + (dst_negative_scale_prefix_tail_sourcelookup)) + ((dst_negative_scale_prefix_tail_sourcelookup) + (dst_negative_scale_prefix_tail_sourcelookup)))))) /\ (((((exists ff_h_pvs_prefix_tail_sourcelookuppositive. ff_h_pvs_prefix_tail_sourcelookuppositive + S (dst_positive_prefix_tail_sourcelookup) = S ((S (dc_index_prefix_tail_source)) * dst_positive_scale_prefix_tail_sourcelookup)) /\ exists ff_q_pvs_prefix_tail_sourcelookuppositive. dst_positive_code_prefix_tail_sourcelookup = ff_q_pvs_prefix_tail_sourcelookuppositive * S ((S (dc_index_prefix_tail_source)) * dst_positive_scale_prefix_tail_sourcelookup) + (dst_positive_prefix_tail_sourcelookup))) /\ (((((exists ff_h_pvs_prefix_tail_sourcelookupnegative. ff_h_pvs_prefix_tail_sourcelookupnegative + S (dst_negative_prefix_tail_sourcelookup) = S ((S (dc_index_prefix_tail_source)) * dst_negative_scale_prefix_tail_sourcelookup)) /\ exists ff_q_pvs_prefix_tail_sourcelookupnegative. dst_negative_code_prefix_tail_sourcelookup = ff_q_pvs_prefix_tail_sourcelookupnegative * S ((S (dc_index_prefix_tail_source)) * dst_negative_scale_prefix_tail_sourcelookup) + (dst_negative_prefix_tail_sourcelookup))) /\ (exists ge_balance_positive_prefix_tail_sourcelookupvalue ge_balance_negative_prefix_tail_sourcelookupvalue. (((((dc_value_prefix_tail_source) = 2 * (ge_balance_positive_prefix_tail_sourcelookupvalue) /\ (ge_balance_negative_prefix_tail_sourcelookupvalue) = 0) \/ exists ge_signed_half_prefix_tail_sourcelookupvaluedecode. (((dc_value_prefix_tail_source) = 2 * ge_signed_half_prefix_tail_sourcelookupvaluedecode + 1 /\ (ge_balance_positive_prefix_tail_sourcelookupvalue) = 0) /\ (ge_balance_negative_prefix_tail_sourcelookupvalue) = S ge_signed_half_prefix_tail_sourcelookupvaluedecode))) /\ ((dst_positive_prefix_tail_sourcelookup) + ge_balance_negative_prefix_tail_sourcelookupvalue = (dst_negative_prefix_tail_sourcelookup) + ge_balance_positive_prefix_tail_sourcelookupvalue))))))))) -> ((((~((dc_index_prefix_tail_source)=0)) /\ (exists dc_quotient_prefix_tail_sourceentry dc_left_prefix_tail_sourceentry dc_right_prefix_tail_sourceentry. (((n)=(dc_index_prefix_tail_source)*dc_quotient_prefix_tail_sourceentry) /\ (((exists dst_positive_code_prefix_tail_sourceentryleft dst_positive_scale_prefix_tail_sourceentryleft dst_negative_code_prefix_tail_sourceentryleft dst_negative_scale_prefix_tail_sourceentryleft dst_positive_prefix_tail_sourceentryleft dst_negative_prefix_tail_sourceentryleft. (((F) = (((((dst_positive_code_prefix_tail_sourceentryleft) + (dst_positive_scale_prefix_tail_sourceentryleft)) * S ((dst_positive_code_prefix_tail_sourceentryleft) + (dst_positive_scale_prefix_tail_sourceentryleft)) + ((dst_positive_scale_prefix_tail_sourceentryleft) + (dst_positive_scale_prefix_tail_sourceentryleft))) + (((dst_negative_code_prefix_tail_sourceentryleft) + (dst_negative_scale_prefix_tail_sourceentryleft)) * S ((dst_negative_code_prefix_tail_sourceentryleft) + (dst_negative_scale_prefix_tail_sourceentryleft)) + ((dst_negative_scale_prefix_tail_sourceentryleft) + (dst_negative_scale_prefix_tail_sourceentryleft)))) * S ((((dst_positive_code_prefix_tail_sourceentryleft) + (dst_positive_scale_prefix_tail_sourceentryleft)) * S ((dst_positive_code_prefix_tail_sourceentryleft) + (dst_positive_scale_prefix_tail_sourceentryleft)) + ((dst_positive_scale_prefix_tail_sourceentryleft) + (dst_positive_scale_prefix_tail_sourceentryleft))) + (((dst_negative_code_prefix_tail_sourceentryleft) + (dst_negative_scale_prefix_tail_sourceentryleft)) * S ((dst_negative_code_prefix_tail_sourceentryleft) + (dst_negative_scale_prefix_tail_sourceentryleft)) + ((dst_negative_scale_prefix_tail_sourceentryleft) + (dst_negative_scale_prefix_tail_sourceentryleft)))) + ((((dst_negative_code_prefix_tail_sourceentryleft) + (dst_negative_scale_prefix_tail_sourceentryleft)) * S ((dst_negative_code_prefix_tail_sourceentryleft) + (dst_negative_scale_prefix_tail_sourceentryleft)) + ((dst_negative_scale_prefix_tail_sourceentryleft) + (dst_negative_scale_prefix_tail_sourceentryleft))) + (((dst_negative_code_prefix_tail_sourceentryleft) + (dst_negative_scale_prefix_tail_sourceentryleft)) * S ((dst_negative_code_prefix_tail_sourceentryleft) + (dst_negative_scale_prefix_tail_sourceentryleft)) + ((dst_negative_scale_prefix_tail_sourceentryleft) + (dst_negative_scale_prefix_tail_sourceentryleft)))))) /\ (((((exists ff_h_pvs_prefix_tail_sourceentryleftpositive. ff_h_pvs_prefix_tail_sourceentryleftpositive + S (dst_positive_prefix_tail_sourceentryleft) = S ((S (dc_index_prefix_tail_source)) * dst_positive_scale_prefix_tail_sourceentryleft)) /\ exists ff_q_pvs_prefix_tail_sourceentryleftpositive. dst_positive_code_prefix_tail_sourceentryleft = ff_q_pvs_prefix_tail_sourceentryleftpositive * S ((S (dc_index_prefix_tail_source)) * dst_positive_scale_prefix_tail_sourceentryleft) + (dst_positive_prefix_tail_sourceentryleft))) /\ (((((exists ff_h_pvs_prefix_tail_sourceentryleftnegative. ff_h_pvs_prefix_tail_sourceentryleftnegative + S (dst_negative_prefix_tail_sourceentryleft) = S ((S (dc_index_prefix_tail_source)) * dst_negative_scale_prefix_tail_sourceentryleft)) /\ exists ff_q_pvs_prefix_tail_sourceentryleftnegative. dst_negative_code_prefix_tail_sourceentryleft = ff_q_pvs_prefix_tail_sourceentryleftnegative * S ((S (dc_index_prefix_tail_source)) * dst_negative_scale_prefix_tail_sourceentryleft) + (dst_negative_prefix_tail_sourceentryleft))) /\ (exists ge_balance_positive_prefix_tail_sourceentryleftvalue ge_balance_negative_prefix_tail_sourceentryleftvalue. (((((dc_left_prefix_tail_sourceentry) = 2 * (ge_balance_positive_prefix_tail_sourceentryleftvalue) /\ (ge_balance_negative_prefix_tail_sourceentryleftvalue) = 0) \/ exists ge_signed_half_prefix_tail_sourceentryleftvaluedecode. (((dc_left_prefix_tail_sourceentry) = 2 * ge_signed_half_prefix_tail_sourceentryleftvaluedecode + 1 /\ (ge_balance_positive_prefix_tail_sourceentryleftvalue) = 0) /\ (ge_balance_negative_prefix_tail_sourceentryleftvalue) = S ge_signed_half_prefix_tail_sourceentryleftvaluedecode))) /\ ((dst_positive_prefix_tail_sourceentryleft) + ge_balance_negative_prefix_tail_sourceentryleftvalue = (dst_negative_prefix_tail_sourceentryleft) + ge_balance_positive_prefix_tail_sourceentryleftvalue))))))))) /\ (((exists dst_positive_code_prefix_tail_sourceentryright dst_positive_scale_prefix_tail_sourceentryright dst_negative_code_prefix_tail_sourceentryright dst_negative_scale_prefix_tail_sourceentryright dst_positive_prefix_tail_sourceentryright dst_negative_prefix_tail_sourceentryright. (((G) = (((((dst_positive_code_prefix_tail_sourceentryright) + (dst_positive_scale_prefix_tail_sourceentryright)) * S ((dst_positive_code_prefix_tail_sourceentryright) + (dst_positive_scale_prefix_tail_sourceentryright)) + ((dst_positive_scale_prefix_tail_sourceentryright) + (dst_positive_scale_prefix_tail_sourceentryright))) + (((dst_negative_code_prefix_tail_sourceentryright) + (dst_negative_scale_prefix_tail_sourceentryright)) * S ((dst_negative_code_prefix_tail_sourceentryright) + (dst_negative_scale_prefix_tail_sourceentryright)) + ((dst_negative_scale_prefix_tail_sourceentryright) + (dst_negative_scale_prefix_tail_sourceentryright)))) * S ((((dst_positive_code_prefix_tail_sourceentryright) + (dst_positive_scale_prefix_tail_sourceentryright)) * S ((dst_positive_code_prefix_tail_sourceentryright) + (dst_positive_scale_prefix_tail_sourceentryright)) + ((dst_positive_scale_prefix_tail_sourceentryright) + (dst_positive_scale_prefix_tail_sourceentryright))) + (((dst_negative_code_prefix_tail_sourceentryright) + (dst_negative_scale_prefix_tail_sourceentryright)) * S ((dst_negative_code_prefix_tail_sourceentryright) + (dst_negative_scale_prefix_tail_sourceentryright)) + ((dst_negative_scale_prefix_tail_sourceentryright) + (dst_negative_scale_prefix_tail_sourceentryright)))) + ((((dst_negative_code_prefix_tail_sourceentryright) + (dst_negative_scale_prefix_tail_sourceentryright)) * S ((dst_negative_code_prefix_tail_sourceentryright) + (dst_negative_scale_prefix_tail_sourceentryright)) + ((dst_negative_scale_prefix_tail_sourceentryright) + (dst_negative_scale_prefix_tail_sourceentryright))) + (((dst_negative_code_prefix_tail_sourceentryright) + (dst_negative_scale_prefix_tail_sourceentryright)) * S ((dst_negative_code_prefix_tail_sourceentryright) + (dst_negative_scale_prefix_tail_sourceentryright)) + ((dst_negative_scale_prefix_tail_sourceentryright) + (dst_negative_scale_prefix_tail_sourceentryright)))))) /\ (((((exists ff_h_pvs_prefix_tail_sourceentryrightpositive. ff_h_pvs_prefix_tail_sourceentryrightpositive + S (dst_positive_prefix_tail_sourceentryright) = S ((S (dc_quotient_prefix_tail_sourceentry)) * dst_positive_scale_prefix_tail_sourceentryright)) /\ exists ff_q_pvs_prefix_tail_sourceentryrightpositive. dst_positive_code_prefix_tail_sourceentryright = ff_q_pvs_prefix_tail_sourceentryrightpositive * S ((S (dc_quotient_prefix_tail_sourceentry)) * dst_positive_scale_prefix_tail_sourceentryright) + (dst_positive_prefix_tail_sourceentryright))) /\ (((((exists ff_h_pvs_prefix_tail_sourceentryrightnegative. ff_h_pvs_prefix_tail_sourceentryrightnegative + S (dst_negative_prefix_tail_sourceentryright) = S ((S (dc_quotient_prefix_tail_sourceentry)) * dst_negative_scale_prefix_tail_sourceentryright)) /\ exists ff_q_pvs_prefix_tail_sourceentryrightnegative. dst_negative_code_prefix_tail_sourceentryright = ff_q_pvs_prefix_tail_sourceentryrightnegative * S ((S (dc_quotient_prefix_tail_sourceentry)) * dst_negative_scale_prefix_tail_sourceentryright) + (dst_negative_prefix_tail_sourceentryright))) /\ (exists ge_balance_positive_prefix_tail_sourceentryrightvalue ge_balance_negative_prefix_tail_sourceentryrightvalue. (((((dc_right_prefix_tail_sourceentry) = 2 * (ge_balance_positive_prefix_tail_sourceentryrightvalue) /\ (ge_balance_negative_prefix_tail_sourceentryrightvalue) = 0) \/ exists ge_signed_half_prefix_tail_sourceentryrightvaluedecode. (((dc_right_prefix_tail_sourceentry) = 2 * ge_signed_half_prefix_tail_sourceentryrightvaluedecode + 1 /\ (ge_balance_positive_prefix_tail_sourceentryrightvalue) = 0) /\ (ge_balance_negative_prefix_tail_sourceentryrightvalue) = S ge_signed_half_prefix_tail_sourceentryrightvaluedecode))) /\ ((dst_positive_prefix_tail_sourceentryright) + ge_balance_negative_prefix_tail_sourceentryrightvalue = (dst_negative_prefix_tail_sourceentryright) + ge_balance_positive_prefix_tail_sourceentryrightvalue))))))))) /\ (exists sto_ap_prefix_tail_sourceentryproduct sto_an_prefix_tail_sourceentryproduct sto_bp_prefix_tail_sourceentryproduct sto_bn_prefix_tail_sourceentryproduct sto_cp_prefix_tail_sourceentryproduct sto_cn_prefix_tail_sourceentryproduct. (((((dc_left_prefix_tail_sourceentry) = 2 * (sto_ap_prefix_tail_sourceentryproduct) /\ (sto_an_prefix_tail_sourceentryproduct) = 0) \/ exists ge_signed_half_prefix_tail_sourceentryproductleft. (((dc_left_prefix_tail_sourceentry) = 2 * ge_signed_half_prefix_tail_sourceentryproductleft + 1 /\ (sto_ap_prefix_tail_sourceentryproduct) = 0) /\ (sto_an_prefix_tail_sourceentryproduct) = S ge_signed_half_prefix_tail_sourceentryproductleft))) /\ ((((((dc_right_prefix_tail_sourceentry) = 2 * (sto_bp_prefix_tail_sourceentryproduct) /\ (sto_bn_prefix_tail_sourceentryproduct) = 0) \/ exists ge_signed_half_prefix_tail_sourceentryproductright. (((dc_right_prefix_tail_sourceentry) = 2 * ge_signed_half_prefix_tail_sourceentryproductright + 1 /\ (sto_bp_prefix_tail_sourceentryproduct) = 0) /\ (sto_bn_prefix_tail_sourceentryproduct) = S ge_signed_half_prefix_tail_sourceentryproductright))) /\ ((((((dc_value_prefix_tail_source) = 2 * (sto_cp_prefix_tail_sourceentryproduct) /\ (sto_cn_prefix_tail_sourceentryproduct) = 0) \/ exists ge_signed_half_prefix_tail_sourceentryproductoutput. (((dc_value_prefix_tail_source) = 2 * ge_signed_half_prefix_tail_sourceentryproductoutput + 1 /\ (sto_cp_prefix_tail_sourceentryproduct) = 0) /\ (sto_cn_prefix_tail_sourceentryproduct) = S ge_signed_half_prefix_tail_sourceentryproductoutput))) /\ ((sto_ap_prefix_tail_sourceentryproduct * sto_bp_prefix_tail_sourceentryproduct + sto_an_prefix_tail_sourceentryproduct * sto_bn_prefix_tail_sourceentryproduct) + sto_cn_prefix_tail_sourceentryproduct = (sto_ap_prefix_tail_sourceentryproduct * sto_bn_prefix_tail_sourceentryproduct + sto_an_prefix_tail_sourceentryproduct * sto_bp_prefix_tail_sourceentryproduct) + sto_cp_prefix_tail_sourceentryproduct))))))))))))))) \/ ((((dc_index_prefix_tail_source)=0 \/ ~(exists pvs_factor_prefix_tail_sourceentrynondivisor. (n) = (dc_index_prefix_tail_source) * pvs_factor_prefix_tail_sourceentrynondivisor)) /\ ((dc_value_prefix_tail_source)=0))))))) -> (forall sfs_index_prefix_tail_result sfs_value_prefix_tail_result. (exists pvs_le_gap_prefix_tail_resultlower. pvs_le_gap_prefix_tail_resultlower + (S n) = (sfs_index_prefix_tail_result)) -> (exists pvs_gap_prefix_tail_resultupper. pvs_gap_prefix_tail_resultupper + S (sfs_index_prefix_tail_result) = (S L)) -> (exists dst_positive_code_prefix_tail_resultentry dst_positive_scale_prefix_tail_resultentry dst_negative_code_prefix_tail_resultentry dst_negative_scale_prefix_tail_resultentry dst_positive_prefix_tail_resultentry dst_negative_prefix_tail_resultentry. (((M) = (((((dst_positive_code_prefix_tail_resultentry) + (dst_positive_scale_prefix_tail_resultentry)) * S ((dst_positive_code_prefix_tail_resultentry) + (dst_positive_scale_prefix_tail_resultentry)) + ((dst_positive_scale_prefix_tail_resultentry) + (dst_positive_scale_prefix_tail_resultentry))) + (((dst_negative_code_prefix_tail_resultentry) + (dst_negative_scale_prefix_tail_resultentry)) * S ((dst_negative_code_prefix_tail_resultentry) + (dst_negative_scale_prefix_tail_resultentry)) + ((dst_negative_scale_prefix_tail_resultentry) + (dst_negative_scale_prefix_tail_resultentry)))) * S ((((dst_positive_code_prefix_tail_resultentry) + (dst_positive_scale_prefix_tail_resultentry)) * S ((dst_positive_code_prefix_tail_resultentry) + (dst_positive_scale_prefix_tail_resultentry)) + ((dst_positive_scale_prefix_tail_resultentry) + (dst_positive_scale_prefix_tail_resultentry))) + (((dst_negative_code_prefix_tail_resultentry) + (dst_negative_scale_prefix_tail_resultentry)) * S ((dst_negative_code_prefix_tail_resultentry) + (dst_negative_scale_prefix_tail_resultentry)) + ((dst_negative_scale_prefix_tail_resultentry) + (dst_negative_scale_prefix_tail_resultentry)))) + ((((dst_negative_code_prefix_tail_resultentry) + (dst_negative_scale_prefix_tail_resultentry)) * S ((dst_negative_code_prefix_tail_resultentry) + (dst_negative_scale_prefix_tail_resultentry)) + ((dst_negative_scale_prefix_tail_resultentry) + (dst_negative_scale_prefix_tail_resultentry))) + (((dst_negative_code_prefix_tail_resultentry) + (dst_negative_scale_prefix_tail_resultentry)) * S ((dst_negative_code_prefix_tail_resultentry) + (dst_negative_scale_prefix_tail_resultentry)) + ((dst_negative_scale_prefix_tail_resultentry) + (dst_negative_scale_prefix_tail_resultentry)))))) /\ (((((exists ff_h_pvs_prefix_tail_resultentrypositive. ff_h_pvs_prefix_tail_resultentrypositive + S (dst_positive_prefix_tail_resultentry) = S ((S (sfs_index_prefix_tail_result)) * dst_positive_scale_prefix_tail_resultentry)) /\ exists ff_q_pvs_prefix_tail_resultentrypositive. dst_positive_code_prefix_tail_resultentry = ff_q_pvs_prefix_tail_resultentrypositive * S ((S (sfs_index_prefix_tail_result)) * dst_positive_scale_prefix_tail_resultentry) + (dst_positive_prefix_tail_resultentry))) /\ (((((exists ff_h_pvs_prefix_tail_resultentrynegative. ff_h_pvs_prefix_tail_resultentrynegative + S (dst_negative_prefix_tail_resultentry) = S ((S (sfs_index_prefix_tail_result)) * dst_negative_scale_prefix_tail_resultentry)) /\ exists ff_q_pvs_prefix_tail_resultentrynegative. dst_negative_code_prefix_tail_resultentry = ff_q_pvs_prefix_tail_resultentrynegative * S ((S (sfs_index_prefix_tail_result)) * dst_negative_scale_prefix_tail_resultentry) + (dst_negative_prefix_tail_resultentry))) /\ (exists ge_balance_positive_prefix_tail_resultentryvalue ge_balance_negative_prefix_tail_resultentryvalue. (((((sfs_value_prefix_tail_result) = 2 * (ge_balance_positive_prefix_tail_resultentryvalue) /\ (ge_balance_negative_prefix_tail_resultentryvalue) = 0) \/ exists ge_signed_half_prefix_tail_resultentryvaluedecode. (((sfs_value_prefix_tail_result) = 2 * ge_signed_half_prefix_tail_resultentryvaluedecode + 1 /\ (ge_balance_positive_prefix_tail_resultentryvalue) = 0) /\ (ge_balance_negative_prefix_tail_resultentryvalue) = S ge_signed_half_prefix_tail_resultentryvaluedecode))) /\ ((dst_positive_prefix_tail_resultentry) + ge_balance_negative_prefix_tail_resultentryvalue = (dst_negative_prefix_tail_resultentry) + ge_balance_positive_prefix_tail_resultentryvalue))))))))) -> sfs_value_prefix_tail_result=0)

Constructive proof overview

Generated structural guide

Every actually stored convolution summand after index n is zero, with the inclusive prefix endpoints retained exactly.

The unchanged tactic script uses 3 declared prerequisites and contains 34 exact native proof lines.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

DC0025 dirichlet_convolution_entry_past_support_zero DC000B dirichlet_convolution_prefix_lookup le_of_succ_le_succ Stable theorem; checked-use authorized

Direct dependents

DC0027 dirichlet_convolution_from_padded_prefix

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

34 script commands · 5 reading checkpoints · 0 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.

Named ingredients (2)

dirichlet convolution entry past support zero dirichlet convolution prefix lookup

01Fix variables and assumptionsL1–10

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