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.

Each retained summand has a witnessed n=d*q and actual signed multiplication. Zero and nondivisors contribute zero. Input and output values at zero are unrestricted; uniqueness is for positive represented values. The separate inverse family proves the unit-at-one criterion. Full G009 multiplicative-function closure is now admitted in the separate Alpha-v32 multiplicative-convolution family.

Exact theorem in conservative defined notation

∀ F. ∀ G. ∀ n. ∀ L. ∀ M. ¬n = 0 → DirichletPrefix(F,G,n,L,M) → SignedZeroWindow(M,S n,S L)

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

Definition DAG

SignedZeroWindow(F,k,l) · 1 DirichletPrefix(F,G,n,l,M) · 1

Actual proof prerequisites

dirichlet_convolution_entry_past_support_zero dirichlet_convolution_prefix_lookup le_of_succ_le_succ · checked external prerequisite

Original expanded first-order 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)

Complete tactic proof in conservative notation

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

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.

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)

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.