DC0020

dirichlet_convolution_prefix_value_from_entry

Every independently justified summand value is present in the actual prefix, by constructed lookup and functionality.

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.

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. ∀ d. ∀ z. DirichletPrefix(F,G,n,l,M) → Le(d,l) → DirichletEntry(F,G,n,d,z) → ArithAt(M,d,z)

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

Definition DAG

ArithAt(F,i,z) · 2DirichletEntry(F,G,n,d,z) · 1DirichletPrefix(F,G,n,l,M) · 1Le(a,b) · 1

Actual proof prerequisites

divisor_signed_table_lookup · checked external prerequisitedirichlet_convolution_entry_functional
Original expanded first-order statement 
forall F G n l M d z. (((exists dst_positive_code_value_prefixtable dst_positive_scale_value_prefixtable dst_negative_code_value_prefixtable dst_negative_scale_value_prefixtable. (((M) = (((((dst_positive_code_value_prefixtable) + (dst_positive_scale_value_prefixtable)) * S ((dst_positive_code_value_prefixtable) + (dst_positive_scale_value_prefixtable)) + ((dst_positive_scale_value_prefixtable) + (dst_positive_scale_value_prefixtable))) + (((dst_negative_code_value_prefixtable) + (dst_negative_scale_value_prefixtable)) * S ((dst_negative_code_value_prefixtable) + (dst_negative_scale_value_prefixtable)) + ((dst_negative_scale_value_prefixtable) + (dst_negative_scale_value_prefixtable)))) * S ((((dst_positive_code_value_prefixtable) + (dst_positive_scale_value_prefixtable)) * S ((dst_positive_code_value_prefixtable) + (dst_positive_scale_value_prefixtable)) + ((dst_positive_scale_value_prefixtable) + (dst_positive_scale_value_prefixtable))) + (((dst_negative_code_value_prefixtable) + (dst_negative_scale_value_prefixtable)) * S ((dst_negative_code_value_prefixtable) + (dst_negative_scale_value_prefixtable)) + ((dst_negative_scale_value_prefixtable) + (dst_negative_scale_value_prefixtable)))) + ((((dst_negative_code_value_prefixtable) + (dst_negative_scale_value_prefixtable)) * S ((dst_negative_code_value_prefixtable) + (dst_negative_scale_value_prefixtable)) + ((dst_negative_scale_value_prefixtable) + (dst_negative_scale_value_prefixtable))) + (((dst_negative_code_value_prefixtable) + (dst_negative_scale_value_prefixtable)) * S ((dst_negative_code_value_prefixtable) + (dst_negative_scale_value_prefixtable)) + ((dst_negative_scale_value_prefixtable) + (dst_negative_scale_value_prefixtable)))))) /\ (forall dst_index_value_prefixtable. (exists pvs_le_gap_value_prefixtabledomain. pvs_le_gap_value_prefixtabledomain + (dst_index_value_prefixtable) = (l)) -> exists dst_positive_value_prefixtable dst_negative_value_prefixtable dst_value_value_prefixtable. ((((exists ff_h_pvs_value_prefixtableentrypositive. ff_h_pvs_value_prefixtableentrypositive + S (dst_positive_value_prefixtable) = S ((S (dst_index_value_prefixtable)) * dst_positive_scale_value_prefixtable)) /\ exists ff_q_pvs_value_prefixtableentrypositive. dst_positive_code_value_prefixtable = ff_q_pvs_value_prefixtableentrypositive * S ((S (dst_index_value_prefixtable)) * dst_positive_scale_value_prefixtable) + (dst_positive_value_prefixtable))) /\ (((((exists ff_h_pvs_value_prefixtableentrynegative. ff_h_pvs_value_prefixtableentrynegative + S (dst_negative_value_prefixtable) = S ((S (dst_index_value_prefixtable)) * dst_negative_scale_value_prefixtable)) /\ exists ff_q_pvs_value_prefixtableentrynegative. dst_negative_code_value_prefixtable = ff_q_pvs_value_prefixtableentrynegative * S ((S (dst_index_value_prefixtable)) * dst_negative_scale_value_prefixtable) + (dst_negative_value_prefixtable))) /\ (exists ge_balance_positive_value_prefixtableentryvalue ge_balance_negative_value_prefixtableentryvalue. (((((dst_value_value_prefixtable) = 2 * (ge_balance_positive_value_prefixtableentryvalue) /\ (ge_balance_negative_value_prefixtableentryvalue) = 0) \/ exists ge_signed_half_value_prefixtableentryvaluedecode. (((dst_value_value_prefixtable) = 2 * ge_signed_half_value_prefixtableentryvaluedecode + 1 /\ (ge_balance_positive_value_prefixtableentryvalue) = 0) /\ (ge_balance_negative_value_prefixtableentryvalue) = S ge_signed_half_value_prefixtableentryvaluedecode))) /\ ((dst_positive_value_prefixtable) + ge_balance_negative_value_prefixtableentryvalue = (dst_negative_value_prefixtable) + ge_balance_positive_value_prefixtableentryvalue))))))))) /\ (forall dc_index_value_prefix dc_value_value_prefix. (exists pvs_le_gap_value_prefixdomain. pvs_le_gap_value_prefixdomain + (dc_index_value_prefix) = (l)) -> (exists dst_positive_code_value_prefixlookup dst_positive_scale_value_prefixlookup dst_negative_code_value_prefixlookup dst_negative_scale_value_prefixlookup dst_positive_value_prefixlookup dst_negative_value_prefixlookup. (((M) = (((((dst_positive_code_value_prefixlookup) + (dst_positive_scale_value_prefixlookup)) * S ((dst_positive_code_value_prefixlookup) + (dst_positive_scale_value_prefixlookup)) + ((dst_positive_scale_value_prefixlookup) + (dst_positive_scale_value_prefixlookup))) + (((dst_negative_code_value_prefixlookup) + (dst_negative_scale_value_prefixlookup)) * S ((dst_negative_code_value_prefixlookup) + (dst_negative_scale_value_prefixlookup)) + ((dst_negative_scale_value_prefixlookup) + (dst_negative_scale_value_prefixlookup)))) * S ((((dst_positive_code_value_prefixlookup) + (dst_positive_scale_value_prefixlookup)) * S ((dst_positive_code_value_prefixlookup) + (dst_positive_scale_value_prefixlookup)) + ((dst_positive_scale_value_prefixlookup) + (dst_positive_scale_value_prefixlookup))) + (((dst_negative_code_value_prefixlookup) + (dst_negative_scale_value_prefixlookup)) * S ((dst_negative_code_value_prefixlookup) + (dst_negative_scale_value_prefixlookup)) + ((dst_negative_scale_value_prefixlookup) + (dst_negative_scale_value_prefixlookup)))) + ((((dst_negative_code_value_prefixlookup) + (dst_negative_scale_value_prefixlookup)) * S ((dst_negative_code_value_prefixlookup) + (dst_negative_scale_value_prefixlookup)) + ((dst_negative_scale_value_prefixlookup) + (dst_negative_scale_value_prefixlookup))) + (((dst_negative_code_value_prefixlookup) + (dst_negative_scale_value_prefixlookup)) * S ((dst_negative_code_value_prefixlookup) + (dst_negative_scale_value_prefixlookup)) + ((dst_negative_scale_value_prefixlookup) + (dst_negative_scale_value_prefixlookup)))))) /\ (((((exists ff_h_pvs_value_prefixlookuppositive. ff_h_pvs_value_prefixlookuppositive + S (dst_positive_value_prefixlookup) = S ((S (dc_index_value_prefix)) * dst_positive_scale_value_prefixlookup)) /\ exists ff_q_pvs_value_prefixlookuppositive. dst_positive_code_value_prefixlookup = ff_q_pvs_value_prefixlookuppositive * S ((S (dc_index_value_prefix)) * dst_positive_scale_value_prefixlookup) + (dst_positive_value_prefixlookup))) /\ (((((exists ff_h_pvs_value_prefixlookupnegative. ff_h_pvs_value_prefixlookupnegative + S (dst_negative_value_prefixlookup) = S ((S (dc_index_value_prefix)) * dst_negative_scale_value_prefixlookup)) /\ exists ff_q_pvs_value_prefixlookupnegative. dst_negative_code_value_prefixlookup = ff_q_pvs_value_prefixlookupnegative * S ((S (dc_index_value_prefix)) * dst_negative_scale_value_prefixlookup) + (dst_negative_value_prefixlookup))) /\ (exists ge_balance_positive_value_prefixlookupvalue ge_balance_negative_value_prefixlookupvalue. (((((dc_value_value_prefix) = 2 * (ge_balance_positive_value_prefixlookupvalue) /\ (ge_balance_negative_value_prefixlookupvalue) = 0) \/ exists ge_signed_half_value_prefixlookupvaluedecode. (((dc_value_value_prefix) = 2 * ge_signed_half_value_prefixlookupvaluedecode + 1 /\ (ge_balance_positive_value_prefixlookupvalue) = 0) /\ (ge_balance_negative_value_prefixlookupvalue) = S ge_signed_half_value_prefixlookupvaluedecode))) /\ ((dst_positive_value_prefixlookup) + ge_balance_negative_value_prefixlookupvalue = (dst_negative_value_prefixlookup) + ge_balance_positive_value_prefixlookupvalue))))))))) -> ((((~((dc_index_value_prefix)=0)) /\ (exists dc_quotient_value_prefixentry dc_left_value_prefixentry dc_right_value_prefixentry. (((n)=(dc_index_value_prefix)*dc_quotient_value_prefixentry) /\ (((exists dst_positive_code_value_prefixentryleft dst_positive_scale_value_prefixentryleft dst_negative_code_value_prefixentryleft dst_negative_scale_value_prefixentryleft dst_positive_value_prefixentryleft dst_negative_value_prefixentryleft. (((F) = (((((dst_positive_code_value_prefixentryleft) + (dst_positive_scale_value_prefixentryleft)) * S ((dst_positive_code_value_prefixentryleft) + (dst_positive_scale_value_prefixentryleft)) + ((dst_positive_scale_value_prefixentryleft) + (dst_positive_scale_value_prefixentryleft))) + (((dst_negative_code_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft)) * S ((dst_negative_code_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft)) + ((dst_negative_scale_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft)))) * S ((((dst_positive_code_value_prefixentryleft) + (dst_positive_scale_value_prefixentryleft)) * S ((dst_positive_code_value_prefixentryleft) + (dst_positive_scale_value_prefixentryleft)) + ((dst_positive_scale_value_prefixentryleft) + (dst_positive_scale_value_prefixentryleft))) + (((dst_negative_code_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft)) * S ((dst_negative_code_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft)) + ((dst_negative_scale_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft)))) + ((((dst_negative_code_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft)) * S ((dst_negative_code_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft)) + ((dst_negative_scale_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft))) + (((dst_negative_code_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft)) * S ((dst_negative_code_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft)) + ((dst_negative_scale_value_prefixentryleft) + (dst_negative_scale_value_prefixentryleft)))))) /\ (((((exists ff_h_pvs_value_prefixentryleftpositive. ff_h_pvs_value_prefixentryleftpositive + S (dst_positive_value_prefixentryleft) = S ((S (dc_index_value_prefix)) * dst_positive_scale_value_prefixentryleft)) /\ exists ff_q_pvs_value_prefixentryleftpositive. dst_positive_code_value_prefixentryleft = ff_q_pvs_value_prefixentryleftpositive * S ((S (dc_index_value_prefix)) * dst_positive_scale_value_prefixentryleft) + (dst_positive_value_prefixentryleft))) /\ (((((exists ff_h_pvs_value_prefixentryleftnegative. ff_h_pvs_value_prefixentryleftnegative + S (dst_negative_value_prefixentryleft) = S ((S (dc_index_value_prefix)) * dst_negative_scale_value_prefixentryleft)) /\ exists ff_q_pvs_value_prefixentryleftnegative. dst_negative_code_value_prefixentryleft = ff_q_pvs_value_prefixentryleftnegative * S ((S (dc_index_value_prefix)) * dst_negative_scale_value_prefixentryleft) + (dst_negative_value_prefixentryleft))) /\ (exists ge_balance_positive_value_prefixentryleftvalue ge_balance_negative_value_prefixentryleftvalue. (((((dc_left_value_prefixentry) = 2 * (ge_balance_positive_value_prefixentryleftvalue) /\ (ge_balance_negative_value_prefixentryleftvalue) = 0) \/ exists ge_signed_half_value_prefixentryleftvaluedecode. (((dc_left_value_prefixentry) = 2 * ge_signed_half_value_prefixentryleftvaluedecode + 1 /\ (ge_balance_positive_value_prefixentryleftvalue) = 0) /\ (ge_balance_negative_value_prefixentryleftvalue) = S ge_signed_half_value_prefixentryleftvaluedecode))) /\ ((dst_positive_value_prefixentryleft) + ge_balance_negative_value_prefixentryleftvalue = (dst_negative_value_prefixentryleft) + ge_balance_positive_value_prefixentryleftvalue))))))))) /\ (((exists dst_positive_code_value_prefixentryright dst_positive_scale_value_prefixentryright dst_negative_code_value_prefixentryright dst_negative_scale_value_prefixentryright dst_positive_value_prefixentryright dst_negative_value_prefixentryright. (((G) = (((((dst_positive_code_value_prefixentryright) + (dst_positive_scale_value_prefixentryright)) * S ((dst_positive_code_value_prefixentryright) + (dst_positive_scale_value_prefixentryright)) + ((dst_positive_scale_value_prefixentryright) + (dst_positive_scale_value_prefixentryright))) + (((dst_negative_code_value_prefixentryright) + (dst_negative_scale_value_prefixentryright)) * S ((dst_negative_code_value_prefixentryright) + (dst_negative_scale_value_prefixentryright)) + ((dst_negative_scale_value_prefixentryright) + (dst_negative_scale_value_prefixentryright)))) * S ((((dst_positive_code_value_prefixentryright) + (dst_positive_scale_value_prefixentryright)) * S ((dst_positive_code_value_prefixentryright) + (dst_positive_scale_value_prefixentryright)) + ((dst_positive_scale_value_prefixentryright) + (dst_positive_scale_value_prefixentryright))) + (((dst_negative_code_value_prefixentryright) + (dst_negative_scale_value_prefixentryright)) * S ((dst_negative_code_value_prefixentryright) + (dst_negative_scale_value_prefixentryright)) + ((dst_negative_scale_value_prefixentryright) + (dst_negative_scale_value_prefixentryright)))) + ((((dst_negative_code_value_prefixentryright) + (dst_negative_scale_value_prefixentryright)) * S ((dst_negative_code_value_prefixentryright) + (dst_negative_scale_value_prefixentryright)) + ((dst_negative_scale_value_prefixentryright) + (dst_negative_scale_value_prefixentryright))) + (((dst_negative_code_value_prefixentryright) + (dst_negative_scale_value_prefixentryright)) * S ((dst_negative_code_value_prefixentryright) + (dst_negative_scale_value_prefixentryright)) + ((dst_negative_scale_value_prefixentryright) + (dst_negative_scale_value_prefixentryright)))))) /\ (((((exists ff_h_pvs_value_prefixentryrightpositive. ff_h_pvs_value_prefixentryrightpositive + S (dst_positive_value_prefixentryright) = S ((S (dc_quotient_value_prefixentry)) * dst_positive_scale_value_prefixentryright)) /\ exists ff_q_pvs_value_prefixentryrightpositive. dst_positive_code_value_prefixentryright = ff_q_pvs_value_prefixentryrightpositive * S ((S (dc_quotient_value_prefixentry)) * dst_positive_scale_value_prefixentryright) + (dst_positive_value_prefixentryright))) /\ (((((exists ff_h_pvs_value_prefixentryrightnegative. ff_h_pvs_value_prefixentryrightnegative + S (dst_negative_value_prefixentryright) = S ((S (dc_quotient_value_prefixentry)) * dst_negative_scale_value_prefixentryright)) /\ exists ff_q_pvs_value_prefixentryrightnegative. dst_negative_code_value_prefixentryright = ff_q_pvs_value_prefixentryrightnegative * S ((S (dc_quotient_value_prefixentry)) * dst_negative_scale_value_prefixentryright) + (dst_negative_value_prefixentryright))) /\ (exists ge_balance_positive_value_prefixentryrightvalue ge_balance_negative_value_prefixentryrightvalue. (((((dc_right_value_prefixentry) = 2 * (ge_balance_positive_value_prefixentryrightvalue) /\ (ge_balance_negative_value_prefixentryrightvalue) = 0) \/ exists ge_signed_half_value_prefixentryrightvaluedecode. (((dc_right_value_prefixentry) = 2 * ge_signed_half_value_prefixentryrightvaluedecode + 1 /\ (ge_balance_positive_value_prefixentryrightvalue) = 0) /\ (ge_balance_negative_value_prefixentryrightvalue) = S ge_signed_half_value_prefixentryrightvaluedecode))) /\ ((dst_positive_value_prefixentryright) + ge_balance_negative_value_prefixentryrightvalue = (dst_negative_value_prefixentryright) + ge_balance_positive_value_prefixentryrightvalue))))))))) /\ (exists sto_ap_value_prefixentryproduct sto_an_value_prefixentryproduct sto_bp_value_prefixentryproduct sto_bn_value_prefixentryproduct sto_cp_value_prefixentryproduct sto_cn_value_prefixentryproduct. (((((dc_left_value_prefixentry) = 2 * (sto_ap_value_prefixentryproduct) /\ (sto_an_value_prefixentryproduct) = 0) \/ exists ge_signed_half_value_prefixentryproductleft. (((dc_left_value_prefixentry) = 2 * ge_signed_half_value_prefixentryproductleft + 1 /\ (sto_ap_value_prefixentryproduct) = 0) /\ (sto_an_value_prefixentryproduct) = S ge_signed_half_value_prefixentryproductleft))) /\ ((((((dc_right_value_prefixentry) = 2 * (sto_bp_value_prefixentryproduct) /\ (sto_bn_value_prefixentryproduct) = 0) \/ exists ge_signed_half_value_prefixentryproductright. (((dc_right_value_prefixentry) = 2 * ge_signed_half_value_prefixentryproductright + 1 /\ (sto_bp_value_prefixentryproduct) = 0) /\ (sto_bn_value_prefixentryproduct) = S ge_signed_half_value_prefixentryproductright))) /\ ((((((dc_value_value_prefix) = 2 * (sto_cp_value_prefixentryproduct) /\ (sto_cn_value_prefixentryproduct) = 0) \/ exists ge_signed_half_value_prefixentryproductoutput. (((dc_value_value_prefix) = 2 * ge_signed_half_value_prefixentryproductoutput + 1 /\ (sto_cp_value_prefixentryproduct) = 0) /\ (sto_cn_value_prefixentryproduct) = S ge_signed_half_value_prefixentryproductoutput))) /\ ((sto_ap_value_prefixentryproduct * sto_bp_value_prefixentryproduct + sto_an_value_prefixentryproduct * sto_bn_value_prefixentryproduct) + sto_cn_value_prefixentryproduct = (sto_ap_value_prefixentryproduct * sto_bn_value_prefixentryproduct + sto_an_value_prefixentryproduct * sto_bp_value_prefixentryproduct) + sto_cp_value_prefixentryproduct))))))))))))))) \/ ((((dc_index_value_prefix)=0 \/ ~(exists pvs_factor_value_prefixentrynondivisor. (n) = (dc_index_value_prefix) * pvs_factor_value_prefixentrynondivisor)) /\ ((dc_value_value_prefix)=0))))))) -> (exists pvs_le_gap_value_bound. pvs_le_gap_value_bound + (d) = (l)) -> ((((~((d)=0)) /\ (exists dc_quotient_value_graph dc_left_value_graph dc_right_value_graph. (((n)=(d)*dc_quotient_value_graph) /\ (((exists dst_positive_code_value_graphleft dst_positive_scale_value_graphleft dst_negative_code_value_graphleft dst_negative_scale_value_graphleft dst_positive_value_graphleft dst_negative_value_graphleft. (((F) = (((((dst_positive_code_value_graphleft) + (dst_positive_scale_value_graphleft)) * S ((dst_positive_code_value_graphleft) + (dst_positive_scale_value_graphleft)) + ((dst_positive_scale_value_graphleft) + (dst_positive_scale_value_graphleft))) + (((dst_negative_code_value_graphleft) + (dst_negative_scale_value_graphleft)) * S ((dst_negative_code_value_graphleft) + (dst_negative_scale_value_graphleft)) + ((dst_negative_scale_value_graphleft) + (dst_negative_scale_value_graphleft)))) * S ((((dst_positive_code_value_graphleft) + (dst_positive_scale_value_graphleft)) * S ((dst_positive_code_value_graphleft) + (dst_positive_scale_value_graphleft)) + ((dst_positive_scale_value_graphleft) + (dst_positive_scale_value_graphleft))) + (((dst_negative_code_value_graphleft) + (dst_negative_scale_value_graphleft)) * S ((dst_negative_code_value_graphleft) + (dst_negative_scale_value_graphleft)) + ((dst_negative_scale_value_graphleft) + (dst_negative_scale_value_graphleft)))) + ((((dst_negative_code_value_graphleft) + (dst_negative_scale_value_graphleft)) * S ((dst_negative_code_value_graphleft) + (dst_negative_scale_value_graphleft)) + ((dst_negative_scale_value_graphleft) + (dst_negative_scale_value_graphleft))) + (((dst_negative_code_value_graphleft) + (dst_negative_scale_value_graphleft)) * S ((dst_negative_code_value_graphleft) + (dst_negative_scale_value_graphleft)) + ((dst_negative_scale_value_graphleft) + (dst_negative_scale_value_graphleft)))))) /\ (((((exists ff_h_pvs_value_graphleftpositive. ff_h_pvs_value_graphleftpositive + S (dst_positive_value_graphleft) = S ((S (d)) * dst_positive_scale_value_graphleft)) /\ exists ff_q_pvs_value_graphleftpositive. dst_positive_code_value_graphleft = ff_q_pvs_value_graphleftpositive * S ((S (d)) * dst_positive_scale_value_graphleft) + (dst_positive_value_graphleft))) /\ (((((exists ff_h_pvs_value_graphleftnegative. ff_h_pvs_value_graphleftnegative + S (dst_negative_value_graphleft) = S ((S (d)) * dst_negative_scale_value_graphleft)) /\ exists ff_q_pvs_value_graphleftnegative. dst_negative_code_value_graphleft = ff_q_pvs_value_graphleftnegative * S ((S (d)) * dst_negative_scale_value_graphleft) + (dst_negative_value_graphleft))) /\ (exists ge_balance_positive_value_graphleftvalue ge_balance_negative_value_graphleftvalue. (((((dc_left_value_graph) = 2 * (ge_balance_positive_value_graphleftvalue) /\ (ge_balance_negative_value_graphleftvalue) = 0) \/ exists ge_signed_half_value_graphleftvaluedecode. (((dc_left_value_graph) = 2 * ge_signed_half_value_graphleftvaluedecode + 1 /\ (ge_balance_positive_value_graphleftvalue) = 0) /\ (ge_balance_negative_value_graphleftvalue) = S ge_signed_half_value_graphleftvaluedecode))) /\ ((dst_positive_value_graphleft) + ge_balance_negative_value_graphleftvalue = (dst_negative_value_graphleft) + ge_balance_positive_value_graphleftvalue))))))))) /\ (((exists dst_positive_code_value_graphright dst_positive_scale_value_graphright dst_negative_code_value_graphright dst_negative_scale_value_graphright dst_positive_value_graphright dst_negative_value_graphright. (((G) = (((((dst_positive_code_value_graphright) + (dst_positive_scale_value_graphright)) * S ((dst_positive_code_value_graphright) + (dst_positive_scale_value_graphright)) + ((dst_positive_scale_value_graphright) + (dst_positive_scale_value_graphright))) + (((dst_negative_code_value_graphright) + (dst_negative_scale_value_graphright)) * S ((dst_negative_code_value_graphright) + (dst_negative_scale_value_graphright)) + ((dst_negative_scale_value_graphright) + (dst_negative_scale_value_graphright)))) * S ((((dst_positive_code_value_graphright) + (dst_positive_scale_value_graphright)) * S ((dst_positive_code_value_graphright) + (dst_positive_scale_value_graphright)) + ((dst_positive_scale_value_graphright) + (dst_positive_scale_value_graphright))) + (((dst_negative_code_value_graphright) + (dst_negative_scale_value_graphright)) * S ((dst_negative_code_value_graphright) + (dst_negative_scale_value_graphright)) + ((dst_negative_scale_value_graphright) + (dst_negative_scale_value_graphright)))) + ((((dst_negative_code_value_graphright) + (dst_negative_scale_value_graphright)) * S ((dst_negative_code_value_graphright) + (dst_negative_scale_value_graphright)) + ((dst_negative_scale_value_graphright) + (dst_negative_scale_value_graphright))) + (((dst_negative_code_value_graphright) + (dst_negative_scale_value_graphright)) * S ((dst_negative_code_value_graphright) + (dst_negative_scale_value_graphright)) + ((dst_negative_scale_value_graphright) + (dst_negative_scale_value_graphright)))))) /\ (((((exists ff_h_pvs_value_graphrightpositive. ff_h_pvs_value_graphrightpositive + S (dst_positive_value_graphright) = S ((S (dc_quotient_value_graph)) * dst_positive_scale_value_graphright)) /\ exists ff_q_pvs_value_graphrightpositive. dst_positive_code_value_graphright = ff_q_pvs_value_graphrightpositive * S ((S (dc_quotient_value_graph)) * dst_positive_scale_value_graphright) + (dst_positive_value_graphright))) /\ (((((exists ff_h_pvs_value_graphrightnegative. ff_h_pvs_value_graphrightnegative + S (dst_negative_value_graphright) = S ((S (dc_quotient_value_graph)) * dst_negative_scale_value_graphright)) /\ exists ff_q_pvs_value_graphrightnegative. dst_negative_code_value_graphright = ff_q_pvs_value_graphrightnegative * S ((S (dc_quotient_value_graph)) * dst_negative_scale_value_graphright) + (dst_negative_value_graphright))) /\ (exists ge_balance_positive_value_graphrightvalue ge_balance_negative_value_graphrightvalue. (((((dc_right_value_graph) = 2 * (ge_balance_positive_value_graphrightvalue) /\ (ge_balance_negative_value_graphrightvalue) = 0) \/ exists ge_signed_half_value_graphrightvaluedecode. (((dc_right_value_graph) = 2 * ge_signed_half_value_graphrightvaluedecode + 1 /\ (ge_balance_positive_value_graphrightvalue) = 0) /\ (ge_balance_negative_value_graphrightvalue) = S ge_signed_half_value_graphrightvaluedecode))) /\ ((dst_positive_value_graphright) + ge_balance_negative_value_graphrightvalue = (dst_negative_value_graphright) + ge_balance_positive_value_graphrightvalue))))))))) /\ (exists sto_ap_value_graphproduct sto_an_value_graphproduct sto_bp_value_graphproduct sto_bn_value_graphproduct sto_cp_value_graphproduct sto_cn_value_graphproduct. (((((dc_left_value_graph) = 2 * (sto_ap_value_graphproduct) /\ (sto_an_value_graphproduct) = 0) \/ exists ge_signed_half_value_graphproductleft. (((dc_left_value_graph) = 2 * ge_signed_half_value_graphproductleft + 1 /\ (sto_ap_value_graphproduct) = 0) /\ (sto_an_value_graphproduct) = S ge_signed_half_value_graphproductleft))) /\ ((((((dc_right_value_graph) = 2 * (sto_bp_value_graphproduct) /\ (sto_bn_value_graphproduct) = 0) \/ exists ge_signed_half_value_graphproductright. (((dc_right_value_graph) = 2 * ge_signed_half_value_graphproductright + 1 /\ (sto_bp_value_graphproduct) = 0) /\ (sto_bn_value_graphproduct) = S ge_signed_half_value_graphproductright))) /\ ((((((z) = 2 * (sto_cp_value_graphproduct) /\ (sto_cn_value_graphproduct) = 0) \/ exists ge_signed_half_value_graphproductoutput. (((z) = 2 * ge_signed_half_value_graphproductoutput + 1 /\ (sto_cp_value_graphproduct) = 0) /\ (sto_cn_value_graphproduct) = S ge_signed_half_value_graphproductoutput))) /\ ((sto_ap_value_graphproduct * sto_bp_value_graphproduct + sto_an_value_graphproduct * sto_bn_value_graphproduct) + sto_cn_value_graphproduct = (sto_ap_value_graphproduct * sto_bn_value_graphproduct + sto_an_value_graphproduct * sto_bp_value_graphproduct) + sto_cp_value_graphproduct))))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_value_graphnondivisor. (n) = (d) * pvs_factor_value_graphnondivisor)) /\ ((z)=0)))) -> (exists dst_positive_code_value_result dst_positive_scale_value_result dst_negative_code_value_result dst_negative_scale_value_result dst_positive_value_result dst_negative_value_result. (((M) = (((((dst_positive_code_value_result) + (dst_positive_scale_value_result)) * S ((dst_positive_code_value_result) + (dst_positive_scale_value_result)) + ((dst_positive_scale_value_result) + (dst_positive_scale_value_result))) + (((dst_negative_code_value_result) + (dst_negative_scale_value_result)) * S ((dst_negative_code_value_result) + (dst_negative_scale_value_result)) + ((dst_negative_scale_value_result) + (dst_negative_scale_value_result)))) * S ((((dst_positive_code_value_result) + (dst_positive_scale_value_result)) * S ((dst_positive_code_value_result) + (dst_positive_scale_value_result)) + ((dst_positive_scale_value_result) + (dst_positive_scale_value_result))) + (((dst_negative_code_value_result) + (dst_negative_scale_value_result)) * S ((dst_negative_code_value_result) + (dst_negative_scale_value_result)) + ((dst_negative_scale_value_result) + (dst_negative_scale_value_result)))) + ((((dst_negative_code_value_result) + (dst_negative_scale_value_result)) * S ((dst_negative_code_value_result) + (dst_negative_scale_value_result)) + ((dst_negative_scale_value_result) + (dst_negative_scale_value_result))) + (((dst_negative_code_value_result) + (dst_negative_scale_value_result)) * S ((dst_negative_code_value_result) + (dst_negative_scale_value_result)) + ((dst_negative_scale_value_result) + (dst_negative_scale_value_result)))))) /\ (((((exists ff_h_pvs_value_resultpositive. ff_h_pvs_value_resultpositive + S (dst_positive_value_result) = S ((S (d)) * dst_positive_scale_value_result)) /\ exists ff_q_pvs_value_resultpositive. dst_positive_code_value_result = ff_q_pvs_value_resultpositive * S ((S (d)) * dst_positive_scale_value_result) + (dst_positive_value_result))) /\ (((((exists ff_h_pvs_value_resultnegative. ff_h_pvs_value_resultnegative + S (dst_negative_value_result) = S ((S (d)) * dst_negative_scale_value_result)) /\ exists ff_q_pvs_value_resultnegative. dst_negative_code_value_result = ff_q_pvs_value_resultnegative * S ((S (d)) * dst_negative_scale_value_result) + (dst_negative_value_result))) /\ (exists ge_balance_positive_value_resultvalue ge_balance_negative_value_resultvalue. (((((z) = 2 * (ge_balance_positive_value_resultvalue) /\ (ge_balance_negative_value_resultvalue) = 0) \/ exists ge_signed_half_value_resultvaluedecode. (((z) = 2 * ge_signed_half_value_resultvaluedecode + 1 /\ (ge_balance_positive_value_resultvalue) = 0) /\ (ge_balance_negative_value_resultvalue) = S ge_signed_half_value_resultvaluedecode))) /\ ((dst_positive_value_result) + ge_balance_negative_value_resultvalue = (dst_negative_value_result) + ge_balance_positive_value_resultvalue)))))))))

Complete tactic proof in conservative notation

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

36 script commands · 8 reading checkpoints · 2 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 (1)
dirichlet convolution entry functional
01Fix variables and assumptionsL1–10

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 l
  5. L5
    intro M
  6. L6
    intro d
  7. L7
    intro z
  8. L8
    intro hp
  9. L9
    intro hd
  10. L10
    intro he
02Separate the logical casesL11–11

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

  1. L11
    cases hp
03Establish hvL12–18

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

  1. L12
    have hv : ∃ v. ArithAt(M,d,v)Definitions: ArithAt(M,d,v)Original native command in the exact edition
  2. L13
    specialize divisor_signed_table_lookup (l)
  3. L14
    specialize divisor_signed_table_lookup (M)
  4. L15
    specialize divisor_signed_table_lookup (d)
  5. L16
    apply divisor_signed_table_lookup
  6. L17
    exact hp_left
  7. L18
    exact hd
04Separate the logical casesL19–19

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

  1. L19
    cases hv
05Establish heqL20–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet convolution entry functional.

  1. L20
    have heq : z=x
  2. L21
    specialize dirichlet_convolution_entry_functional (F)
  3. L22
    specialize dirichlet_convolution_entry_functional (G)
  4. L23
    specialize dirichlet_convolution_entry_functional (n)
  5. L24
    specialize dirichlet_convolution_entry_functional (d)
  6. L25
    specialize dirichlet_convolution_entry_functional (z)
  7. L26
    specialize dirichlet_convolution_entry_functional (x)
  8. L27
    apply dirichlet_convolution_entry_functional
  9. L28
    exact he
  10. L29
    specialize hp_right (d)
06Use earlier factsL30–33

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

  1. L30
    specialize hp_right (x)
  2. L31
    apply hp_right
  3. L32
    exact hd
  4. L33
    exact hv_witness
07Calculate and transport equalitiesL34–35

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

  1. L34
    rewrite heq
  2. L35
    rewrite heq
08Use earlier factsL36–36

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

  1. L36
    exact hv_witness

Library-wide reading audit

Original defined command ledger · 36 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro n
  4. 0004intro l
  5. 0005intro M
  6. 0006intro d
  7. 0007intro z
  8. 0008intro hp
  9. 0009intro hd
  10. 0010intro he
  11. 0011cases hp
  12. 0012have hv : ∃ v. ArithAt(M,d,v)
  13. 0013specialize divisor_signed_table_lookup (l)
  14. 0014specialize divisor_signed_table_lookup (M)
  15. 0015specialize divisor_signed_table_lookup (d)
  16. 0016apply divisor_signed_table_lookup
  17. 0017exact hp_left
  18. 0018exact hd
  19. 0019cases hv
  20. 0020have heq : z=x
  21. 0021specialize dirichlet_convolution_entry_functional (F)
  22. 0022specialize dirichlet_convolution_entry_functional (G)
  23. 0023specialize dirichlet_convolution_entry_functional (n)
  24. 0024specialize dirichlet_convolution_entry_functional (d)
  25. 0025specialize dirichlet_convolution_entry_functional (z)
  26. 0026specialize dirichlet_convolution_entry_functional (x)
  27. 0027apply dirichlet_convolution_entry_functional
  28. 0028exact he
  29. 0029specialize hp_right (d)
  30. 0030specialize hp_right (x)
  31. 0031apply hp_right
  32. 0032exact hd
  33. 0033exact hv_witness
  34. 0034rewrite heq
  35. 0035rewrite heq
  36. 0036exact hv_witness