Abstract Zeta–Möbius Inversion: With Dirichlet and Inclusion–Exclusion Instances

This archive contains a complete Lean 4 formalisation of an abstract Zeta–Möbius inversion schema, together with two fully verified concrete instances: Dirichlet convolution on arithmetic functions Inclusion–exclusion on finite sets (the Boolean lattice) The project isolates the minimal algebraic structure required for Möbius inversion: a monoid equipped with distinguished elements ζ and μ that are proven to be two-sided inverses. No arithmetic, analytic, or combinatorial meaning is built into the schema itself. All inversion and cancellation properties are derived formally from the abstract axioms. Both concrete instances are supplied only via explicit inverse specifications. No global instances, axioms, or analytic assumptions are introduced. This design ensures that all dependencies are local, explicit, and auditable, and that the abstract framework can be safely reused in other formal developments. The formalisation demonstrates that classical inversion principles from number theory (Dirichlet inversion) and combinatorics (inclusion–exclusion) share the same underlying algebraic structure, despite operating over fundamentally different domains. The archive includes: the abstract Zeta–Möbius schema, verified instances for Dirichlet convolution and inclusion–exclusion, supporting algebraic infrastructure, and minimal smoke tests confirming correct composition with the abstract solver lemmas. The project builds exclusively on Lean 4 and Mathlib and is intended as a reusable, transport-stable foundation for formalised Möbius inversion and related algebraic reasoning. Version 1.2 adds the inclusion–exclusion instance, a worked inversion example, improved documentation, and clarifies the role of this development as a transportability demonstration building on the foundational abstract schema.