Abstract Zeta–Möbius Inversion: A Minimal Monoid-Based Schema for Formal Verification
Fuente:
Zenodo
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Recurso digital |
| Langue: | anglais |
| Publié: |
Zenodo
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866901742562574336 |
|---|---|
| author | Jefferson, Bob |
| author_facet | Jefferson, Bob |
| contents | <p>This archive contains <em>Abstract Zeta–Möbius Inversion</em>, a standalone Lean 4 formalisation of the abstract algebraic structure underlying Möbius inversion.</p> <p>The project isolates the minimal assumptions required for Möbius inversion by introducing an abstract <strong>Zeta–Möbius schema</strong>: 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.</p> <p>Crucially, no arithmetic meaning is built into the abstract layer. Classical Dirichlet convolution appears only as a <em>concrete instance</em>, 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.</p> <p>The formalisation:</p> <ul> <li> <p>is axiom-free beyond the standard axioms already present in Mathlib,</p> </li> <li> <p>makes no analytic or asymptotic assumptions,</p> </li> <li> <p>introduces no global instances that hide proofs or dependencies, and</p> </li> <li> <p>prioritises minimality, transparency, and transport stability over convenience.</p> </li> </ul> <p>The repository includes:</p> <ul> <li> <p>the abstract Zeta–Möbius schema,</p> </li> <li> <p>solver-style inversion and cancellation lemmas,</p> </li> <li> <p>a transport-stable algebraic development of Dirichlet convolution,</p> </li> <li> <p>a parametrised Dirichlet instance of the schema, and</p> </li> <li> <p>minimal smoke tests demonstrating correct composition of the abstract and concrete layers.</p> </li> </ul> <p>An accompanying paper, <em>Abstract Zeta–Möbius Inversion: A Minimal Monoid-Based Schema for Formal Verification</em>, is included in the <code>docs/</code> directory and explains the motivation, design decisions, and formal structure of the development.</p> <p>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.</p> |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_18260962 |
| institution | Zenodo |
| language | eng |
| publishDate | 2026 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | Abstract Zeta–Möbius Inversion: A Minimal Monoid-Based Schema for Formal Verification Jefferson, Bob Möbius inversion zeta–Möbius inversion formal verification Lean 4 Mathlib Algebra Dirichlet convolution arithmetic functions proof assistants <p>This archive contains <em>Abstract Zeta–Möbius Inversion</em>, a standalone Lean 4 formalisation of the abstract algebraic structure underlying Möbius inversion.</p> <p>The project isolates the minimal assumptions required for Möbius inversion by introducing an abstract <strong>Zeta–Möbius schema</strong>: 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.</p> <p>Crucially, no arithmetic meaning is built into the abstract layer. Classical Dirichlet convolution appears only as a <em>concrete instance</em>, 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.</p> <p>The formalisation:</p> <ul> <li> <p>is axiom-free beyond the standard axioms already present in Mathlib,</p> </li> <li> <p>makes no analytic or asymptotic assumptions,</p> </li> <li> <p>introduces no global instances that hide proofs or dependencies, and</p> </li> <li> <p>prioritises minimality, transparency, and transport stability over convenience.</p> </li> </ul> <p>The repository includes:</p> <ul> <li> <p>the abstract Zeta–Möbius schema,</p> </li> <li> <p>solver-style inversion and cancellation lemmas,</p> </li> <li> <p>a transport-stable algebraic development of Dirichlet convolution,</p> </li> <li> <p>a parametrised Dirichlet instance of the schema, and</p> </li> <li> <p>minimal smoke tests demonstrating correct composition of the abstract and concrete layers.</p> </li> </ul> <p>An accompanying paper, <em>Abstract Zeta–Möbius Inversion: A Minimal Monoid-Based Schema for Formal Verification</em>, is included in the <code>docs/</code> directory and explains the motivation, design decisions, and formal structure of the development.</p> <p>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.</p> |
| title | Abstract Zeta–Möbius Inversion: A Minimal Monoid-Based Schema for Formal Verification |
| topic | Möbius inversion zeta–Möbius inversion formal verification Lean 4 Mathlib Algebra Dirichlet convolution arithmetic functions proof assistants |
| url | https://doi.org/10.5281/zenodo.18260962 |