DC000F

dirichlet_convolution_prefix_omitted_entry

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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

Exact expanded first-order arithmetic statement

forall F G n l M 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)))))))))

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

divisor_signed_table_lookup Alpha theorem; checked-use authorized DC0004 dirichlet_convolution_entry_omitted_value

Direct dependents

none

Formal native tactic body

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

Read the argument

Proof checkpoints

34 script commands · 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.

Named ingredients (1)
dirichlet convolution entry omitted value

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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
  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 exact 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 : exists u. (exists dst_positive_code_omit_actual_lookup dst_positive_scale_omit_actual_lookup dst_negative_code_omit_actual_lookup dst_negative_scale_omit_actual_lookup dst_positive_omit_actual_lookup dst_negative_omit_actual_lookup. (((M) = (((((dst_positive_code_omit_actual_lookup) + (dst_positive_scale_omit_actual_lookup)) * S ((dst_positive_code_omit_actual_lookup) + (dst_positive_scale_omit_actual_lookup)) + ((dst_positive_scale_omit_actual_lookup) + (dst_positive_scale_omit_actual_lookup))) + (((dst_negative_code_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup)) * S ((dst_negative_code_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup)) + ((dst_negative_scale_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup)))) * S ((((dst_positive_code_omit_actual_lookup) + (dst_positive_scale_omit_actual_lookup)) * S ((dst_positive_code_omit_actual_lookup) + (dst_positive_scale_omit_actual_lookup)) + ((dst_positive_scale_omit_actual_lookup) + (dst_positive_scale_omit_actual_lookup))) + (((dst_negative_code_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup)) * S ((dst_negative_code_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup)) + ((dst_negative_scale_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup)))) + ((((dst_negative_code_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup)) * S ((dst_negative_code_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup)) + ((dst_negative_scale_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup))) + (((dst_negative_code_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup)) * S ((dst_negative_code_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup)) + ((dst_negative_scale_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup)))))) /\ (((((exists ff_h_pvs_omit_actual_lookuppositive. ff_h_pvs_omit_actual_lookuppositive + S (dst_positive_omit_actual_lookup) = S ((S (d)) * dst_positive_scale_omit_actual_lookup)) /\ exists ff_q_pvs_omit_actual_lookuppositive. dst_positive_code_omit_actual_lookup = ff_q_pvs_omit_actual_lookuppositive * S ((S (d)) * dst_positive_scale_omit_actual_lookup) + (dst_positive_omit_actual_lookup))) /\ (((((exists ff_h_pvs_omit_actual_lookupnegative. ff_h_pvs_omit_actual_lookupnegative + S (dst_negative_omit_actual_lookup) = S ((S (d)) * dst_negative_scale_omit_actual_lookup)) /\ exists ff_q_pvs_omit_actual_lookupnegative. dst_negative_code_omit_actual_lookup = ff_q_pvs_omit_actual_lookupnegative * S ((S (d)) * dst_negative_scale_omit_actual_lookup) + (dst_negative_omit_actual_lookup))) /\ (exists ge_balance_positive_omit_actual_lookupvalue ge_balance_negative_omit_actual_lookupvalue. (((((u) = 2 * (ge_balance_positive_omit_actual_lookupvalue) /\ (ge_balance_negative_omit_actual_lookupvalue) = 0) \/ exists ge_signed_half_omit_actual_lookupvaluedecode. (((u) = 2 * ge_signed_half_omit_actual_lookupvaluedecode + 1 /\ (ge_balance_positive_omit_actual_lookupvalue) = 0) /\ (ge_balance_negative_omit_actual_lookupvalue) = S ge_signed_half_omit_actual_lookupvaluedecode))) /\ ((dst_positive_omit_actual_lookup) + ge_balance_negative_omit_actual_lookupvalue = (dst_negative_omit_actual_lookup) + ge_balance_positive_omit_actual_lookupvalue)))))))))
  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