Αποθηκεύτηκε σε:
| Κύριος συγγραφέας: | |
|---|---|
| Μορφή: | Recurso digital |
| Γλώσσα: | Αγγλικά |
| Έκδοση: |
Zenodo
2026
|
| Θέματα: | |
| Διαθέσιμο Online: | https://doi.org/10.5281/zenodo.18260962 |
| Ετικέτες: |
Προσθήκη ετικέτας
Δεν υπάρχουν, Καταχωρήστε ετικέτα πρώτοι!
|
Πίνακας περιεχομένων:
- <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>