A Lean 4 Multiplicative Functions Core: Transport-Stable Dirichlet Convolution and Möbius Inversion

Multiplicative Functions Core (Version 2.1) This archive contains Multiplicative Functions Core (v2.1), a Lean 4 library providing a fully formalised, finite, and purely algebraic core for multiplicative arithmetic functions, finite Dirichlet convolution, and Möbius inversion. The development is built entirely on finite constructions, using Nat.factorization and finite sums over divisors. No analytic number theory, infinite series, or asymptotic arguments are used anywhere in the library. Mathematical content The Möbius function is implemented in a factorisation-first style (muViaFactorization). Its basic structural properties are formally proved, including: values at 0 and 1, vanishing on squareful integers, behaviour on squarefree integers, compatibility with prime factorisation. The classical Möbius divisor sum ∑d∣nμ(d)\sum_{d \mid n} \mu(d)d∣n∑μ(d) is implemented as mobiusDivisorSum and identified with the bundled Dirichlet convolution μ⋆1\mu \star 1μ⋆1. Dirichlet convolution and inversion Version 2 completes the Dirichlet-convolution architecture introduced in Version 1. In contrast to v1, v2 proves the full two-sided Dirichlet inverse property μ⋆1=1⋆μ=ε\mu \star 1 = 1 \star \mu = \varepsilonμ⋆1=1⋆μ=ε purely algebraically, without analytic or asymptotic arguments. The right-hand and left-hand inverse properties are first packaged as explicit specification propositions and then upgraded to a full Dirichlet inverse specification. Möbius inversion is exposed to users as stable, monoid-level theorems, avoiding fragile unfolding of divisor sums. Transport-stable architecture A central design feature of the library is transport stability. Dirichlet convolution on bundled arithmetic functions is packaged as a monoid by transporting structure across an equivalence with Mathlib’s ArithmeticFunction. This ensures that associativity, unit laws, and inverse laws are definitionally stable, and that downstream proofs are robust under internal refactoring. The archive includes a formal bridge proving that the factorisation-based Möbius function muViaFactorization agrees pointwise with Mathlib’s bundled ArithmeticFunction.moebius, allowing results to be transported cleanly between the two formulations. Software properties All definitions and proofs are finite, algebraic, and transport-stable No axioms beyond those already present in Mathlib are used(propext, Classical.choice, Quot.sound) No scratch or attic files are included in the archive Reproducibility and documentation Reproducibility is ensured via a pinned Lean toolchain and lake-manifest.json.The archive includes a small smoke test at: Multiplicative/Examples/SmokeTest.lean which verifies that the public API imports correctly and that the main Möbius inversion theorems are accessible. A companion paper in the docs/ directory provides detailed architectural, mathematical, and design documentation for the library and should be cited alongside the software where appropriate.