DC000F

dirichlet_convolution_prefix_omitted_entry

The real prefix has zero at every omitted index, including zero, without any corresponding input-value condition.

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. DirichletPrefix(F,G,n,l,M) → Le(d,l) → d = 0 ∨ ¬Dvd(d,n) → ArithAt(M,d,0)

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

Definition DAG

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

Actual proof prerequisites

divisor_signed_table_lookup · checked external prerequisitedirichlet_convolution_entry_omitted_value
Original expanded first-order statement 
forall F G n l M d. (((exists dst_positive_code_omit_prefixtable dst_positive_scale_omit_prefixtable dst_negative_code_omit_prefixtable dst_negative_scale_omit_prefixtable. (((M) = (((((dst_positive_code_omit_prefixtable) + (dst_positive_scale_omit_prefixtable)) * S ((dst_positive_code_omit_prefixtable) + (dst_positive_scale_omit_prefixtable)) + ((dst_positive_scale_omit_prefixtable) + (dst_positive_scale_omit_prefixtable))) + (((dst_negative_code_omit_prefixtable) + (dst_negative_scale_omit_prefixtable)) * S ((dst_negative_code_omit_prefixtable) + (dst_negative_scale_omit_prefixtable)) + ((dst_negative_scale_omit_prefixtable) + (dst_negative_scale_omit_prefixtable)))) * S ((((dst_positive_code_omit_prefixtable) + (dst_positive_scale_omit_prefixtable)) * S ((dst_positive_code_omit_prefixtable) + (dst_positive_scale_omit_prefixtable)) + ((dst_positive_scale_omit_prefixtable) + (dst_positive_scale_omit_prefixtable))) + (((dst_negative_code_omit_prefixtable) + (dst_negative_scale_omit_prefixtable)) * S ((dst_negative_code_omit_prefixtable) + (dst_negative_scale_omit_prefixtable)) + ((dst_negative_scale_omit_prefixtable) + (dst_negative_scale_omit_prefixtable)))) + ((((dst_negative_code_omit_prefixtable) + (dst_negative_scale_omit_prefixtable)) * S ((dst_negative_code_omit_prefixtable) + (dst_negative_scale_omit_prefixtable)) + ((dst_negative_scale_omit_prefixtable) + (dst_negative_scale_omit_prefixtable))) + (((dst_negative_code_omit_prefixtable) + (dst_negative_scale_omit_prefixtable)) * S ((dst_negative_code_omit_prefixtable) + (dst_negative_scale_omit_prefixtable)) + ((dst_negative_scale_omit_prefixtable) + (dst_negative_scale_omit_prefixtable)))))) /\ (forall dst_index_omit_prefixtable. (exists pvs_le_gap_omit_prefixtabledomain. pvs_le_gap_omit_prefixtabledomain + (dst_index_omit_prefixtable) = (l)) -> exists dst_positive_omit_prefixtable dst_negative_omit_prefixtable dst_value_omit_prefixtable. ((((exists ff_h_pvs_omit_prefixtableentrypositive. ff_h_pvs_omit_prefixtableentrypositive + S (dst_positive_omit_prefixtable) = S ((S (dst_index_omit_prefixtable)) * dst_positive_scale_omit_prefixtable)) /\ exists ff_q_pvs_omit_prefixtableentrypositive. dst_positive_code_omit_prefixtable = ff_q_pvs_omit_prefixtableentrypositive * S ((S (dst_index_omit_prefixtable)) * dst_positive_scale_omit_prefixtable) + (dst_positive_omit_prefixtable))) /\ (((((exists ff_h_pvs_omit_prefixtableentrynegative. ff_h_pvs_omit_prefixtableentrynegative + S (dst_negative_omit_prefixtable) = S ((S (dst_index_omit_prefixtable)) * dst_negative_scale_omit_prefixtable)) /\ exists ff_q_pvs_omit_prefixtableentrynegative. dst_negative_code_omit_prefixtable = ff_q_pvs_omit_prefixtableentrynegative * S ((S (dst_index_omit_prefixtable)) * dst_negative_scale_omit_prefixtable) + (dst_negative_omit_prefixtable))) /\ (exists ge_balance_positive_omit_prefixtableentryvalue ge_balance_negative_omit_prefixtableentryvalue. (((((dst_value_omit_prefixtable) = 2 * (ge_balance_positive_omit_prefixtableentryvalue) /\ (ge_balance_negative_omit_prefixtableentryvalue) = 0) \/ exists ge_signed_half_omit_prefixtableentryvaluedecode. (((dst_value_omit_prefixtable) = 2 * ge_signed_half_omit_prefixtableentryvaluedecode + 1 /\ (ge_balance_positive_omit_prefixtableentryvalue) = 0) /\ (ge_balance_negative_omit_prefixtableentryvalue) = S ge_signed_half_omit_prefixtableentryvaluedecode))) /\ ((dst_positive_omit_prefixtable) + ge_balance_negative_omit_prefixtableentryvalue = (dst_negative_omit_prefixtable) + ge_balance_positive_omit_prefixtableentryvalue))))))))) /\ (forall dc_index_omit_prefix dc_value_omit_prefix. (exists pvs_le_gap_omit_prefixdomain. pvs_le_gap_omit_prefixdomain + (dc_index_omit_prefix) = (l)) -> (exists dst_positive_code_omit_prefixlookup dst_positive_scale_omit_prefixlookup dst_negative_code_omit_prefixlookup dst_negative_scale_omit_prefixlookup dst_positive_omit_prefixlookup dst_negative_omit_prefixlookup. (((M) = (((((dst_positive_code_omit_prefixlookup) + (dst_positive_scale_omit_prefixlookup)) * S ((dst_positive_code_omit_prefixlookup) + (dst_positive_scale_omit_prefixlookup)) + ((dst_positive_scale_omit_prefixlookup) + (dst_positive_scale_omit_prefixlookup))) + (((dst_negative_code_omit_prefixlookup) + (dst_negative_scale_omit_prefixlookup)) * S ((dst_negative_code_omit_prefixlookup) + (dst_negative_scale_omit_prefixlookup)) + ((dst_negative_scale_omit_prefixlookup) + (dst_negative_scale_omit_prefixlookup)))) * S ((((dst_positive_code_omit_prefixlookup) + (dst_positive_scale_omit_prefixlookup)) * S ((dst_positive_code_omit_prefixlookup) + (dst_positive_scale_omit_prefixlookup)) + ((dst_positive_scale_omit_prefixlookup) + (dst_positive_scale_omit_prefixlookup))) + (((dst_negative_code_omit_prefixlookup) + (dst_negative_scale_omit_prefixlookup)) * S ((dst_negative_code_omit_prefixlookup) + (dst_negative_scale_omit_prefixlookup)) + ((dst_negative_scale_omit_prefixlookup) + (dst_negative_scale_omit_prefixlookup)))) + ((((dst_negative_code_omit_prefixlookup) + (dst_negative_scale_omit_prefixlookup)) * S ((dst_negative_code_omit_prefixlookup) + (dst_negative_scale_omit_prefixlookup)) + ((dst_negative_scale_omit_prefixlookup) + (dst_negative_scale_omit_prefixlookup))) + (((dst_negative_code_omit_prefixlookup) + (dst_negative_scale_omit_prefixlookup)) * S ((dst_negative_code_omit_prefixlookup) + (dst_negative_scale_omit_prefixlookup)) + ((dst_negative_scale_omit_prefixlookup) + (dst_negative_scale_omit_prefixlookup)))))) /\ (((((exists ff_h_pvs_omit_prefixlookuppositive. ff_h_pvs_omit_prefixlookuppositive + S (dst_positive_omit_prefixlookup) = S ((S (dc_index_omit_prefix)) * dst_positive_scale_omit_prefixlookup)) /\ exists ff_q_pvs_omit_prefixlookuppositive. dst_positive_code_omit_prefixlookup = ff_q_pvs_omit_prefixlookuppositive * S ((S (dc_index_omit_prefix)) * dst_positive_scale_omit_prefixlookup) + (dst_positive_omit_prefixlookup))) /\ (((((exists ff_h_pvs_omit_prefixlookupnegative. ff_h_pvs_omit_prefixlookupnegative + S (dst_negative_omit_prefixlookup) = S ((S (dc_index_omit_prefix)) * dst_negative_scale_omit_prefixlookup)) /\ exists ff_q_pvs_omit_prefixlookupnegative. dst_negative_code_omit_prefixlookup = ff_q_pvs_omit_prefixlookupnegative * S ((S (dc_index_omit_prefix)) * dst_negative_scale_omit_prefixlookup) + (dst_negative_omit_prefixlookup))) /\ (exists ge_balance_positive_omit_prefixlookupvalue ge_balance_negative_omit_prefixlookupvalue. (((((dc_value_omit_prefix) = 2 * (ge_balance_positive_omit_prefixlookupvalue) /\ (ge_balance_negative_omit_prefixlookupvalue) = 0) \/ exists ge_signed_half_omit_prefixlookupvaluedecode. (((dc_value_omit_prefix) = 2 * ge_signed_half_omit_prefixlookupvaluedecode + 1 /\ (ge_balance_positive_omit_prefixlookupvalue) = 0) /\ (ge_balance_negative_omit_prefixlookupvalue) = S ge_signed_half_omit_prefixlookupvaluedecode))) /\ ((dst_positive_omit_prefixlookup) + ge_balance_negative_omit_prefixlookupvalue = (dst_negative_omit_prefixlookup) + ge_balance_positive_omit_prefixlookupvalue))))))))) -> ((((~((dc_index_omit_prefix)=0)) /\ (exists dc_quotient_omit_prefixentry dc_left_omit_prefixentry dc_right_omit_prefixentry. (((n)=(dc_index_omit_prefix)*dc_quotient_omit_prefixentry) /\ (((exists dst_positive_code_omit_prefixentryleft dst_positive_scale_omit_prefixentryleft dst_negative_code_omit_prefixentryleft dst_negative_scale_omit_prefixentryleft dst_positive_omit_prefixentryleft dst_negative_omit_prefixentryleft. (((F) = (((((dst_positive_code_omit_prefixentryleft) + (dst_positive_scale_omit_prefixentryleft)) * S ((dst_positive_code_omit_prefixentryleft) + (dst_positive_scale_omit_prefixentryleft)) + ((dst_positive_scale_omit_prefixentryleft) + (dst_positive_scale_omit_prefixentryleft))) + (((dst_negative_code_omit_prefixentryleft) + (dst_negative_scale_omit_prefixentryleft)) * S ((dst_negative_code_omit_prefixentryleft) + (dst_negative_scale_omit_prefixentryleft)) + ((dst_negative_scale_omit_prefixentryleft) + (dst_negative_scale_omit_prefixentryleft)))) * S ((((dst_positive_code_omit_prefixentryleft) + (dst_positive_scale_omit_prefixentryleft)) * S ((dst_positive_code_omit_prefixentryleft) + (dst_positive_scale_omit_prefixentryleft)) + ((dst_positive_scale_omit_prefixentryleft) + (dst_positive_scale_omit_prefixentryleft))) + (((dst_negative_code_omit_prefixentryleft) + (dst_negative_scale_omit_prefixentryleft)) * S ((dst_negative_code_omit_prefixentryleft) + (dst_negative_scale_omit_prefixentryleft)) + ((dst_negative_scale_omit_prefixentryleft) + (dst_negative_scale_omit_prefixentryleft)))) + ((((dst_negative_code_omit_prefixentryleft) + (dst_negative_scale_omit_prefixentryleft)) * S ((dst_negative_code_omit_prefixentryleft) + (dst_negative_scale_omit_prefixentryleft)) + ((dst_negative_scale_omit_prefixentryleft) + (dst_negative_scale_omit_prefixentryleft))) + (((dst_negative_code_omit_prefixentryleft) + (dst_negative_scale_omit_prefixentryleft)) * S ((dst_negative_code_omit_prefixentryleft) + (dst_negative_scale_omit_prefixentryleft)) + ((dst_negative_scale_omit_prefixentryleft) + (dst_negative_scale_omit_prefixentryleft)))))) /\ (((((exists ff_h_pvs_omit_prefixentryleftpositive. ff_h_pvs_omit_prefixentryleftpositive + S (dst_positive_omit_prefixentryleft) = S ((S (dc_index_omit_prefix)) * dst_positive_scale_omit_prefixentryleft)) /\ exists ff_q_pvs_omit_prefixentryleftpositive. dst_positive_code_omit_prefixentryleft = ff_q_pvs_omit_prefixentryleftpositive * S ((S (dc_index_omit_prefix)) * dst_positive_scale_omit_prefixentryleft) + (dst_positive_omit_prefixentryleft))) /\ (((((exists ff_h_pvs_omit_prefixentryleftnegative. ff_h_pvs_omit_prefixentryleftnegative + S (dst_negative_omit_prefixentryleft) = S ((S (dc_index_omit_prefix)) * dst_negative_scale_omit_prefixentryleft)) /\ exists ff_q_pvs_omit_prefixentryleftnegative. dst_negative_code_omit_prefixentryleft = ff_q_pvs_omit_prefixentryleftnegative * S ((S (dc_index_omit_prefix)) * dst_negative_scale_omit_prefixentryleft) + (dst_negative_omit_prefixentryleft))) /\ (exists ge_balance_positive_omit_prefixentryleftvalue ge_balance_negative_omit_prefixentryleftvalue. (((((dc_left_omit_prefixentry) = 2 * (ge_balance_positive_omit_prefixentryleftvalue) /\ (ge_balance_negative_omit_prefixentryleftvalue) = 0) \/ exists ge_signed_half_omit_prefixentryleftvaluedecode. (((dc_left_omit_prefixentry) = 2 * ge_signed_half_omit_prefixentryleftvaluedecode + 1 /\ (ge_balance_positive_omit_prefixentryleftvalue) = 0) /\ (ge_balance_negative_omit_prefixentryleftvalue) = S ge_signed_half_omit_prefixentryleftvaluedecode))) /\ ((dst_positive_omit_prefixentryleft) + ge_balance_negative_omit_prefixentryleftvalue = (dst_negative_omit_prefixentryleft) + ge_balance_positive_omit_prefixentryleftvalue))))))))) /\ (((exists dst_positive_code_omit_prefixentryright dst_positive_scale_omit_prefixentryright dst_negative_code_omit_prefixentryright dst_negative_scale_omit_prefixentryright dst_positive_omit_prefixentryright dst_negative_omit_prefixentryright. (((G) = (((((dst_positive_code_omit_prefixentryright) + (dst_positive_scale_omit_prefixentryright)) * S ((dst_positive_code_omit_prefixentryright) + (dst_positive_scale_omit_prefixentryright)) + ((dst_positive_scale_omit_prefixentryright) + (dst_positive_scale_omit_prefixentryright))) + (((dst_negative_code_omit_prefixentryright) + (dst_negative_scale_omit_prefixentryright)) * S ((dst_negative_code_omit_prefixentryright) + (dst_negative_scale_omit_prefixentryright)) + ((dst_negative_scale_omit_prefixentryright) + (dst_negative_scale_omit_prefixentryright)))) * S ((((dst_positive_code_omit_prefixentryright) + (dst_positive_scale_omit_prefixentryright)) * S ((dst_positive_code_omit_prefixentryright) + (dst_positive_scale_omit_prefixentryright)) + ((dst_positive_scale_omit_prefixentryright) + (dst_positive_scale_omit_prefixentryright))) + (((dst_negative_code_omit_prefixentryright) + (dst_negative_scale_omit_prefixentryright)) * S ((dst_negative_code_omit_prefixentryright) + (dst_negative_scale_omit_prefixentryright)) + ((dst_negative_scale_omit_prefixentryright) + (dst_negative_scale_omit_prefixentryright)))) + ((((dst_negative_code_omit_prefixentryright) + (dst_negative_scale_omit_prefixentryright)) * S ((dst_negative_code_omit_prefixentryright) + (dst_negative_scale_omit_prefixentryright)) + ((dst_negative_scale_omit_prefixentryright) + (dst_negative_scale_omit_prefixentryright))) + (((dst_negative_code_omit_prefixentryright) + (dst_negative_scale_omit_prefixentryright)) * S ((dst_negative_code_omit_prefixentryright) + (dst_negative_scale_omit_prefixentryright)) + ((dst_negative_scale_omit_prefixentryright) + (dst_negative_scale_omit_prefixentryright)))))) /\ (((((exists ff_h_pvs_omit_prefixentryrightpositive. ff_h_pvs_omit_prefixentryrightpositive + S (dst_positive_omit_prefixentryright) = S ((S (dc_quotient_omit_prefixentry)) * dst_positive_scale_omit_prefixentryright)) /\ exists ff_q_pvs_omit_prefixentryrightpositive. dst_positive_code_omit_prefixentryright = ff_q_pvs_omit_prefixentryrightpositive * S ((S (dc_quotient_omit_prefixentry)) * dst_positive_scale_omit_prefixentryright) + (dst_positive_omit_prefixentryright))) /\ (((((exists ff_h_pvs_omit_prefixentryrightnegative. ff_h_pvs_omit_prefixentryrightnegative + S (dst_negative_omit_prefixentryright) = S ((S (dc_quotient_omit_prefixentry)) * dst_negative_scale_omit_prefixentryright)) /\ exists ff_q_pvs_omit_prefixentryrightnegative. dst_negative_code_omit_prefixentryright = ff_q_pvs_omit_prefixentryrightnegative * S ((S (dc_quotient_omit_prefixentry)) * dst_negative_scale_omit_prefixentryright) + (dst_negative_omit_prefixentryright))) /\ (exists ge_balance_positive_omit_prefixentryrightvalue ge_balance_negative_omit_prefixentryrightvalue. (((((dc_right_omit_prefixentry) = 2 * (ge_balance_positive_omit_prefixentryrightvalue) /\ (ge_balance_negative_omit_prefixentryrightvalue) = 0) \/ exists ge_signed_half_omit_prefixentryrightvaluedecode. (((dc_right_omit_prefixentry) = 2 * ge_signed_half_omit_prefixentryrightvaluedecode + 1 /\ (ge_balance_positive_omit_prefixentryrightvalue) = 0) /\ (ge_balance_negative_omit_prefixentryrightvalue) = S ge_signed_half_omit_prefixentryrightvaluedecode))) /\ ((dst_positive_omit_prefixentryright) + ge_balance_negative_omit_prefixentryrightvalue = (dst_negative_omit_prefixentryright) + ge_balance_positive_omit_prefixentryrightvalue))))))))) /\ (exists sto_ap_omit_prefixentryproduct sto_an_omit_prefixentryproduct sto_bp_omit_prefixentryproduct sto_bn_omit_prefixentryproduct sto_cp_omit_prefixentryproduct sto_cn_omit_prefixentryproduct. (((((dc_left_omit_prefixentry) = 2 * (sto_ap_omit_prefixentryproduct) /\ (sto_an_omit_prefixentryproduct) = 0) \/ exists ge_signed_half_omit_prefixentryproductleft. (((dc_left_omit_prefixentry) = 2 * ge_signed_half_omit_prefixentryproductleft + 1 /\ (sto_ap_omit_prefixentryproduct) = 0) /\ (sto_an_omit_prefixentryproduct) = S ge_signed_half_omit_prefixentryproductleft))) /\ ((((((dc_right_omit_prefixentry) = 2 * (sto_bp_omit_prefixentryproduct) /\ (sto_bn_omit_prefixentryproduct) = 0) \/ exists ge_signed_half_omit_prefixentryproductright. (((dc_right_omit_prefixentry) = 2 * ge_signed_half_omit_prefixentryproductright + 1 /\ (sto_bp_omit_prefixentryproduct) = 0) /\ (sto_bn_omit_prefixentryproduct) = S ge_signed_half_omit_prefixentryproductright))) /\ ((((((dc_value_omit_prefix) = 2 * (sto_cp_omit_prefixentryproduct) /\ (sto_cn_omit_prefixentryproduct) = 0) \/ exists ge_signed_half_omit_prefixentryproductoutput. (((dc_value_omit_prefix) = 2 * ge_signed_half_omit_prefixentryproductoutput + 1 /\ (sto_cp_omit_prefixentryproduct) = 0) /\ (sto_cn_omit_prefixentryproduct) = S ge_signed_half_omit_prefixentryproductoutput))) /\ ((sto_ap_omit_prefixentryproduct * sto_bp_omit_prefixentryproduct + sto_an_omit_prefixentryproduct * sto_bn_omit_prefixentryproduct) + sto_cn_omit_prefixentryproduct = (sto_ap_omit_prefixentryproduct * sto_bn_omit_prefixentryproduct + sto_an_omit_prefixentryproduct * sto_bp_omit_prefixentryproduct) + sto_cp_omit_prefixentryproduct))))))))))))))) \/ ((((dc_index_omit_prefix)=0 \/ ~(exists pvs_factor_omit_prefixentrynondivisor. (n) = (dc_index_omit_prefix) * pvs_factor_omit_prefixentrynondivisor)) /\ ((dc_value_omit_prefix)=0))))))) -> (exists pvs_le_gap_omit_bound. pvs_le_gap_omit_bound + (d) = (l)) -> (d=0 \/ ~(exists pvs_factor_omit_reason. (n) = (d) * pvs_factor_omit_reason)) -> (exists dst_positive_code_omit_result dst_positive_scale_omit_result dst_negative_code_omit_result dst_negative_scale_omit_result dst_positive_omit_result dst_negative_omit_result. (((M) = (((((dst_positive_code_omit_result) + (dst_positive_scale_omit_result)) * S ((dst_positive_code_omit_result) + (dst_positive_scale_omit_result)) + ((dst_positive_scale_omit_result) + (dst_positive_scale_omit_result))) + (((dst_negative_code_omit_result) + (dst_negative_scale_omit_result)) * S ((dst_negative_code_omit_result) + (dst_negative_scale_omit_result)) + ((dst_negative_scale_omit_result) + (dst_negative_scale_omit_result)))) * S ((((dst_positive_code_omit_result) + (dst_positive_scale_omit_result)) * S ((dst_positive_code_omit_result) + (dst_positive_scale_omit_result)) + ((dst_positive_scale_omit_result) + (dst_positive_scale_omit_result))) + (((dst_negative_code_omit_result) + (dst_negative_scale_omit_result)) * S ((dst_negative_code_omit_result) + (dst_negative_scale_omit_result)) + ((dst_negative_scale_omit_result) + (dst_negative_scale_omit_result)))) + ((((dst_negative_code_omit_result) + (dst_negative_scale_omit_result)) * S ((dst_negative_code_omit_result) + (dst_negative_scale_omit_result)) + ((dst_negative_scale_omit_result) + (dst_negative_scale_omit_result))) + (((dst_negative_code_omit_result) + (dst_negative_scale_omit_result)) * S ((dst_negative_code_omit_result) + (dst_negative_scale_omit_result)) + ((dst_negative_scale_omit_result) + (dst_negative_scale_omit_result)))))) /\ (((((exists ff_h_pvs_omit_resultpositive. ff_h_pvs_omit_resultpositive + S (dst_positive_omit_result) = S ((S (d)) * dst_positive_scale_omit_result)) /\ exists ff_q_pvs_omit_resultpositive. dst_positive_code_omit_result = ff_q_pvs_omit_resultpositive * S ((S (d)) * dst_positive_scale_omit_result) + (dst_positive_omit_result))) /\ (((((exists ff_h_pvs_omit_resultnegative. ff_h_pvs_omit_resultnegative + S (dst_negative_omit_result) = S ((S (d)) * dst_negative_scale_omit_result)) /\ exists ff_q_pvs_omit_resultnegative. dst_negative_code_omit_result = ff_q_pvs_omit_resultnegative * S ((S (d)) * dst_negative_scale_omit_result) + (dst_negative_omit_result))) /\ (exists ge_balance_positive_omit_resultvalue ge_balance_negative_omit_resultvalue. (((((0) = 2 * (ge_balance_positive_omit_resultvalue) /\ (ge_balance_negative_omit_resultvalue) = 0) \/ exists ge_signed_half_omit_resultvaluedecode. (((0) = 2 * ge_signed_half_omit_resultvaluedecode + 1 /\ (ge_balance_positive_omit_resultvalue) = 0) /\ (ge_balance_negative_omit_resultvalue) = S ge_signed_half_omit_resultvaluedecode))) /\ ((dst_positive_omit_result) + ge_balance_negative_omit_resultvalue = (dst_negative_omit_result) + ge_balance_positive_omit_resultvalue)))))))))

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 · 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 omitted value
01Fix variables and assumptionsL1–9

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 hm
  8. L8
    intro hbound
  9. L9
    intro hc
02Separate the logical casesL10–10

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

  1. L10
    cases hm
03Establish huL11–17

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

  1. L11
    have hu : ∃ u. ArithAt(M,d,u)Definitions: ArithAt(M,d,u)Original native command in the exact edition
  2. L12
    specialize divisor_signed_table_lookup (l)
  3. L13
    specialize divisor_signed_table_lookup (M)
  4. L14
    specialize divisor_signed_table_lookup (d)
  5. L15
    apply divisor_signed_table_lookup
  6. L16
    exact hm_left
  7. L17
    exact hbound
04Separate the logical casesL18–18

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

  1. L18
    cases hu
05Establish heqL19–28

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

  1. L19
    have heq : x=0
  2. L20
    specialize dirichlet_convolution_entry_omitted_value (F)
  3. L21
    specialize dirichlet_convolution_entry_omitted_value (G)
  4. L22
    specialize dirichlet_convolution_entry_omitted_value (n)
  5. L23
    specialize dirichlet_convolution_entry_omitted_value (d)
  6. L24
    specialize dirichlet_convolution_entry_omitted_value (x)
  7. L25
    apply dirichlet_convolution_entry_omitted_value
  8. L26
    exact hc
  9. L27
    specialize hm_right (d)
  10. L28
    specialize hm_right (x)
06Use earlier factsL29–31

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

  1. L29
    apply hm_right
  2. L30
    exact hbound
  3. L31
    exact hu_witness
07Calculate and transport equalitiesL32–33

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

  1. L32
    rewrite heq at hu_witness
  2. L33
    rewrite heq at hu_witness
08Use earlier factsL34–34

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

  1. L34
    exact hu_witness

Library-wide reading audit

Original defined command ledger · 34 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro n
  4. 0004intro l
  5. 0005intro M
  6. 0006intro d
  7. 0007intro hm
  8. 0008intro hbound
  9. 0009intro hc
  10. 0010cases hm
  11. 0011have hu : ∃ u. ArithAt(M,d,u)
  12. 0012specialize divisor_signed_table_lookup (l)
  13. 0013specialize divisor_signed_table_lookup (M)
  14. 0014specialize divisor_signed_table_lookup (d)
  15. 0015apply divisor_signed_table_lookup
  16. 0016exact hm_left
  17. 0017exact hbound
  18. 0018cases hu
  19. 0019have heq : x=0
  20. 0020specialize dirichlet_convolution_entry_omitted_value (F)
  21. 0021specialize dirichlet_convolution_entry_omitted_value (G)
  22. 0022specialize dirichlet_convolution_entry_omitted_value (n)
  23. 0023specialize dirichlet_convolution_entry_omitted_value (d)
  24. 0024specialize dirichlet_convolution_entry_omitted_value (x)
  25. 0025apply dirichlet_convolution_entry_omitted_value
  26. 0026exact hc
  27. 0027specialize hm_right (d)
  28. 0028specialize hm_right (x)
  29. 0029apply hm_right
  30. 0030exact hbound
  31. 0031exact hu_witness
  32. 0032rewrite heq at hu_witness
  33. 0033rewrite heq at hu_witness
  34. 0034exact hu_witness