Covariance identity for the random Fourier series

The multidimensional Poisson-summation proof is deterministic and lives in CovariancePoissonDeterministic. This compatibility module adds only the final probability-facing covariance corollary, preserving the original import path and public API.

theorem Anderson4D.NoiseModel.integral_xiEps_mul_eq_etaEpsT4 (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x y : T4) : ∫ (ω : M.Ω), M.xiEps ρ ε ω x * M.xiEps ρ ε ω y = ρ.etaEpsT4 ε (x - y)

Headline covariance identity (paper (2.3)).

The Lebesgue-normalized random Fourier series, including its half-density (2π)⁻², has exactly the periodized cutoff covariance used by detIntegrand and the Wick-expansion layer.