Actual divisor pairs · support reindexing · finite signed closure · Constructive arithmetic

Multiplicative Dirichlet convolution

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

Construct a convolution table of normalized multiplicative signed prefixes and prove its complete coprime product law and positive-value uniqueness.

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 5388 native tactic lines and 313 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem MX0059 and follow only the lemmas and conservative definitions supporting dirichlet_convolution_multiplicative_exists_unique.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G009 milestone → theorem and definition dependencies.
Major independently established statements: MX004A signed_support_reindex_sum_equal · MX002C signed_cartesian_product_sums_exists · MX0011 coprime_divisor_factor_pair_exists_unique · MX0057 dirichlet_convolution_multiplicative_values · MX0058 dirichlet_convolution_multiplicative_table · MX0059 dirichlet_convolution_multiplicative_exists_unique.
Independently verified Alpha v34 checked-use theorem family: 90 dependency-curried kernel-checked theorem bodies · 313 proof prerequisites · 42 linked definitions · 97 definition-dependency arrows · 5388 exact tactic lines · first admitted v32 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 462 bundle nodes; SHA-256 953dc5ef340379b1e34883c2f9ab2181e91c872f5bbb7943c52b2fb70ce76959.
Exact mathematical boundary: MultiplicativePrefix requires N>0 and the actual value F(1)=+1, not merely ±1. The product law covers positive coprime m,n with mn≤N. Zeroth values and table representations are unrestricted; uniqueness compares represented positive values only. Actual incidence, Cartesian tables and finite folds are constructed. General prime-power fields (G091) remain open. These exact theorems are first admitted to Alpha v32; Stable remains unchanged.