Manuscript and Formal Verification Repository: "A Dyadic Covariance Framework for the Mertens Function and the $N^{1/2+\varepsilon}$ Problem"

Repository description This repository contains the main manuscript, a verification supplement, and a companion Lean 4 / Aristotle formalization repository associated with a finite dyadic covariance framework for the Mertens function. The manuscript presents a proof of the bound \[M(N) \ll_\varepsilon N^{1/2+\varepsilon},\] together with the final implication to the Riemann Hypothesis through Littlewood's criterion. The proof is organized around an exact dyadic covariance identity for \(M(N)^2\), followed by a finite packet/profile descent, resonant-state separation, terminal affine-sieve ledgers, and a final packet law whose aggregation yields the Mertens estimate. The approach is designed to preserve the signed structure of the Möbius function until the finite arithmetic data have been reorganized into certified packet ledgers. Non-elementary analytic inputs — including Barban–Davenport–Halberstam / Bombieri–Vinogradov type estimates, Topacogullari's additive-divisor theorem, Kuznetsov / spectral large-sieve estimates, Kim–Sarnak bounds, and automorphic shifted-convolution estimates — are isolated as named theorem boundaries with explicit applicability checks. --- Contents of this repository 1. Main manuscript (.pdf) The full proof, including the exact dyadic cancellation, finite packet/profile descent, statewise tail reductions, terminal affine obstruction, analytic input registry, variable-matching ledger, \(N^\varepsilon\)-loss ledger, final packet law, and aggregation to the Mertens bound. 2. Verification supplement (.pdf) A compact proof map and analytic dependency ledger. It records the main logical checkpoints, the branch structure, the parameter-compatibility checks, the analytic input ledger, and the final-only use of Littlewood's criterion. 3. Lean 4 / Aristotle companion repository (.zip) A reproducible Lean 4 development for selected finite and elementary components of the proof architecture, including finite identities, reindexings, packet-ledger bookkeeping, dependency checks, and conditional final-chain formalizations. The Lean development is not a complete machine-checked proof of the analytic theorem. The external analytic estimates and their full mathematical consumption remain part of the manuscript, not independently machine-verified Lean proofs. --- Purpose This repository is intended to support mathematical review by making the finite-ledger architecture, dependency structure, analytic input boundaries, and scope of the formalization transparent and reproducible. --- Keywords: Mertens function; Riemann Hypothesis; Möbius function; dyadic covariance; analytic number theory; sieve methods; spectral large sieve; Kuznetsov formula; shifted convolution; Lean 4; Aristotle; formal verification.