A Formal Structural Audit of Dirichlet–Möbius Algebra

This archive contains a Lean 4 formal codebase and accompanying paper providing a structural audit of Dirichlet convolution and Möbius inversion. The project does not introduce new results in number theory. Instead, it reconstructs the classical Dirichlet–Möbius algebra in a fully explicit, transport-stable formal setting and documents the structural assumptions that standard textbook treatments typically leave implicit. These include: explicit transport between equivalent representations of arithmetic functions, the minimal algebraic requirements for associativity, units, and inversion, enforced boundary conventions (notably the value at 0), and the directionality of zeta convolution and Möbius inversion. All algebraic operations are centralised in a canonical representation and inherited by others via explicit equivalences. The development is mechanically verified, reproducible, and pinned to a specific Lean toolchain and Mathlib commit. The accompanying paper, A Formal Structural Audit of Dirichlet–Möbius Algebra, analyses what becomes visible when these constructions are formalised under such constraints. It presents concrete failure modes, repaired interfaces, and general methodological lessons for transport-stable formalisation. This work complements, rather than modifies, Mathlib. It interoperates with existing libraries via explicit equivalences but exists as a separate verification and audit layer. The archive is intended both as a reference-grade formal artefact and as a methodological resource for developers of formal mathematics libraries that rely on Dirichlet convolution, divisor sums, or Möbius inversion. Version 1.2 reflects a finalised, submission-ready paper and a consolidated repository structure, with clarified scope, terminology, and documentation.