Actual quotients · finite product tables · commutativity · Constructive arithmetic

Constructed Dirichlet convolution

ArithTable(N,F) ∧ ArithTable(N,G) ⇒ ∃H. DirichletTable(N,F,G,H)

Construct finite signed convolution tables and prove positive-value uniqueness, commutativity and zero padding.

Open the definition-aware map Read the final theorem See campaign milestone G009

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 certificate

Fully expanded arithmetic

Inspect all 1754 native tactic lines and 102 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem DC0028 and follow only the lemmas and conservative definitions supporting dirichlet_convolution_padded_prefix_iff.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G009 milestone → theorem and definition dependencies.
Major independently established statements: DC001D dirichlet_convolution_table_exists_extensionally_unique · DC0024 dirichlet_convolution_table_commutative · DC0028 dirichlet_convolution_padded_prefix_iff.
Independently verified Alpha v34 checked-use theorem family: 40 dependency-curried kernel-checked theorem bodies · 102 proof prerequisites · 26 linked definitions · 50 definition-dependency arrows · 1754 exact tactic lines · first admitted v31 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 270 bundle nodes; SHA-256 313316e788a10dc281dfb0541a447bad9b7b26bbbd68b1030db89d8d28c5a38b.
Exact mathematical boundary: 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.