Bombieri–Vinogradov in Lean, conditional on Siegel–Walfisz: proof layout that compiled

About 1500 lines on top of a multiplicative large sieve over primitive characters, Pólya–Vinogradov, and Vaughan's identity. SW is kept as an explicit hypothesis. (1) Orthogonality with Mathlib's DirichletCharacter.sum_char_inv_mul_char_eq gives φ(q)(ψ(y;q,a) − ψ_q(y)/φ(q)) = ∑_{χ≠1} χ(a⁻¹)ψ(y,χ). Here (1 : MulChar) a⁻¹ = 1 via MulChar.one_apply and IsUnit.of_mul_eq_one a (ZMod.inv_mul_of_unit a ha). Use filter_ne' plus add_sum_erase to split off χ₀. (2) Pass to the primitive character with conductor/primitiveCharacter/changeLevel_primitiveCharacter. Injectivity of χ ↦ ⟨conductor, primitiveCharacter⟩ into a Σ-type: the inverse is x ↦ if h : x.1 ∣ q then changeLevel h x.2 else 1. Then sum_image and sum_sigma. (3) For the max over y, define M = (range (x+1)).sup' nonempty_range_add_one (‖ψ(·,χ)‖) and take a maximiser with exists_mem_eq_sup'. Feed the main estimate an arbitrary choice function y : (d : ℕ) → DirichletCharacter ℂ d → ℕ, so no max ever appears inside the estimate. (4) Main estimate: Vaughan. Type I terms by Pólya–Vinogradov applied to the inner sum of ∑_m f(m)ψ(m)∑_{k≤y/m} g(k)ψ(k). Type II by dyadic blocks plus a Perron-free bilinear sieve with cut-off. With U, V polylogarithmic there is no need to split μ≤V*Λ≤U*1 as Davenport does. (5) Over the moduli: ∑_{q≤Q, d|q} 1/φ(q) ≤ (π²/6)²(1+log Q)/φ(d). Then Abel summation against a quadratic bound ∑_{d≤R} w_d ≤ α+βR+γR², which gives ∑_{Q₁<d≤Q} w_d/d ≤ 2α/(Q₁+1)+β(2+log Q)+2γQ. (6) For the asymptotic form, state the explicit version under the condition (log x)^{20n+92} ≤ x, then filter_upwards with isLittleO_pow_log_id_atTop.bound. Use powers of ⌊log x⌋₊ for Q₁, U, V to avoid rpow.