Arbitrary-target triangular construction · exact criterion · positive uniqueness · Constructive arithmetic

General finite signed Dirichlet inverses

ArithTable(N,F) ⇒ ((∃G. DirichletInverse(N,F,G)) ⇔ (N=0 ∨ DirichletUnitAtOne(F)))

Construct the inverse with any prescribed zeroth value, characterize existence, and prove positive-value uniqueness and compatible restrictions.

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

Open the exact edition →

Focused route

Final dependency cone

Start at theorem IV0013 and follow only the lemmas and conservative definitions supporting dirichlet_inverse_criterion.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G009 milestone → theorem and definition dependencies.
Major independently established statements: IV0009 dirichlet_unit_equation_construct · IV0015 dirichlet_inverse_exists_positive_unique · IV0013 dirichlet_inverse_criterion.
Independently verified Alpha v34 checked-use theorem family: 21 dependency-curried kernel-checked theorem bodies · 53 proof prerequisites · 24 linked definitions · 41 definition-dependency arrows · 764 exact tactic lines · first admitted v31 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 401 bundle nodes; SHA-256 420f08dcb5c67a260a28f391bdaa5b1f75464c73dc174fbe5cdcd4d08336c826.
Exact mathematical boundary: For an actual table an inverse exists exactly when N=0 or F(1) is signed +1 or -1. At a positive window this is the unit-at-one criterion; the empty window imposes no condition at one. Every inverse has actual delta and two-sided convolution witnesses. Its zeroth value is arbitrary, so uniqueness is positive-value equality, not equality of codes or of zeroth values. Multiplicative-function closure and full finite signed G009 are admitted in the separate Alpha-v32 multiplicative-convolution family.