Arbitrary zeroth values · actual constructors · divisor sums · Constructive arithmetic

One and delta convolution tables

ArithTable(N,F) ∧ KroneckerDeltaTable(N,E) ⇒ DirichletTable(N,F,E,F) ∧ DirichletTable(N,E,F,F)

Construct one and delta tables and prove the actual two-sided unit and divisor-sum identities.

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

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

Open the exact edition →

Focused route

Final dependency cone

Start at theorem DU0019 and follow only the lemmas and conservative definitions supporting dirichlet_constant_one_realizes_divisor_sum.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G009 milestone · G007 milestone → theorem and definition dependencies.
Major independently established statements: DU0013 dirichlet_delta_unit_exists · DU0018 dirichlet_constant_one_sum_iff · DU0019 dirichlet_constant_one_realizes_divisor_sum.
Independently verified Alpha v34 checked-use theorem family: 25 dependency-curried kernel-checked theorem bodies · 82 proof prerequisites · 23 linked definitions · 45 definition-dependency arrows · 1109 exact tactic lines · first admitted v31 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 282 bundle nodes; SHA-256 232ddd461eb83d97c1a6255a872be7e970b635ce1d4e958c8bed7706419687b7.
Exact mathematical boundary: Signed one is code 2. Positive-only table graphs preserve arbitrary zeroth values, including N=0. The unit and divisor-sum identities are proved, never embedded in definitions. The separate inverse family proves the general unit-at-one criterion; multiplicative-function closure remains open.