Constructive Peter--Weyl Theory: What Is Known and What Remains Open
What is known about constructive Peter-Weyl theory, and what remains open? This expository article separates established theorems, comparisons between formulations, and questions requiring further investigation in the Bishop-Coquand-Spitters line. Its central finding is that constructive Peter-Weyl theory already has an established compact-group approximation core: under specified analytic and Gelfand hypotheses, finite-rank central convolution projections converge strongly in the Haar L2 norm. We make these hypotheses and the projection-kernel normalization explicit, and record the resulting spectral Hilbert completion. This answers the question of completion affirmatively for that precise core theorem. Broader claims about the whole classical package or its validity across constructive foundations require separate comparisons; uniform approximation, irreducible representation data, and point-set recovery are not inferred from strong convergence alone. The historical problems of left-right almost periodicity and universal Bohr compactification are examined with a dated follow-up literature review, distinguishing related progress from a verified resolution. A sufficient metric realization criterion, finite examples, and a separate nonassociative outlook clarify the scope of the established method. An extended appendix proves the classical Peter-Weyl theorem through Haar averaging, convolution, spectral density, point separation, and irreducible orthogonality. Stage-by-stage comparisons explain which arguments transfer constructively and which require additional data or a different proof. The article therefore identifies what is proved and what additional statements or data remain to be examined, without treating an unidentified resolution as proof that a problem is currently open.