Tensor Renormalization Group Meets Computer Assistance

Tensor renormalization group, originally devised as a numerical technique, is emerging as a rigorous analytical framework for studying lattice models in statistical physics. Here we introduce a new renormalization map - the 2x1 map - which coarse-grains the lattice anisotropically by a factor of two in one direction followed by a 90-degree rotation. We develop a novel graphical language that translates the action of the 2x1 map into a system of inequalities on tensor components, with rigorous estimates in the Hilbert-Schmidt norm. We define a finite-dimensional "bounding box" called the hat-tensor, and a master function governing its RG flow. Iterating this function numerically, we establish convergence to the high-temperature fixed point for tensors lying within a quantifiable neighborhood. Our main theorem shows that tensors with deviations bounded by 0.02 in 63 orthogonal sectors flow to the fixed point. We also apply the method to specific models - the 2D Ising and XY models - obtaining explicit bounds on their high-temperature phase. This work brings the Tensor RG program closer towards a rigorous, computer-assisted construction of critical fixed points.