The Weil explicit formula expresses \(\sum _\rho h(\rho )\) in terms of local data. Meyer’s (2005) spectral interpretation identifies the adèlic \(L^2\) spectrum with the multiset of zeta zeros, closing arithmetic_admissibility.

Gap: Weil explicit formula and Meyer’s spectral-Weil identity require full adèlic Fourier analysis (not in Mathlib 4.19.0). Documented as three axioms: weil_explicit_formula, meyer_spectral_weil_identity, weil_distribution_positivity.