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 \emph{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 \emph{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.