DC000E

dirichlet_convolution_prefix_quotient_entry

At every witnessed positive divisor, the actual summand table contains precisely F(d)*G(q), with n=d*q supplied and checked.

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. ∀ q. ∀ a. ∀ b. ∀ z. DirichletPrefix(F,G,n,l,M) → Le(d,l) → ¬d = 0 → n = d · q → ArithAt(F,d,a) → ArithAt(G,q,b) → SignedMul(a,b,z) → ArithAt(M,d,z)

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

Definition DAG

SignedMul(a,b,c) · 1ArithAt(F,i,z) · 4DirichletPrefix(F,G,n,l,M) · 1Le(a,b) · 1

Actual proof prerequisites

divisor_signed_table_lookup · checked external prerequisitedirichlet_convolution_entry_functionaldirichlet_convolution_entry_from_quotient
Original expanded first-order statement 
forall F G n l M d q a b z. (((exists dst_positive_code_keep_prefixtable dst_positive_scale_keep_prefixtable dst_negative_code_keep_prefixtable dst_negative_scale_keep_prefixtable. (((M) = (((((dst_positive_code_keep_prefixtable) + (dst_positive_scale_keep_prefixtable)) * S ((dst_positive_code_keep_prefixtable) + (dst_positive_scale_keep_prefixtable)) + ((dst_positive_scale_keep_prefixtable) + (dst_positive_scale_keep_prefixtable))) + (((dst_negative_code_keep_prefixtable) + (dst_negative_scale_keep_prefixtable)) * S ((dst_negative_code_keep_prefixtable) + (dst_negative_scale_keep_prefixtable)) + ((dst_negative_scale_keep_prefixtable) + (dst_negative_scale_keep_prefixtable)))) * S ((((dst_positive_code_keep_prefixtable) + (dst_positive_scale_keep_prefixtable)) * S ((dst_positive_code_keep_prefixtable) + (dst_positive_scale_keep_prefixtable)) + ((dst_positive_scale_keep_prefixtable) + (dst_positive_scale_keep_prefixtable))) + (((dst_negative_code_keep_prefixtable) + (dst_negative_scale_keep_prefixtable)) * S ((dst_negative_code_keep_prefixtable) + (dst_negative_scale_keep_prefixtable)) + ((dst_negative_scale_keep_prefixtable) + (dst_negative_scale_keep_prefixtable)))) + ((((dst_negative_code_keep_prefixtable) + (dst_negative_scale_keep_prefixtable)) * S ((dst_negative_code_keep_prefixtable) + (dst_negative_scale_keep_prefixtable)) + ((dst_negative_scale_keep_prefixtable) + (dst_negative_scale_keep_prefixtable))) + (((dst_negative_code_keep_prefixtable) + (dst_negative_scale_keep_prefixtable)) * S ((dst_negative_code_keep_prefixtable) + (dst_negative_scale_keep_prefixtable)) + ((dst_negative_scale_keep_prefixtable) + (dst_negative_scale_keep_prefixtable)))))) /\ (forall dst_index_keep_prefixtable. (exists pvs_le_gap_keep_prefixtabledomain. pvs_le_gap_keep_prefixtabledomain + (dst_index_keep_prefixtable) = (l)) -> exists dst_positive_keep_prefixtable dst_negative_keep_prefixtable dst_value_keep_prefixtable. ((((exists ff_h_pvs_keep_prefixtableentrypositive. ff_h_pvs_keep_prefixtableentrypositive + S (dst_positive_keep_prefixtable) = S ((S (dst_index_keep_prefixtable)) * dst_positive_scale_keep_prefixtable)) /\ exists ff_q_pvs_keep_prefixtableentrypositive. dst_positive_code_keep_prefixtable = ff_q_pvs_keep_prefixtableentrypositive * S ((S (dst_index_keep_prefixtable)) * dst_positive_scale_keep_prefixtable) + (dst_positive_keep_prefixtable))) /\ (((((exists ff_h_pvs_keep_prefixtableentrynegative. ff_h_pvs_keep_prefixtableentrynegative + S (dst_negative_keep_prefixtable) = S ((S (dst_index_keep_prefixtable)) * dst_negative_scale_keep_prefixtable)) /\ exists ff_q_pvs_keep_prefixtableentrynegative. dst_negative_code_keep_prefixtable = ff_q_pvs_keep_prefixtableentrynegative * S ((S (dst_index_keep_prefixtable)) * dst_negative_scale_keep_prefixtable) + (dst_negative_keep_prefixtable))) /\ (exists ge_balance_positive_keep_prefixtableentryvalue ge_balance_negative_keep_prefixtableentryvalue. (((((dst_value_keep_prefixtable) = 2 * (ge_balance_positive_keep_prefixtableentryvalue) /\ (ge_balance_negative_keep_prefixtableentryvalue) = 0) \/ exists ge_signed_half_keep_prefixtableentryvaluedecode. (((dst_value_keep_prefixtable) = 2 * ge_signed_half_keep_prefixtableentryvaluedecode + 1 /\ (ge_balance_positive_keep_prefixtableentryvalue) = 0) /\ (ge_balance_negative_keep_prefixtableentryvalue) = S ge_signed_half_keep_prefixtableentryvaluedecode))) /\ ((dst_positive_keep_prefixtable) + ge_balance_negative_keep_prefixtableentryvalue = (dst_negative_keep_prefixtable) + ge_balance_positive_keep_prefixtableentryvalue))))))))) /\ (forall dc_index_keep_prefix dc_value_keep_prefix. (exists pvs_le_gap_keep_prefixdomain. pvs_le_gap_keep_prefixdomain + (dc_index_keep_prefix) = (l)) -> (exists dst_positive_code_keep_prefixlookup dst_positive_scale_keep_prefixlookup dst_negative_code_keep_prefixlookup dst_negative_scale_keep_prefixlookup dst_positive_keep_prefixlookup dst_negative_keep_prefixlookup. (((M) = (((((dst_positive_code_keep_prefixlookup) + (dst_positive_scale_keep_prefixlookup)) * S ((dst_positive_code_keep_prefixlookup) + (dst_positive_scale_keep_prefixlookup)) + ((dst_positive_scale_keep_prefixlookup) + (dst_positive_scale_keep_prefixlookup))) + (((dst_negative_code_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup)) * S ((dst_negative_code_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup)) + ((dst_negative_scale_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup)))) * S ((((dst_positive_code_keep_prefixlookup) + (dst_positive_scale_keep_prefixlookup)) * S ((dst_positive_code_keep_prefixlookup) + (dst_positive_scale_keep_prefixlookup)) + ((dst_positive_scale_keep_prefixlookup) + (dst_positive_scale_keep_prefixlookup))) + (((dst_negative_code_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup)) * S ((dst_negative_code_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup)) + ((dst_negative_scale_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup)))) + ((((dst_negative_code_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup)) * S ((dst_negative_code_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup)) + ((dst_negative_scale_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup))) + (((dst_negative_code_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup)) * S ((dst_negative_code_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup)) + ((dst_negative_scale_keep_prefixlookup) + (dst_negative_scale_keep_prefixlookup)))))) /\ (((((exists ff_h_pvs_keep_prefixlookuppositive. ff_h_pvs_keep_prefixlookuppositive + S (dst_positive_keep_prefixlookup) = S ((S (dc_index_keep_prefix)) * dst_positive_scale_keep_prefixlookup)) /\ exists ff_q_pvs_keep_prefixlookuppositive. dst_positive_code_keep_prefixlookup = ff_q_pvs_keep_prefixlookuppositive * S ((S (dc_index_keep_prefix)) * dst_positive_scale_keep_prefixlookup) + (dst_positive_keep_prefixlookup))) /\ (((((exists ff_h_pvs_keep_prefixlookupnegative. ff_h_pvs_keep_prefixlookupnegative + S (dst_negative_keep_prefixlookup) = S ((S (dc_index_keep_prefix)) * dst_negative_scale_keep_prefixlookup)) /\ exists ff_q_pvs_keep_prefixlookupnegative. dst_negative_code_keep_prefixlookup = ff_q_pvs_keep_prefixlookupnegative * S ((S (dc_index_keep_prefix)) * dst_negative_scale_keep_prefixlookup) + (dst_negative_keep_prefixlookup))) /\ (exists ge_balance_positive_keep_prefixlookupvalue ge_balance_negative_keep_prefixlookupvalue. (((((dc_value_keep_prefix) = 2 * (ge_balance_positive_keep_prefixlookupvalue) /\ (ge_balance_negative_keep_prefixlookupvalue) = 0) \/ exists ge_signed_half_keep_prefixlookupvaluedecode. (((dc_value_keep_prefix) = 2 * ge_signed_half_keep_prefixlookupvaluedecode + 1 /\ (ge_balance_positive_keep_prefixlookupvalue) = 0) /\ (ge_balance_negative_keep_prefixlookupvalue) = S ge_signed_half_keep_prefixlookupvaluedecode))) /\ ((dst_positive_keep_prefixlookup) + ge_balance_negative_keep_prefixlookupvalue = (dst_negative_keep_prefixlookup) + ge_balance_positive_keep_prefixlookupvalue))))))))) -> ((((~((dc_index_keep_prefix)=0)) /\ (exists dc_quotient_keep_prefixentry dc_left_keep_prefixentry dc_right_keep_prefixentry. (((n)=(dc_index_keep_prefix)*dc_quotient_keep_prefixentry) /\ (((exists dst_positive_code_keep_prefixentryleft dst_positive_scale_keep_prefixentryleft dst_negative_code_keep_prefixentryleft dst_negative_scale_keep_prefixentryleft dst_positive_keep_prefixentryleft dst_negative_keep_prefixentryleft. (((F) = (((((dst_positive_code_keep_prefixentryleft) + (dst_positive_scale_keep_prefixentryleft)) * S ((dst_positive_code_keep_prefixentryleft) + (dst_positive_scale_keep_prefixentryleft)) + ((dst_positive_scale_keep_prefixentryleft) + (dst_positive_scale_keep_prefixentryleft))) + (((dst_negative_code_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft)) * S ((dst_negative_code_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft)) + ((dst_negative_scale_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft)))) * S ((((dst_positive_code_keep_prefixentryleft) + (dst_positive_scale_keep_prefixentryleft)) * S ((dst_positive_code_keep_prefixentryleft) + (dst_positive_scale_keep_prefixentryleft)) + ((dst_positive_scale_keep_prefixentryleft) + (dst_positive_scale_keep_prefixentryleft))) + (((dst_negative_code_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft)) * S ((dst_negative_code_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft)) + ((dst_negative_scale_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft)))) + ((((dst_negative_code_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft)) * S ((dst_negative_code_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft)) + ((dst_negative_scale_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft))) + (((dst_negative_code_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft)) * S ((dst_negative_code_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft)) + ((dst_negative_scale_keep_prefixentryleft) + (dst_negative_scale_keep_prefixentryleft)))))) /\ (((((exists ff_h_pvs_keep_prefixentryleftpositive. ff_h_pvs_keep_prefixentryleftpositive + S (dst_positive_keep_prefixentryleft) = S ((S (dc_index_keep_prefix)) * dst_positive_scale_keep_prefixentryleft)) /\ exists ff_q_pvs_keep_prefixentryleftpositive. dst_positive_code_keep_prefixentryleft = ff_q_pvs_keep_prefixentryleftpositive * S ((S (dc_index_keep_prefix)) * dst_positive_scale_keep_prefixentryleft) + (dst_positive_keep_prefixentryleft))) /\ (((((exists ff_h_pvs_keep_prefixentryleftnegative. ff_h_pvs_keep_prefixentryleftnegative + S (dst_negative_keep_prefixentryleft) = S ((S (dc_index_keep_prefix)) * dst_negative_scale_keep_prefixentryleft)) /\ exists ff_q_pvs_keep_prefixentryleftnegative. dst_negative_code_keep_prefixentryleft = ff_q_pvs_keep_prefixentryleftnegative * S ((S (dc_index_keep_prefix)) * dst_negative_scale_keep_prefixentryleft) + (dst_negative_keep_prefixentryleft))) /\ (exists ge_balance_positive_keep_prefixentryleftvalue ge_balance_negative_keep_prefixentryleftvalue. (((((dc_left_keep_prefixentry) = 2 * (ge_balance_positive_keep_prefixentryleftvalue) /\ (ge_balance_negative_keep_prefixentryleftvalue) = 0) \/ exists ge_signed_half_keep_prefixentryleftvaluedecode. (((dc_left_keep_prefixentry) = 2 * ge_signed_half_keep_prefixentryleftvaluedecode + 1 /\ (ge_balance_positive_keep_prefixentryleftvalue) = 0) /\ (ge_balance_negative_keep_prefixentryleftvalue) = S ge_signed_half_keep_prefixentryleftvaluedecode))) /\ ((dst_positive_keep_prefixentryleft) + ge_balance_negative_keep_prefixentryleftvalue = (dst_negative_keep_prefixentryleft) + ge_balance_positive_keep_prefixentryleftvalue))))))))) /\ (((exists dst_positive_code_keep_prefixentryright dst_positive_scale_keep_prefixentryright dst_negative_code_keep_prefixentryright dst_negative_scale_keep_prefixentryright dst_positive_keep_prefixentryright dst_negative_keep_prefixentryright. (((G) = (((((dst_positive_code_keep_prefixentryright) + (dst_positive_scale_keep_prefixentryright)) * S ((dst_positive_code_keep_prefixentryright) + (dst_positive_scale_keep_prefixentryright)) + ((dst_positive_scale_keep_prefixentryright) + (dst_positive_scale_keep_prefixentryright))) + (((dst_negative_code_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright)) * S ((dst_negative_code_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright)) + ((dst_negative_scale_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright)))) * S ((((dst_positive_code_keep_prefixentryright) + (dst_positive_scale_keep_prefixentryright)) * S ((dst_positive_code_keep_prefixentryright) + (dst_positive_scale_keep_prefixentryright)) + ((dst_positive_scale_keep_prefixentryright) + (dst_positive_scale_keep_prefixentryright))) + (((dst_negative_code_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright)) * S ((dst_negative_code_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright)) + ((dst_negative_scale_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright)))) + ((((dst_negative_code_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright)) * S ((dst_negative_code_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright)) + ((dst_negative_scale_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright))) + (((dst_negative_code_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright)) * S ((dst_negative_code_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright)) + ((dst_negative_scale_keep_prefixentryright) + (dst_negative_scale_keep_prefixentryright)))))) /\ (((((exists ff_h_pvs_keep_prefixentryrightpositive. ff_h_pvs_keep_prefixentryrightpositive + S (dst_positive_keep_prefixentryright) = S ((S (dc_quotient_keep_prefixentry)) * dst_positive_scale_keep_prefixentryright)) /\ exists ff_q_pvs_keep_prefixentryrightpositive. dst_positive_code_keep_prefixentryright = ff_q_pvs_keep_prefixentryrightpositive * S ((S (dc_quotient_keep_prefixentry)) * dst_positive_scale_keep_prefixentryright) + (dst_positive_keep_prefixentryright))) /\ (((((exists ff_h_pvs_keep_prefixentryrightnegative. ff_h_pvs_keep_prefixentryrightnegative + S (dst_negative_keep_prefixentryright) = S ((S (dc_quotient_keep_prefixentry)) * dst_negative_scale_keep_prefixentryright)) /\ exists ff_q_pvs_keep_prefixentryrightnegative. dst_negative_code_keep_prefixentryright = ff_q_pvs_keep_prefixentryrightnegative * S ((S (dc_quotient_keep_prefixentry)) * dst_negative_scale_keep_prefixentryright) + (dst_negative_keep_prefixentryright))) /\ (exists ge_balance_positive_keep_prefixentryrightvalue ge_balance_negative_keep_prefixentryrightvalue. (((((dc_right_keep_prefixentry) = 2 * (ge_balance_positive_keep_prefixentryrightvalue) /\ (ge_balance_negative_keep_prefixentryrightvalue) = 0) \/ exists ge_signed_half_keep_prefixentryrightvaluedecode. (((dc_right_keep_prefixentry) = 2 * ge_signed_half_keep_prefixentryrightvaluedecode + 1 /\ (ge_balance_positive_keep_prefixentryrightvalue) = 0) /\ (ge_balance_negative_keep_prefixentryrightvalue) = S ge_signed_half_keep_prefixentryrightvaluedecode))) /\ ((dst_positive_keep_prefixentryright) + ge_balance_negative_keep_prefixentryrightvalue = (dst_negative_keep_prefixentryright) + ge_balance_positive_keep_prefixentryrightvalue))))))))) /\ (exists sto_ap_keep_prefixentryproduct sto_an_keep_prefixentryproduct sto_bp_keep_prefixentryproduct sto_bn_keep_prefixentryproduct sto_cp_keep_prefixentryproduct sto_cn_keep_prefixentryproduct. (((((dc_left_keep_prefixentry) = 2 * (sto_ap_keep_prefixentryproduct) /\ (sto_an_keep_prefixentryproduct) = 0) \/ exists ge_signed_half_keep_prefixentryproductleft. (((dc_left_keep_prefixentry) = 2 * ge_signed_half_keep_prefixentryproductleft + 1 /\ (sto_ap_keep_prefixentryproduct) = 0) /\ (sto_an_keep_prefixentryproduct) = S ge_signed_half_keep_prefixentryproductleft))) /\ ((((((dc_right_keep_prefixentry) = 2 * (sto_bp_keep_prefixentryproduct) /\ (sto_bn_keep_prefixentryproduct) = 0) \/ exists ge_signed_half_keep_prefixentryproductright. (((dc_right_keep_prefixentry) = 2 * ge_signed_half_keep_prefixentryproductright + 1 /\ (sto_bp_keep_prefixentryproduct) = 0) /\ (sto_bn_keep_prefixentryproduct) = S ge_signed_half_keep_prefixentryproductright))) /\ ((((((dc_value_keep_prefix) = 2 * (sto_cp_keep_prefixentryproduct) /\ (sto_cn_keep_prefixentryproduct) = 0) \/ exists ge_signed_half_keep_prefixentryproductoutput. (((dc_value_keep_prefix) = 2 * ge_signed_half_keep_prefixentryproductoutput + 1 /\ (sto_cp_keep_prefixentryproduct) = 0) /\ (sto_cn_keep_prefixentryproduct) = S ge_signed_half_keep_prefixentryproductoutput))) /\ ((sto_ap_keep_prefixentryproduct * sto_bp_keep_prefixentryproduct + sto_an_keep_prefixentryproduct * sto_bn_keep_prefixentryproduct) + sto_cn_keep_prefixentryproduct = (sto_ap_keep_prefixentryproduct * sto_bn_keep_prefixentryproduct + sto_an_keep_prefixentryproduct * sto_bp_keep_prefixentryproduct) + sto_cp_keep_prefixentryproduct))))))))))))))) \/ ((((dc_index_keep_prefix)=0 \/ ~(exists pvs_factor_keep_prefixentrynondivisor. (n) = (dc_index_keep_prefix) * pvs_factor_keep_prefixentrynondivisor)) /\ ((dc_value_keep_prefix)=0))))))) -> (exists pvs_le_gap_keep_bound. pvs_le_gap_keep_bound + (d) = (l)) -> ~(d=0) -> n=d*q -> (exists dst_positive_code_keep_left dst_positive_scale_keep_left dst_negative_code_keep_left dst_negative_scale_keep_left dst_positive_keep_left dst_negative_keep_left. (((F) = (((((dst_positive_code_keep_left) + (dst_positive_scale_keep_left)) * S ((dst_positive_code_keep_left) + (dst_positive_scale_keep_left)) + ((dst_positive_scale_keep_left) + (dst_positive_scale_keep_left))) + (((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) * S ((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) + ((dst_negative_scale_keep_left) + (dst_negative_scale_keep_left)))) * S ((((dst_positive_code_keep_left) + (dst_positive_scale_keep_left)) * S ((dst_positive_code_keep_left) + (dst_positive_scale_keep_left)) + ((dst_positive_scale_keep_left) + (dst_positive_scale_keep_left))) + (((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) * S ((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) + ((dst_negative_scale_keep_left) + (dst_negative_scale_keep_left)))) + ((((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) * S ((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) + ((dst_negative_scale_keep_left) + (dst_negative_scale_keep_left))) + (((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) * S ((dst_negative_code_keep_left) + (dst_negative_scale_keep_left)) + ((dst_negative_scale_keep_left) + (dst_negative_scale_keep_left)))))) /\ (((((exists ff_h_pvs_keep_leftpositive. ff_h_pvs_keep_leftpositive + S (dst_positive_keep_left) = S ((S (d)) * dst_positive_scale_keep_left)) /\ exists ff_q_pvs_keep_leftpositive. dst_positive_code_keep_left = ff_q_pvs_keep_leftpositive * S ((S (d)) * dst_positive_scale_keep_left) + (dst_positive_keep_left))) /\ (((((exists ff_h_pvs_keep_leftnegative. ff_h_pvs_keep_leftnegative + S (dst_negative_keep_left) = S ((S (d)) * dst_negative_scale_keep_left)) /\ exists ff_q_pvs_keep_leftnegative. dst_negative_code_keep_left = ff_q_pvs_keep_leftnegative * S ((S (d)) * dst_negative_scale_keep_left) + (dst_negative_keep_left))) /\ (exists ge_balance_positive_keep_leftvalue ge_balance_negative_keep_leftvalue. (((((a) = 2 * (ge_balance_positive_keep_leftvalue) /\ (ge_balance_negative_keep_leftvalue) = 0) \/ exists ge_signed_half_keep_leftvaluedecode. (((a) = 2 * ge_signed_half_keep_leftvaluedecode + 1 /\ (ge_balance_positive_keep_leftvalue) = 0) /\ (ge_balance_negative_keep_leftvalue) = S ge_signed_half_keep_leftvaluedecode))) /\ ((dst_positive_keep_left) + ge_balance_negative_keep_leftvalue = (dst_negative_keep_left) + ge_balance_positive_keep_leftvalue))))))))) -> (exists dst_positive_code_keep_right dst_positive_scale_keep_right dst_negative_code_keep_right dst_negative_scale_keep_right dst_positive_keep_right dst_negative_keep_right. (((G) = (((((dst_positive_code_keep_right) + (dst_positive_scale_keep_right)) * S ((dst_positive_code_keep_right) + (dst_positive_scale_keep_right)) + ((dst_positive_scale_keep_right) + (dst_positive_scale_keep_right))) + (((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) * S ((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) + ((dst_negative_scale_keep_right) + (dst_negative_scale_keep_right)))) * S ((((dst_positive_code_keep_right) + (dst_positive_scale_keep_right)) * S ((dst_positive_code_keep_right) + (dst_positive_scale_keep_right)) + ((dst_positive_scale_keep_right) + (dst_positive_scale_keep_right))) + (((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) * S ((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) + ((dst_negative_scale_keep_right) + (dst_negative_scale_keep_right)))) + ((((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) * S ((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) + ((dst_negative_scale_keep_right) + (dst_negative_scale_keep_right))) + (((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) * S ((dst_negative_code_keep_right) + (dst_negative_scale_keep_right)) + ((dst_negative_scale_keep_right) + (dst_negative_scale_keep_right)))))) /\ (((((exists ff_h_pvs_keep_rightpositive. ff_h_pvs_keep_rightpositive + S (dst_positive_keep_right) = S ((S (q)) * dst_positive_scale_keep_right)) /\ exists ff_q_pvs_keep_rightpositive. dst_positive_code_keep_right = ff_q_pvs_keep_rightpositive * S ((S (q)) * dst_positive_scale_keep_right) + (dst_positive_keep_right))) /\ (((((exists ff_h_pvs_keep_rightnegative. ff_h_pvs_keep_rightnegative + S (dst_negative_keep_right) = S ((S (q)) * dst_negative_scale_keep_right)) /\ exists ff_q_pvs_keep_rightnegative. dst_negative_code_keep_right = ff_q_pvs_keep_rightnegative * S ((S (q)) * dst_negative_scale_keep_right) + (dst_negative_keep_right))) /\ (exists ge_balance_positive_keep_rightvalue ge_balance_negative_keep_rightvalue. (((((b) = 2 * (ge_balance_positive_keep_rightvalue) /\ (ge_balance_negative_keep_rightvalue) = 0) \/ exists ge_signed_half_keep_rightvaluedecode. (((b) = 2 * ge_signed_half_keep_rightvaluedecode + 1 /\ (ge_balance_positive_keep_rightvalue) = 0) /\ (ge_balance_negative_keep_rightvalue) = S ge_signed_half_keep_rightvaluedecode))) /\ ((dst_positive_keep_right) + ge_balance_negative_keep_rightvalue = (dst_negative_keep_right) + ge_balance_positive_keep_rightvalue))))))))) -> (exists sto_ap_keep_product sto_an_keep_product sto_bp_keep_product sto_bn_keep_product sto_cp_keep_product sto_cn_keep_product. (((((a) = 2 * (sto_ap_keep_product) /\ (sto_an_keep_product) = 0) \/ exists ge_signed_half_keep_productleft. (((a) = 2 * ge_signed_half_keep_productleft + 1 /\ (sto_ap_keep_product) = 0) /\ (sto_an_keep_product) = S ge_signed_half_keep_productleft))) /\ ((((((b) = 2 * (sto_bp_keep_product) /\ (sto_bn_keep_product) = 0) \/ exists ge_signed_half_keep_productright. (((b) = 2 * ge_signed_half_keep_productright + 1 /\ (sto_bp_keep_product) = 0) /\ (sto_bn_keep_product) = S ge_signed_half_keep_productright))) /\ ((((((z) = 2 * (sto_cp_keep_product) /\ (sto_cn_keep_product) = 0) \/ exists ge_signed_half_keep_productoutput. (((z) = 2 * ge_signed_half_keep_productoutput + 1 /\ (sto_cp_keep_product) = 0) /\ (sto_cn_keep_product) = S ge_signed_half_keep_productoutput))) /\ ((sto_ap_keep_product * sto_bp_keep_product + sto_an_keep_product * sto_bn_keep_product) + sto_cn_keep_product = (sto_ap_keep_product * sto_bn_keep_product + sto_an_keep_product * sto_bp_keep_product) + sto_cp_keep_product))))))) -> (exists dst_positive_code_keep_result dst_positive_scale_keep_result dst_negative_code_keep_result dst_negative_scale_keep_result dst_positive_keep_result dst_negative_keep_result. (((M) = (((((dst_positive_code_keep_result) + (dst_positive_scale_keep_result)) * S ((dst_positive_code_keep_result) + (dst_positive_scale_keep_result)) + ((dst_positive_scale_keep_result) + (dst_positive_scale_keep_result))) + (((dst_negative_code_keep_result) + (dst_negative_scale_keep_result)) * S ((dst_negative_code_keep_result) + (dst_negative_scale_keep_result)) + ((dst_negative_scale_keep_result) + (dst_negative_scale_keep_result)))) * S ((((dst_positive_code_keep_result) + (dst_positive_scale_keep_result)) * S ((dst_positive_code_keep_result) + (dst_positive_scale_keep_result)) + ((dst_positive_scale_keep_result) + (dst_positive_scale_keep_result))) + (((dst_negative_code_keep_result) + (dst_negative_scale_keep_result)) * S ((dst_negative_code_keep_result) + (dst_negative_scale_keep_result)) + ((dst_negative_scale_keep_result) + (dst_negative_scale_keep_result)))) + ((((dst_negative_code_keep_result) + (dst_negative_scale_keep_result)) * S ((dst_negative_code_keep_result) + (dst_negative_scale_keep_result)) + ((dst_negative_scale_keep_result) + (dst_negative_scale_keep_result))) + (((dst_negative_code_keep_result) + (dst_negative_scale_keep_result)) * S ((dst_negative_code_keep_result) + (dst_negative_scale_keep_result)) + ((dst_negative_scale_keep_result) + (dst_negative_scale_keep_result)))))) /\ (((((exists ff_h_pvs_keep_resultpositive. ff_h_pvs_keep_resultpositive + S (dst_positive_keep_result) = S ((S (d)) * dst_positive_scale_keep_result)) /\ exists ff_q_pvs_keep_resultpositive. dst_positive_code_keep_result = ff_q_pvs_keep_resultpositive * S ((S (d)) * dst_positive_scale_keep_result) + (dst_positive_keep_result))) /\ (((((exists ff_h_pvs_keep_resultnegative. ff_h_pvs_keep_resultnegative + S (dst_negative_keep_result) = S ((S (d)) * dst_negative_scale_keep_result)) /\ exists ff_q_pvs_keep_resultnegative. dst_negative_code_keep_result = ff_q_pvs_keep_resultnegative * S ((S (d)) * dst_negative_scale_keep_result) + (dst_negative_keep_result))) /\ (exists ge_balance_positive_keep_resultvalue ge_balance_negative_keep_resultvalue. (((((z) = 2 * (ge_balance_positive_keep_resultvalue) /\ (ge_balance_negative_keep_resultvalue) = 0) \/ exists ge_signed_half_keep_resultvaluedecode. (((z) = 2 * ge_signed_half_keep_resultvaluedecode + 1 /\ (ge_balance_positive_keep_resultvalue) = 0) /\ (ge_balance_negative_keep_resultvalue) = S ge_signed_half_keep_resultvaluedecode))) /\ ((dst_positive_keep_result) + ge_balance_negative_keep_resultvalue = (dst_negative_keep_result) + ge_balance_positive_keep_resultvalue)))))))))

Complete tactic proof in conservative notation

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

56 script commands · 10 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 (2)
dirichlet convolution entry functionaldirichlet convolution entry from quotient
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 q
  8. L8
    intro a
  9. L9
    intro b
  10. L10
    intro z
02Fix variables and assumptionsL11–17

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

  1. L11
    intro hm
  2. L12
    intro hbound
  3. L13
    intro hd
  4. L14
    intro hq
  5. L15
    intro ha
  6. L16
    intro hb
  7. L17
    intro hz
03Separate the logical casesL18–18

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

  1. L18
    cases hm
04Establish huL19–25

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

  1. L19
    have hu : ∃ u. ArithAt(M,d,u)Definitions: ArithAt(M,d,u)Original native command in the exact edition
  2. L20
    specialize divisor_signed_table_lookup (l)
  3. L21
    specialize divisor_signed_table_lookup (M)
  4. L22
    specialize divisor_signed_table_lookup (d)
  5. L23
    apply divisor_signed_table_lookup
  6. L24
    exact hm_left
  7. L25
    exact hbound
05Separate the logical casesL26–26

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

  1. L26
    cases hu
06Establish heqL27–36

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

  1. L27
    have heq : x=z
  2. L28
    specialize dirichlet_convolution_entry_functional (F)
  3. L29
    specialize dirichlet_convolution_entry_functional (G)
  4. L30
    specialize dirichlet_convolution_entry_functional (n)
  5. L31
    specialize dirichlet_convolution_entry_functional (d)
  6. L32
    specialize dirichlet_convolution_entry_functional (x)
  7. L33
    specialize dirichlet_convolution_entry_functional (z)
  8. L34
    apply dirichlet_convolution_entry_functional
  9. L35
    specialize hm_right (d)
  10. L36
    specialize hm_right (x)
07Use earlier factsL37–46

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

  1. L37
    apply hm_right
  2. L38
    exact hbound
  3. L39
    exact hu_witness
  4. L40
    specialize dirichlet_convolution_entry_from_quotient (F)
  5. L41
    specialize dirichlet_convolution_entry_from_quotient (G)
  6. L42
    specialize dirichlet_convolution_entry_from_quotient (n)
  7. L43
    specialize dirichlet_convolution_entry_from_quotient (d)
  8. L44
    specialize dirichlet_convolution_entry_from_quotient (q)
  9. L45
    specialize dirichlet_convolution_entry_from_quotient (a)
  10. L46
    specialize dirichlet_convolution_entry_from_quotient (b)
08Use earlier factsL47–53

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

  1. L47
    specialize dirichlet_convolution_entry_from_quotient (z)
  2. L48
    apply dirichlet_convolution_entry_from_quotient
  3. L49
    exact hd
  4. L50
    exact hq
  5. L51
    exact ha
  6. L52
    exact hb
  7. L53
    exact hz
09Calculate and transport equalitiesL54–55

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

  1. L54
    rewrite heq at hu_witness
  2. L55
    rewrite heq at hu_witness
10Use earlier factsL56–56

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

  1. L56
    exact hu_witness

Library-wide reading audit

Original defined command ledger · 56 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro n
  4. 0004intro l
  5. 0005intro M
  6. 0006intro d
  7. 0007intro q
  8. 0008intro a
  9. 0009intro b
  10. 0010intro z
  11. 0011intro hm
  12. 0012intro hbound
  13. 0013intro hd
  14. 0014intro hq
  15. 0015intro ha
  16. 0016intro hb
  17. 0017intro hz
  18. 0018cases hm
  19. 0019have hu : ∃ u. ArithAt(M,d,u)
  20. 0020specialize divisor_signed_table_lookup (l)
  21. 0021specialize divisor_signed_table_lookup (M)
  22. 0022specialize divisor_signed_table_lookup (d)
  23. 0023apply divisor_signed_table_lookup
  24. 0024exact hm_left
  25. 0025exact hbound
  26. 0026cases hu
  27. 0027have heq : x=z
  28. 0028specialize dirichlet_convolution_entry_functional (F)
  29. 0029specialize dirichlet_convolution_entry_functional (G)
  30. 0030specialize dirichlet_convolution_entry_functional (n)
  31. 0031specialize dirichlet_convolution_entry_functional (d)
  32. 0032specialize dirichlet_convolution_entry_functional (x)
  33. 0033specialize dirichlet_convolution_entry_functional (z)
  34. 0034apply dirichlet_convolution_entry_functional
  35. 0035specialize hm_right (d)
  36. 0036specialize hm_right (x)
  37. 0037apply hm_right
  38. 0038exact hbound
  39. 0039exact hu_witness
  40. 0040specialize dirichlet_convolution_entry_from_quotient (F)
  41. 0041specialize dirichlet_convolution_entry_from_quotient (G)
  42. 0042specialize dirichlet_convolution_entry_from_quotient (n)
  43. 0043specialize dirichlet_convolution_entry_from_quotient (d)
  44. 0044specialize dirichlet_convolution_entry_from_quotient (q)
  45. 0045specialize dirichlet_convolution_entry_from_quotient (a)
  46. 0046specialize dirichlet_convolution_entry_from_quotient (b)
  47. 0047specialize dirichlet_convolution_entry_from_quotient (z)
  48. 0048apply dirichlet_convolution_entry_from_quotient
  49. 0049exact hd
  50. 0050exact hq
  51. 0051exact ha
  52. 0052exact hb
  53. 0053exact hz
  54. 0054rewrite heq at hu_witness
  55. 0055rewrite heq at hu_witness
  56. 0056exact hu_witness