Strict-prefix folds · real table extension · the value at one · Constructive arithmetic

Constructed triangular convolution steps

ArithAt(F,1,a) ∧ ArithAt(G,1,b) ⇒ (DirichletSum(F,G,1,z) ⇔ SignedMul(a,b,z))

Construct the proper convolution prefix before the new endpoint, then append the actual signed product.

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

Open the exact edition →

Focused route

Final dependency cone

Start at theorem DT0006 and follow only the lemmas and conservative definitions supporting dirichlet_convolution_strict_prefix_exists.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G009 milestone → theorem and definition dependencies.
Major independently established statements: DT0008 dirichlet_convolution_first_input_append_step · DT000A dirichlet_convolution_at_one_iff · DT0006 dirichlet_convolution_strict_prefix_exists.
Independently verified Alpha v34 checked-use theorem family: 10 dependency-curried kernel-checked theorem bodies · 43 proof prerequisites · 19 linked definitions · 33 definition-dependency arrows · 547 exact tactic lines · first admitted v31 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 219 bundle nodes; SHA-256 d2d1b032400b46679658f6b196272df3e0869378a651e711e1b7985778e121e1.
Exact mathematical boundary: The strict remainder is an actual inclusive prefix through k with an S k-entry fold; the future input at S k is excluded. A genuine table extension supplies the endpoint. The at-one identity inspects or constructs the real two-entry masked sum. No recurrence, inverse, or omitted summand value is assumed as a conclusion-bearing premise.