Companion data and code for "Long-lived local coherences at high temperature from frozen domain walls"

Companion data and code for “Long-lived local coherences at high temperature from frozen domain walls”, by S. Gopalakrishnan and R. Vasseur (arXiv:2610.20724). This archive contains the machine-checked proof and the figure data for the paper and its Supplemental Material. Lean 4 proof (folder MazurProof_lean). This is a complete machine-checked proof of the static overlap inequality <sigma_x^- R> >= p_{L,x} (Supplemental Material Eq. (15), proved in Supp. Mat. Appendix A), where R is the canonical polar factor of the quantum-group raising generator. The inequality is proved for every chain length L, every site x and every q >= 1, using Lean 4.24 and Mathlib, with no unproved steps and no custom axioms. It can be reproduced by running “bash verify.sh”. This inequality is the input to the Mazur bound used in the paper. License: Apache 2.0. Figure data (folder figure_data). The plotted data are given as plain CSV files for Fig. 2 (quantum-group and Fredkin chains: infinite-time averages and Mazur bounds), Fig. 3 (folded and finite-Delta XXZ chains) and Supplemental Fig. 1 (check of the non-undershoot assumption). Each file begins with comment lines giving the panel, the model and its parameters, and the method used (exact diagonalization, dynamical typicality or Slater-determinant Monte Carlo). The Fig. 3 folder also includes the Python scripts that process the raw data and draw the figure.