Exact Symmetry as Algebra: A Machine-Verified Tensor Calculus that Enforces Physical Selection Rules

Symmetry is central to the physical sciences, yet machine learning usually captures it only approximately, leaving a residual per-step equivariance error \varepsilon that compounds with depth M as M\varepsilon, whereas exact equivariance holds at unbounded depth; we demonstrate this divergence at fourteen orders of magnitude. We show that a symmetry can be made exact by construction, as the multiplication rule of a tensor algebra. In the resulting \starG algebra, defined by any finite group G, the group-Fourier transform block-diagonalizes every tensor into irreducible-representation blocks, making equivariance intrinsic; requiring equivariance conversely forces this suitably normalized transform, so the algebra is determined by G rather than chosen. The standard matrix toolbox, including a Frobenius-optimal low-rank factorization, transfers blockwise, machine-checked in Lean 4 under an explicit axiom budget, and extends unchanged to band-limited compact groups and, under periodic boundary conditions, to all 230 crystallographic space groups and the compact little-group fibers of Euclidean and Poincaré symmetry. This exactness is an applied capability: on inorganic-crystal elastic tensors the algebra enforces point-group selection rules exactly on the output of any predictor, driving a trained graph network's forbidden-channel leakage from 10^{-2} to machine zero, eliminating mechanically unstable predictions, and recovering viable materials that an unconstrained screen discards; on molecular data, with no quantum-mechanical input, it exposes octahedral selection-rule signatures consistent with the Wigner--Eckart theorem. Matched networks lead on pooled molecular accuracy, which we report plainly: the contribution is a complementary algebraic calculus, structural and diagnostic, exact at any depth.