What is in this repo?

This repository contains:

• File paper.pdf with the paper "Tensor Renormalization Group Meets Computer Assistance" [ArXiv:2506.03247].
• The notebook HT.ipynb with the code used for the computer assisted proofs in the paper.
• Files Manifest.toml and Project.toml specifying the package versions required to run HT.ipynb.
• File .JuliaFormatter.toml specifying the code formatting options.
• File colorscheme containing the colorscheme used in Figures 8,9, and 11 in the paper.
• File tensor_fe_ising_upper_bound containing the values of tensor network free energy used in Figure 10 in the paper. To recreate Figure 10 from scratch, please delete this file.

Installation instructions

To run HT.ipynb, install Julia. Then, install IJulia. The rest of the dependencies will be installed automatically during the first execution of the first code cell in the HT.ipynb notebook.

Computer assisted high-temperature phase proof

The notebook HT.ipynb offers a method for checking whether a given system is in the high-temperature phase. We provide several examples explaining how the proofs work in Section 3 of the paper. To obtain similar results for any other system, the user should follow two relatively simple steps:

1. Define the hat-tensor for the system under study. The tensor should have dimensions $4,2,4,2$ (the order of legs as in Eq. 2.1 in the paper) with indices corresponding to sectors $\mathbf{o}, \mathbf{d}, \mathbf{u}, \mathbf{r}$ on the horizontal legs and $\mathbf{o}, \mathbf{x}$ on the vertical legs (see Section 2.3.1 in the paper). It is often simpler to define a hat-tensor with dimensions $2,2,2,2$ whose indices correspond to sectors $\mathbf{o}$ and $\mathbf{x}$ on both horizontal and vertical legs, and then run a preliminary RG step, as done for the Ising and XY examples in the paper and in the notebook. This yields a natural decomposition of the horizontal $\mathbf{x}$ sector into $\mathbf{u} \oplus \mathbf{d} \oplus \mathbf{r}$.

2. Iterate the master_function (also available as the alias 𝔐) provided in HT.ipynb, starting from the defined hat-tensor. After a few iterations, check whether the tensor element trajectories generated by master_function all begin to decay simultaneously.

   1. If yes, the proof is complete and the system is in the high-temperature phase (see details in Section 2.5 of the paper). To make the result fully rigorous, compute the $\lambda$ value (see Eq. 2.30 in the paper) using interval arithmetic to ensure that accumulated roundoff errors do not affect the outcome.
   2. If no, try do more master function iterations, or try using a tensor corresponding to a higher temperature, or adjust the $w_{\mathbf{x}}$ and $w_{\mathbf{o}}$ parameters of the algorithm. Unfortunately, we do not provide an algorithm for optimizing the choice of $w_{\mathbf{x}}$ and $w_{\mathbf{o}}$.

NB: One does not need to run the whole notebook in order to define master_function. It is enough to run the cells in the section "RG map and master function" only.