DC0003 — dirichlet_convolution_entry_from_nondivisor

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. ∀ d. ¬Dvd(d,n) → DirichletEntry(F,G,n,d,0)

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

Definition DAG

DirichletEntry(F,G,n,d,z) · 1 Dvd(d,n) · 1

Actual proof prerequisites

none

Original expanded first-order statement

forall F G n d. ~(exists pvs_factor_omit_guard. (n) = (d) * pvs_factor_omit_guard) -> ((((~((d)=0)) /\ (exists dc_quotient_omit_result dc_left_omit_result dc_right_omit_result. (((n)=(d)*dc_quotient_omit_result) /\ (((exists dst_positive_code_omit_resultleft dst_positive_scale_omit_resultleft dst_negative_code_omit_resultleft dst_negative_scale_omit_resultleft dst_positive_omit_resultleft dst_negative_omit_resultleft. (((F) = (((((dst_positive_code_omit_resultleft) + (dst_positive_scale_omit_resultleft)) * S ((dst_positive_code_omit_resultleft) + (dst_positive_scale_omit_resultleft)) + ((dst_positive_scale_omit_resultleft) + (dst_positive_scale_omit_resultleft))) + (((dst_negative_code_omit_resultleft) + (dst_negative_scale_omit_resultleft)) * S ((dst_negative_code_omit_resultleft) + (dst_negative_scale_omit_resultleft)) + ((dst_negative_scale_omit_resultleft) + (dst_negative_scale_omit_resultleft)))) * S ((((dst_positive_code_omit_resultleft) + (dst_positive_scale_omit_resultleft)) * S ((dst_positive_code_omit_resultleft) + (dst_positive_scale_omit_resultleft)) + ((dst_positive_scale_omit_resultleft) + (dst_positive_scale_omit_resultleft))) + (((dst_negative_code_omit_resultleft) + (dst_negative_scale_omit_resultleft)) * S ((dst_negative_code_omit_resultleft) + (dst_negative_scale_omit_resultleft)) + ((dst_negative_scale_omit_resultleft) + (dst_negative_scale_omit_resultleft)))) + ((((dst_negative_code_omit_resultleft) + (dst_negative_scale_omit_resultleft)) * S ((dst_negative_code_omit_resultleft) + (dst_negative_scale_omit_resultleft)) + ((dst_negative_scale_omit_resultleft) + (dst_negative_scale_omit_resultleft))) + (((dst_negative_code_omit_resultleft) + (dst_negative_scale_omit_resultleft)) * S ((dst_negative_code_omit_resultleft) + (dst_negative_scale_omit_resultleft)) + ((dst_negative_scale_omit_resultleft) + (dst_negative_scale_omit_resultleft)))))) /\ (((((exists ff_h_pvs_omit_resultleftpositive. ff_h_pvs_omit_resultleftpositive + S (dst_positive_omit_resultleft) = S ((S (d)) * dst_positive_scale_omit_resultleft)) /\ exists ff_q_pvs_omit_resultleftpositive. dst_positive_code_omit_resultleft = ff_q_pvs_omit_resultleftpositive * S ((S (d)) * dst_positive_scale_omit_resultleft) + (dst_positive_omit_resultleft))) /\ (((((exists ff_h_pvs_omit_resultleftnegative. ff_h_pvs_omit_resultleftnegative + S (dst_negative_omit_resultleft) = S ((S (d)) * dst_negative_scale_omit_resultleft)) /\ exists ff_q_pvs_omit_resultleftnegative. dst_negative_code_omit_resultleft = ff_q_pvs_omit_resultleftnegative * S ((S (d)) * dst_negative_scale_omit_resultleft) + (dst_negative_omit_resultleft))) /\ (exists ge_balance_positive_omit_resultleftvalue ge_balance_negative_omit_resultleftvalue. (((((dc_left_omit_result) = 2 * (ge_balance_positive_omit_resultleftvalue) /\ (ge_balance_negative_omit_resultleftvalue) = 0) \/ exists ge_signed_half_omit_resultleftvaluedecode. (((dc_left_omit_result) = 2 * ge_signed_half_omit_resultleftvaluedecode + 1 /\ (ge_balance_positive_omit_resultleftvalue) = 0) /\ (ge_balance_negative_omit_resultleftvalue) = S ge_signed_half_omit_resultleftvaluedecode))) /\ ((dst_positive_omit_resultleft) + ge_balance_negative_omit_resultleftvalue = (dst_negative_omit_resultleft) + ge_balance_positive_omit_resultleftvalue))))))))) /\ (((exists dst_positive_code_omit_resultright dst_positive_scale_omit_resultright dst_negative_code_omit_resultright dst_negative_scale_omit_resultright dst_positive_omit_resultright dst_negative_omit_resultright. (((G) = (((((dst_positive_code_omit_resultright) + (dst_positive_scale_omit_resultright)) * S ((dst_positive_code_omit_resultright) + (dst_positive_scale_omit_resultright)) + ((dst_positive_scale_omit_resultright) + (dst_positive_scale_omit_resultright))) + (((dst_negative_code_omit_resultright) + (dst_negative_scale_omit_resultright)) * S ((dst_negative_code_omit_resultright) + (dst_negative_scale_omit_resultright)) + ((dst_negative_scale_omit_resultright) + (dst_negative_scale_omit_resultright)))) * S ((((dst_positive_code_omit_resultright) + (dst_positive_scale_omit_resultright)) * S ((dst_positive_code_omit_resultright) + (dst_positive_scale_omit_resultright)) + ((dst_positive_scale_omit_resultright) + (dst_positive_scale_omit_resultright))) + (((dst_negative_code_omit_resultright) + (dst_negative_scale_omit_resultright)) * S ((dst_negative_code_omit_resultright) + (dst_negative_scale_omit_resultright)) + ((dst_negative_scale_omit_resultright) + (dst_negative_scale_omit_resultright)))) + ((((dst_negative_code_omit_resultright) + (dst_negative_scale_omit_resultright)) * S ((dst_negative_code_omit_resultright) + (dst_negative_scale_omit_resultright)) + ((dst_negative_scale_omit_resultright) + (dst_negative_scale_omit_resultright))) + (((dst_negative_code_omit_resultright) + (dst_negative_scale_omit_resultright)) * S ((dst_negative_code_omit_resultright) + (dst_negative_scale_omit_resultright)) + ((dst_negative_scale_omit_resultright) + (dst_negative_scale_omit_resultright)))))) /\ (((((exists ff_h_pvs_omit_resultrightpositive. ff_h_pvs_omit_resultrightpositive + S (dst_positive_omit_resultright) = S ((S (dc_quotient_omit_result)) * dst_positive_scale_omit_resultright)) /\ exists ff_q_pvs_omit_resultrightpositive. dst_positive_code_omit_resultright = ff_q_pvs_omit_resultrightpositive * S ((S (dc_quotient_omit_result)) * dst_positive_scale_omit_resultright) + (dst_positive_omit_resultright))) /\ (((((exists ff_h_pvs_omit_resultrightnegative. ff_h_pvs_omit_resultrightnegative + S (dst_negative_omit_resultright) = S ((S (dc_quotient_omit_result)) * dst_negative_scale_omit_resultright)) /\ exists ff_q_pvs_omit_resultrightnegative. dst_negative_code_omit_resultright = ff_q_pvs_omit_resultrightnegative * S ((S (dc_quotient_omit_result)) * dst_negative_scale_omit_resultright) + (dst_negative_omit_resultright))) /\ (exists ge_balance_positive_omit_resultrightvalue ge_balance_negative_omit_resultrightvalue. (((((dc_right_omit_result) = 2 * (ge_balance_positive_omit_resultrightvalue) /\ (ge_balance_negative_omit_resultrightvalue) = 0) \/ exists ge_signed_half_omit_resultrightvaluedecode. (((dc_right_omit_result) = 2 * ge_signed_half_omit_resultrightvaluedecode + 1 /\ (ge_balance_positive_omit_resultrightvalue) = 0) /\ (ge_balance_negative_omit_resultrightvalue) = S ge_signed_half_omit_resultrightvaluedecode))) /\ ((dst_positive_omit_resultright) + ge_balance_negative_omit_resultrightvalue = (dst_negative_omit_resultright) + ge_balance_positive_omit_resultrightvalue))))))))) /\ (exists sto_ap_omit_resultproduct sto_an_omit_resultproduct sto_bp_omit_resultproduct sto_bn_omit_resultproduct sto_cp_omit_resultproduct sto_cn_omit_resultproduct. (((((dc_left_omit_result) = 2 * (sto_ap_omit_resultproduct) /\ (sto_an_omit_resultproduct) = 0) \/ exists ge_signed_half_omit_resultproductleft. (((dc_left_omit_result) = 2 * ge_signed_half_omit_resultproductleft + 1 /\ (sto_ap_omit_resultproduct) = 0) /\ (sto_an_omit_resultproduct) = S ge_signed_half_omit_resultproductleft))) /\ ((((((dc_right_omit_result) = 2 * (sto_bp_omit_resultproduct) /\ (sto_bn_omit_resultproduct) = 0) \/ exists ge_signed_half_omit_resultproductright. (((dc_right_omit_result) = 2 * ge_signed_half_omit_resultproductright + 1 /\ (sto_bp_omit_resultproduct) = 0) /\ (sto_bn_omit_resultproduct) = S ge_signed_half_omit_resultproductright))) /\ ((((((0) = 2 * (sto_cp_omit_resultproduct) /\ (sto_cn_omit_resultproduct) = 0) \/ exists ge_signed_half_omit_resultproductoutput. (((0) = 2 * ge_signed_half_omit_resultproductoutput + 1 /\ (sto_cp_omit_resultproduct) = 0) /\ (sto_cn_omit_resultproduct) = S ge_signed_half_omit_resultproductoutput))) /\ ((sto_ap_omit_resultproduct * sto_bp_omit_resultproduct + sto_an_omit_resultproduct * sto_bn_omit_resultproduct) + sto_cn_omit_resultproduct = (sto_ap_omit_resultproduct * sto_bn_omit_resultproduct + sto_an_omit_resultproduct * sto_bp_omit_resultproduct) + sto_cp_omit_resultproduct))))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_omit_resultnondivisor. (n) = (d) * pvs_factor_omit_resultnondivisor)) /\ ((0)=0))))

Complete tactic proof in conservative notation

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

10 script commands · 4 reading checkpoints · 0 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

01Fix variables and assumptionsL1–5

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

L1
intro F
L2
intro G
L3
intro n
L4
intro d
L5
intro hd

02Separate the logical casesL6–8

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

L6
right
L7
split
L8
right

03Use earlier factsL9–9

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

L9
exact hd

04Calculate and transport equalitiesL10–10

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

L10
refl

Library-wide reading audit

Original defined command ledger · 10 lines

0001intro F
0002intro G
0003intro n
0004intro d
0005intro hd
0006right
0007split
0008right
0009exact hd
0010refl