Abstract Zeta–Möbius Inversion: A Minimal Monoid-Based Schema for Formal Verification

This archive contains Abstract Zeta–Möbius Inversion, a standalone Lean 4 formalisation of the abstract algebraic structure underlying Möbius inversion. The project isolates the minimal assumptions required for Möbius inversion by introducing an abstract Zeta–Möbius schema: a monoid equipped with distinguished elements ζ and μ forming a two-sided inverse pair. From this schema, the standard inversion and cancellation principles of Möbius inversion are derived once and for all, independently of any arithmetic, analytic, or combinatorial interpretation. Crucially, no arithmetic meaning is built into the abstract layer. Classical Dirichlet convolution appears only as a concrete instance, supplied via an explicit inverse specification asserting that the Möbius function is the convolution inverse of the constant-one function. This design ensures that all number-theoretic content is local, explicit, and auditable, rather than being smuggled in via global instances or implicit assumptions. The formalisation: is axiom-free beyond the standard axioms already present in Mathlib, makes no analytic or asymptotic assumptions, introduces no global instances that hide proofs or dependencies, and prioritises minimality, transparency, and transport stability over convenience. The repository includes: the abstract Zeta–Möbius schema, solver-style inversion and cancellation lemmas, a transport-stable algebraic development of Dirichlet convolution, a parametrised Dirichlet instance of the schema, and minimal smoke tests demonstrating correct composition of the abstract and concrete layers. An accompanying paper, Abstract Zeta–Möbius Inversion: A Minimal Monoid-Based Schema for Formal Verification, is included in the docs/ directory and explains the motivation, design decisions, and formal structure of the development. This release is intended as a conceptually complete, archival artefact and as a reusable foundation for further formal work on inversion principles in number theory, combinatorics, and related areas.