The \(L^2(\mathbb {A}^\times /\mathbb {Q}^\times )\) spectral decomposition is well-defined after Haar regularization:

1. \(K^1\) compact \(\Rightarrow \) finite Haar measure \(\Rightarrow \) \(L^\infty \subseteq L^2\)

2. Peter-Weyl on \(K^1\): \(L^2(K^1) = \bigoplus _\chi \mathbb {C}\cdot \chi \)

3. Plancherel: \(\| f\| ^2 = \sum _\chi |\hat f(\chi )|^2\)

Algebraic core proved: l_infty_subset_l2_compact (1 sorry: integral_mono with bounded functions, Mathlib 4.19 gap). Three axioms: peter_weyl_K1, plancherel_K1, spectrum_discrete_K1.