%======================================================================
\section{Written-out proofs and their refereeing}\label{s:blueprints}

The steps of [U1] that carry arguments of [GM82] and [BF80, Section 9] over to slit domains, with constants made explicit,
cannot be formalized until the adapted arguments are written out. We therefore wrote out each of these parts as a self-contained document, which the formalization then followed. Six documents
do this, for Stage 1 (Section 6, with Appendix D and the supplement), Subsections 7.0--7.5, Proposition 7.22 with
Appendix C, Subsection 7.6, Appendix B, and Subsections 7.7--7.9 with Appendix A. Three more write out the steps that
[U1] omits in Sections 3--4, the contour bound of Section 5 and the measure theory of Section 9. The nine documents have
233 pages in all.

All the documents have the same form. Each states its inputs (the results it takes from other parts) precisely and in the
form in which it uses them, and its outputs (the results it supplies to other parts). Every step is marked as taken unchanged from
a source, proved in full, or an input; a step taken from a source is cited by equation and page, and equations quoted from
the sources carry page references. If a step could not be completed, it is marked as a gap, with the missing piece stated.
Results of [U1] are cited by their numbers there.

Each document has a referee report, written with generative AI tools separately from the writing of the document it
checks. Each report re-derives all proofs line by line, recomputes all constants, checks that each input is proved
elsewhere or assigned to another part, and lists its findings by severity. The reports check the quoted equations
against the sources or against notes that transcribe them, apart from a few that they take as cited. We archive each document with the corrections made after its review,
together with its referee report, in the record [repo]. The current versions, with the
corrections of the findings list applied, form Part S4 of [U1]. The findings that concern [U1] itself are in the list
of findings.

In Lean, the modules of Sections 3--7 follow the documents statement by statement. The
interfaces of these modules are the documents' inputs and outputs, and their docstrings cite the document's statement and the paper result.
The documents also go beyond the paper in places. For example, they state the seeded sums of Lemma 7.48 for a class of wall
fields defined by local primitives. The fixes made in the documents are among the findings.