A multivariate Erdős–Kac theorem for shifted primes, with explicit arithmetic covariance under Bombieri–Vinogradov

Abstract Let N₁, …, Nₖ be pairwise distinct even integers with X ≤ Nᵢ ≤ 2X, and let p run uniformly over the primes p < X. We record, in closed and machine-verifiable form, the joint distribution of the shifted additive functions ω(N₁−p), …, ω(Nₖ−p). The pairwise covariance of the truncated functions ω_z(Nᵢ−p) admits an explicit two-branch sign split for every z ≤ X^(1/4−ε): • a diagonal contribution (q−2)/(q−1)² when q divides Nᵢ−Nⱼ;• an off-diagonal contribution −1/(q−1)² otherwise, with a power-of-log error coming from Bombieri–Vinogradov. The identity extends to the matrix Γ_X = L·Iₖ + Oₖ(log L), where L = log log X, which is literally the covariance of the corresponding independent-residue model; the method of moments then yields a multivariate central limit theorem for (ω_z(Nᵢ−p)). Choosing z = X^(L^(−1/4)) removes the truncation and gives a multivariate Erdős–Kac theorem on the natural scale √L with limiting covariance the identity, uniformly over the shifts. The algebraic core (the sign split and the Chinese Remainder reduction) is formalised in Lean 4 and verified by the AXLE engine (environment lean-4.28.0); Bombieri–Vinogradov and Mertens are used as black boxes. Numerical computation at X ≤ 10⁵ confirms the pairwise and matrix identities with Frobenius error below 6·10⁻². Contents of the record • 01_Shifted_Primes_Covariance_EN.pdf — English version, main file and default preview;• 01_Primos_Deslocados_Covariancia_PT.pdf — faithful Portuguese version;• 01_shifted-primes-covariance_supplementary.zip — supplementary archive with Python scripts, LaTeX sources, Lean 4 sources and the AXLE verification report. Formal verification (AXLE) AXLE validates formal deduction, not external conjectures. Three blocks were formalised in Lean 4 and verified remotely in environment lean-4.28.0, each returning okay: true with an empty failed_declarations list: 1. The Chinese Remainder Theorem identity used in the pairwise reduction — request_id 259813d5-c2af-4d72-949c-5b26fb60ae4e;2. The discrete arithmetic core of the shared small prime factors lemma — request_id e7130225-a6cc-4588-9479-c4f8b6a10882;3. The covariance of the independent-residue model used in the method-of-moments step — request_id af4bfc2d-964a-41d9-abb2-50f49cf28cbc. Bombieri–Vinogradov, Mertens, Cramér–Wold and the real-analysis step of the weighted bound remain classical and lie outside AXLE's scope.