Recover every original positive value from its divisor transform using actual finite Möbius-weighted sums.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
MI0001 · arithmetic_divisor_transform_convolutionA genuine divisor transform is the actual convolution with a constructed positive constant-one table, on the whole positive domain.
layer 0 · 39 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMI0002 · arithmetic_divisor_convolution_transformActual convolution with the positive constant-one table supplies the original divisor-transform relation, including all required finite sum witnesses.
layer 0 · 33 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMI0003 · mobius_constant_one_convolution_deltaThe previously proved prime-toggle cancellation identifies the actual convolution of independently defined Möbius values and constant one with every actual delta table.
layer 0 · 69 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMI0004 · mobius_dirichlet_inversion_valueActual finite associativity changes Möbius times the divisor transform into delta times the original input; the transform premise covers every required positive quotient.
layer 1 · 74 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMI0005 · mobius_inversion_for_actual_mobius_tableConstruct one and delta tables and every genuine weighted fold before proving that the actual original table is the full positive-window Möbius inverse.
layer 2 · 68 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMI0006 · mobius_inversion_arithmetic_tablesFull finite signed Möbius inversion constructs the independent Möbius table and a real output table whose actual weighted divisor sums recover every positive original value, including the genuine empty-window case N=0.
layer 3 · 38 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMI0007 · mobius_inversion_reconstructs_divisor_transformThe converse constructs actual unit tables and finite folds; associativity turns one times a Möbius convolution back into the original divisor transform.
layer 1 · 109 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableMI0008 · mobius_inversion_iffFor actual finite signed tables, being the divisor transform is equivalent to being inverted by the independently defined Möbius convolution; no values at zero are constrained on either input.
layer 3 · 28 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableExactly 8 displayed theorems have independently verified Alpha checked-use authority; none is admitted to Stable. Body-only enrollment never grants checked theorem use.