Vaughan’s identity / BDH / BV-lite in Lean 4

Stream: mathlib4

[Bob Jefferson]

Hi all — I’m working on a Stage-3 façade for Maynard–Tao (twin window) and now moving to BV-lite (θ < 1/2) to internalize bounded gaps ≤ C inside Lean.

Before we start formalizing, does anyone have in-progress code/branches for any of the following?

1. Vaughan’s identity (any of the standard decompositions for Λ).

2. Large sieve (character/exponential versions) with explicit constants.

3. Barban–Davenport–Halberstam (BDH) second-moment statements.

4. A Bombieri–Vinogradov statement (even coarse constants).

We’re already using mathlib’s ArithmeticFunction.vonMangoldt/Dirichlet character/AP modules. Our end goal is a coarse BV feeding a Maynard inequality to give AvgWindowHitLB ≥ 2 on a small H ⊆ [0,600].

If there’s anything to build on (WIP PRs, sketches, naming conventions), we’d love pointers. Happy to contribute missing pieces as small, reviewable PRs. Thanks!