What Theorem 12.2 rests on

The proof graph of part_i/main.tex, generated from its own \ref edges

What is happening

Each box is a numbered statement; each edge is a reference that statement or its proof actually makes. Nothing here is curated: docs/extract.py reads the manuscript, resolves numbers through its .aux, and takes the edges from the \ref and \eqref commands. Columns are sections, left to right.

Turn off U_GJS. A8 is the Glimm–Jaffe–Spencer package, and its item (vi) — U_GJS — is the one import that is not a literal quotation of a printed theorem. Switch it off and every statement whose proof chain reaches A8 is greyed. What remains standing is what Part I proves unconditionally.

Assumptions are leaves of this graph: they are hypotheses, not derived statements, so the closure stops at A1–A8 rather than running on through whatever their own text happens to cite. That is why the filter lemma comes out independent of A8 — it is operator theory and Fourier analysis, and it does not ask GJS for anything.

Full statements, provenance and page numbers: the result inventory. What U_GJS is and is not: imports.