%======================================================================
\section{Findings about the paper}\label{s:findings}

We recorded $70$ entries about version 1 of [U1]: $5$ errors, $11$ gaps and $11$ unstated hypotheses, besides $43$ points
of presentation, notation or simplification. They include every place where the formalization, the written-out proofs,
their referee reports or the audits found a statement or proof wrong, incomplete or relying on something unstated. For each, the list gives replacement text for [U1] and, where it applies, how the formal proof
and the written-out proofs treat it. No entry changes
Theorem~\ref{thm:main} or its corollaries, and where an entry changes a statement of [U1], the paper's proofs already use the new
statement. The list is the file \lean{changes.md} of the record [repo], and \lean{PROVENANCE.md} there says for each entry where it was
found and which documents are involved, among them the findings ledger \lean{FINDINGS.md} of the Lean archive. Versions 2 and later of [U1] apply every entry
that is not marked optional.

The five errors are statements or proof steps that are false as written. Display (A.3) takes the supremum over the
interpolation parameters inside the sum over elementary terms, while Proposition A.7 combines all terms with one link datum and
bounds that combination uniformly in the parameters, which needs the supremum outside the sum; the corrected form has the
same proof and the same constants. Section D.3(c) bounds the number of points at graph distance $k$ in a slit graph by
$4k^2+2$, the size of an $\ell^1$-sphere of $\mathbb Z^3$, which fails on slit graphs: in a three-dimensional H-tree the sphere
of radius $189$ about the root has $2^{18}=262144$ points, while $4\cdot189^2+2=142886$. What the proof uses is the bound
$\sum_ye^{-a\,d(x,y)}\le64a^{-3}$ for $0<a\le2$, which follows directly from $d\ge\|\cdot\|_1$. Proposition 7.22 is stated for
a label on a region, which does not determine the objects of the expansion; it is proved and used for wall fields, and the
fix states it for them. In Lemma 7.29(f), the claim that the ratios $\mathcal Z_p(X)/Z$ are unchanged holds only for
$X=\emptyset$; the error is harmless, since from Lemma 7.29 on the paper builds every activity and every $\mathcal Z_p(X)$ with
the modified objects. Finally, the growth constant $K_g$ of Appendix B, and the same count after display (A.9), omit the
rounding to lattice cells; only the independence of $K_g$ from $\tau$ is used later, so nothing else changes.

The eleven gaps are steps that are missing or only asserted. Among them, Lemma 3.5 is stated without proof; the
reference density of Section 6 is taken in infinite volume, where the paper neither defines it as a limit over finite volumes
nor proves the bound it uses; Lemma C.1 and
Proposition 7.22 use charge moments that the paper does not state; absolute convergence in Theorem 7.27 is proved only for
the objects built with the modified covariance, which are the only ones used later; and display (A.9) puts a distance factor
on links of the first type, which have no covariance line, so that Proposition B.7 cannot pay for it. The fix drops the
factor for these links, and since the count of link data (Lemma A.6) never uses it, all constants are unchanged. Among the
simplifications is the sharper counting factor $2^{4|C|+2}$ in the tail bound of Theorem 5.1, noted in \S\ref{ss:mincut}.

\paragraph{Findings about the sources.} The paper already records its corrections to [B78] and [BF80] (in the proof of
Lemma A.1, in Remark A.5 and in Proposition A.7), and the formal proof uses them. The referee report on the written-out proof of
Appendix A found one more, which [U1] has recorded in Remark A.5 since version 2: in [BF80, pp.~213--217] the sums are
listed in the reverse of the order in which they are performed, so the constraint of the step 3$\Sigma$, that each set
contain one of the cubes ``mentioned in 10$\Sigma$'', refers to the variable of an inner sum. The count of Proposition A.4 instead uses a valid order, in which each constraint links a variable only to
variables outer to it.