Constructed factor grids · row and column sums · true Fubini · Constructive arithmetic

Finite convolution associativity

DirichletTable(N,F,G,A) ∧ DirichletTable(N,G,H,B) ∧ DirichletTable(N,A,H,L) ∧ DirichletTable(N,F,B,R) ⇒ ArithPositiveEqual(L,R,N)

Build actual first/last-factor grids and prove that both convolution parenthesizations agree.

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

Open the exact edition →

Focused route

Final dependency cone

Start at theorem DF0020 and follow only the lemmas and conservative definitions supporting dirichlet_convolution_associative_tables_exists.

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: DF001D dirichlet_convolution_fubini_interchange · DF001E dirichlet_convolution_associative · DF0020 dirichlet_convolution_associative_tables_exists.
Independently verified Alpha v34 checked-use theorem family: 32 dependency-curried kernel-checked theorem bodies · 117 proof prerequisites · 29 linked definitions · 65 definition-dependency arrows · 1962 exact tactic lines · first admitted v31 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 347 bundle nodes; SHA-256 05cb102ae5fb423e325223589eb17b8f1dd0aa8d3cb8419425142f9be087d9f3.
Exact mathematical boundary: Every grid, slice, row sum and intermediate table is constructed. Retained cells have witnessed n=(a*e)*c and value F(a)*(H(e)*G(c)). The flat endpoint is unused. Table associativity includes N=0 and compares only positive values, not encodings. Full G009 remains broader.