Removal of the spatial cutoff for weakly coupled P(phi)_2

Result inventory

Every numbered statement of part_i/main.tex, in order, generated by docs/extract.py from the manuscript and its .aux. Do not edit by hand.

imports A8 marks a statement whose own proof chain reaches Assumption A8, the GJS package. Item A8(vi) of that package is U_GJS, the single import that is not a literal quotation of a printed theorem, so everything marked here inherits the conditionality of Theorem 12.2. cites U_GJS marks the narrower set that reaches the displayed inequality itself.

#	kind	statement	section	p.	imports A8	cites U_GJS
2.1	Definition	cutoff classes	2 Setting, notation, and standing imports	6	-	-
A1	Assumption	cutoff construction	2 Setting, notation, and standing imports	7	-	-
A2	Assumption	Feynman–Kac–Nelson transfer	2 Setting, notation, and standing imports	8	-	-
A3	Assumption	finite-volume stability	2 Setting, notation, and standing imports	8	-	-
A4	Assumption	free hypercontractivity	2 Setting, notation, and standing imports	8	-	-
A5	Assumption	domain smoothing; common core	2 Setting, notation, and standing imports	8	-	-
A6	Assumption	free propagation; patching; the dynamics $\alpha$	2 Setting, notation, and standing imports	9	-	-
A7	Assumption	covariance data	2 Setting, notation, and standing imports	9	-	-
A8	Assumption	the GJS package	2 Setting, notation, and standing imports	9	yes	yes
2.2	Source Fact	CE2 $=$ {\cite[Thm.~1.1.7]{GJS}}, p.~594	2 Setting, notation, and standing imports	10	-	-
2.3	Source Fact	CE1 $=$ {\cite[Thm.~1.1.8]{GJS}}, p.~595	2 Setting, notation, and standing imports	10	-	-
2.4	Source Fact	{\cite[p.~629, \S4]{GJS}}	2 Setting, notation, and standing imports	10	-	-
2.5	Remark	conventions lock	2 Setting, notation, and standing imports	12	-	-
2.6	Proposition	domain smoothing at the ground state	2 Setting, notation, and standing imports	12	-	-
2.7	Proposition	cutoff propagation, uniformly in $g$	2 Setting, notation, and standing imports	12	-	-
2.8	Lemma	covariance and parity of the cutoff states	2 Setting, notation, and standing imports	12	-	-
3.1	Lemma	class compatibility	3 Dimensionless weak-coupling reduction	13	-	-
3.2	Proposition	dimensionless weak-coupling reduction	3 Dimensionless weak-coupling reduction	13	yes	yes
3.3	Remark	coordinate convention and transport of the conclusions	3 Dimensionless weak-coupling reduction	14	yes	yes
4.1	Lemma	slab FKN; bounded nonnegative arguments	4 Slab transfer	15	-	-
4.2	Lemma	signed bounded extension	4 Slab transfer	15	-	-
4.3	Lemma	unbounded extension	4 Slab transfer	15	yes	yes
4.4	Lemma	slab vacuum; simplicity only	4 Slab transfer	16	-	-
5.1	Theorem	uniform local interaction moment (M$_2$)	5 The uniform local interaction moment	16	yes	yes
5.2	Corollary	$\varphi^4$ instance	5 The uniform local interaction moment	17	-	-
6.1	Lemma	cell count	6 GJS norms of sharp-time polynomial observables	17	-	-
6.2	Proposition	GJS norms of polynomial observables	6 GJS norms of sharp-time polynomial observables	18	yes	-
6.3	Remark	row independence	6 GJS norms of sharp-time polynomial observables	18	-	-
7.1	Lemma	moment transfer	7 The uniform gap	18	yes	yes
7.2	Lemma	one-point limit	7 The uniform gap	18	yes	yes
7.3	Lemma	two-point lower semicontinuity	7 The uniform gap	19	yes	yes
7.4	Lemma	CE2 across a horizontal strip	7 The uniform gap	19	-	-
7.5	Proposition	semigroup decay of centered observables	7 The uniform gap	20	yes	yes
7.6	Lemma	exponential moments	7 The uniform gap	20	yes	yes
7.7	Theorem	density of polynomial vectors	7 The uniform gap	21	yes	yes
7.8	Theorem	uniform gap (G)	7 The uniform gap	21	yes	yes
8.1	Proposition	path regularity of the semigroup	8 Affine-path regularity	22	-	-
8.2	Proposition	projection and eigenvector regularity; derivative formulas	8 Affine-path regularity	23	-	-
9.1	Lemma	exact inverse-energy filter	9 Filter, spectral separation, and clustering	24	-	-
9.2	Lemma	spectral separation	9 Filter, spectral separation, and clustering	25	-	-
9.3	Lemma	clustering with one unbounded local argument	9 Filter, spectral separation, and clustering	25	-	-
10.1	Lemma	state derivative	10 The one-path LPPL estimate	26	-	-
10.2	Lemma	localization of the perturbation	10 The one-path LPPL estimate	26	yes	yes
10.3	Lemma	two-regime bound	10 The one-path LPPL estimate	27	yes	yes
10.4	Proposition	one-path estimate	10 The one-path LPPL estimate	27	yes	yes
10.5	Lemma	the rate function is super-polynomial	10 The one-path LPPL estimate	28	yes	yes
11.1	Theorem	full-net convergence with rate	11 Convergence of the full net; local normality	28	yes	yes
11.2	Proposition	local normality	11 Convergence of the full net; local normality	29	yes	yes
12.1	Proposition	exact spectral passage	12 Ground state, invariances, and the Main Theorem	29	-	-
12.2	Theorem	Main Theorem	12 Ground state, invariances, and the Main Theorem	30	yes	yes
12.3	Corollary	the Glimm–Jaffe vacuum is canonical at weak coupling	12 Ground state, invariances, and the Main Theorem	31	yes	yes
13.1	Hypothesis	structure of a broken phase	13 The two-phase dichotomy	31	-	-
13.2	Theorem	conditional exclusion of a two-phase structure	13 The two-phase dichotomy	31	yes	yes
13.3	Remark	scope of the phase-transition literature	13 The two-phase dichotomy	32	yes	yes
C.1	Proposition	consequence of the audited source mechanisms	C $h$-uniformity: source audit and analytic prerequisites	36	-	-
C.2	Lemma	normalisation	C $h$-uniformity: source audit and analytic prerequisites	37	-	-
C.3	Lemma	Wick lower bound; the $h\ge0$ entry	C $h$-uniformity: source audit and analytic prerequisites	37	-	-
C.4	Lemma	ultraviolet difference; the $h\le1$ entry	C $h$-uniformity: source audit and analytic prerequisites	37	-	-
C.5	Theorem	$h$-uniform stability	C $h$-uniformity: source audit and analytic prerequisites	38	-	-
C.6	Remark	why the class is what it is	C $h$-uniformity: source audit and analytic prerequisites	38	-	-
C.7	Proposition	coverage of every CE application	C $h$-uniformity: source audit and analytic prerequisites	38	yes	yes

Statements

The one-path LPPL estimate

Lemma 10.1 (state derivative)

lem:statederiv · page 26 · proof in the manuscript

For self-adjoint $A\in B(\HH)$ and $0<s<1$,
\begin{equation}
 \frac d{ds}\,\omega_{g_s}(A)
 =-2\,\mathrm{Re}\int_\R W_\gamma(t)
 \Bigl[\ip{V(v)\Om_s}{\beta^{g_s}_t(A)\Om_s}
 -\ip{V(v)\Om_s}{\Om_s}\,\omega_{g_s}(A)\Bigr]dt ,
 \label{eq:statederiv}
\end{equation}
and the integral converges absolutely.

Provenance: src: lamport_gap_to_main.tex <1>5 <2>1 (3.15); filter sign +1/E. Uses: lem:filter, prop:projreg, prop:smoothing

Lemma 10.2 (localization of the perturbation)

lem:localize · page 26 · imports A8 · proof in the manuscript

Choose a smooth partition of unity $\sum_{j\in\Z}\eta_j=1$ with $0\le\eta_j\le1$ and
$\supp\eta_j\subset(j-1,j+1)$, and set $h_j:=\eta_jv$, $V_j:=V(h_j)$, $B_j:=\supp h_j$.
Then only finitely many $h_j$ are nonzero,
\begin{equation}
 V(v)\xi=\sum_jV_j\xi
 \quad\text{on common domains},\qquad
 \|V_j\Om_s\|\le M\quad(0\le s\le1).
 \label{eq:localize}
\end{equation}

Provenance: src: lamport_gap_to_main.tex <1>5 <2>2 (3.16). Uses: lem:classes, thm:M2

Lemma 10.3 (two-regime bound)

lem:tworegime · page 27 · imports A8 · proof in the manuscript

Let $A=A^*\in\A(O)$ with $\|A\|\le1$, and for a nonzero $h_j$ put
$r_j:=\dist(B_j,O)$ and
\[
 C_{j,s}(t):=\ip{V_j\Om_s}{\beta^{g_s}_t(A)\Om_s}
 -\ip{V_j\Om_s}{\Om_s}\,\omega_{g_s}(A) .
\]
If $\gamma r_j/2\ge1$, then
\begin{equation}
 |C_{j,s}(t)|\le
 \begin{cases}
 2Me^{-\gamma r_j/4},&|t|\le r_j/2,\\[2pt]
 2M,&t\in\R .
 \end{cases}
 \label{eq:tworegime}
\end{equation}

Provenance: src: lamport_gap_to_main.tex <1>6 <2>2 (3.17). Uses: lem:cluster, lem:localize, prop:propagation, prop:smoothing

Proposition 10.4 (one-path estimate)

prop:onepath · page 27 · imports A8 · proof in the manuscript

Let $d\ge d_0:=4+2/\gamma$ and suppose $g\equiv g'\equiv1$ on $O_d$. Then
\begin{equation}
 \|(\omega_g-\omega_{g'})|_{\A(O)}\|
 \le32M\sum_{n\ge\lfloor d\rfloor}
 \Bigl(\|W_\gamma\|_1e^{-\gamma n/4}+T_\gamma(n/2)\Bigr) .
 \label{eq:onepath}
\end{equation}

Provenance: src: lamport_gap_to_main.tex <1>6 (3.18)-(3.19). Uses: lem:localize, lem:statederiv, lem:tworegime, prop:projreg

Lemma 10.5 (the rate function is super-polynomial)

lem:rate · page 28 · imports A8 · proof in the manuscript

Define
\begin{equation}
 \Psi_\gamma(d):=
 \begin{cases}
 \displaystyle
 32M\sum_{n\ge\lfloor d\rfloor}
 \Bigl(\|W_\gamma\|_1e^{-\gamma n/4}+T_\gamma(n/2)\Bigr), & d\ge d_0,\\[6pt]
 \max\Bigl\{2,\ \text{the same expression}\Bigr\}, & 0\le d<d_0 .
 \end{cases}
 \label{eq:Psidef}
\end{equation}
Then for every $N\ge1$ there is $C_{N,\gamma,M}<\infty$ with
\begin{equation}
 \Psi_\gamma(d)\le C_{N,\gamma,M}\,(1+d)^{-N}\qquad(d\ge0) .
 \label{eq:Psitail}
\end{equation}
In particular $\|(\omega_g-\omega_{g'})|_{\A(O)}\|\le\Psi_\gamma(d)$ whenever
$g\equiv g'\equiv1$ on $O_d$, $d\ge0$.

Provenance: src: lamport_gap_to_main.tex <1>7 (3.20)-(3.21). Uses: lem:filter, prop:onepath

Convergence of the full net; local normality

Theorem 11.1 (full-net convergence with rate)

thm:cauchy · page 28 · imports A8 · proof in the manuscript

Let $0\le\lambda/m_0^2<\varepsilon_{\mathscr P}$. There is a state $\omega_\infty$ on $\A$
such that, for every bounded open interval $O$,
\[
 \lim_{g\in\G}\bigl\|(\omega_g-\omega_\infty)|_{\A(O)}\bigr\|=0 ,
\]
and
\begin{equation}
 \|(\omega_g-\omega_\infty)|_{\A(O)}\|\le\Psi_{m_1}(d)
 \qquad\text{whenever }g\equiv1\text{ on }O_d .
 \label{eq:rate}
\end{equation}

Provenance: src: lamport_gap_to_main.tex <1>8. Uses: lem:rate, prop:onepath

Proposition 11.2 (local normality)

prop:normal · page 29 · imports A8 · proof in the manuscript

$\omega_\infty|_{\A(O)}$ is normal for every bounded open interval $O$.

Provenance: src: lamport_gap_to_main.tex <1>9 (3.23). Uses: thm:cauchy

Ground state, invariances, and the Main Theorem

Proposition 12.1 (exact spectral passage)

prop:spectral · page 29 · proof in the manuscript

If $(g_n)\subseteq\G$ satisfies $d(g_n,O)\to\infty$ for every bounded interval $O$, and
$\omega_{g_n}\to\omega$ in norm on every $\A(O)$, then $\omega$ is a ground state of
$(\A,\alpha)$ in the spectral sense: $\omega\circ\alpha_t=\omega$ for all $t$; the
function $t\mapsto\omega(A\alpha_t(B))$ is continuous and bounded for all $A,B\in\A$; and
\[
 \int_\R f(t)\,\omega(A\alpha_t(B))\,dt=0
\]
for every $f\in L^1(\R)$ whose transform $\check f(E)=\int f(t)e^{itE}\,dt$ vanishes on
$[0,\infty)$.

Provenance: src: m6/main.tex prop:M0-main(i) (v2), transcribed; = lamport_gap_to_main.tex <1>10.

Theorem 12.2 (Main Theorem)

thm:MAIN · page 30 · imports A8 · proof in the manuscript

Assume $U_{\rm GJS}$, namely Assumption~\ref{A:gjs}(vi), and let
$0\le\lambda/m_0^2<\varepsilon_{\mathscr P}$. Then there is a state $\omega_\infty$ on $\A$
such that:
\begin{enumerate}
\item[\rm(1)] \emph{(full-net convergence with rate)} for every bounded open interval $O$,
      $\lim_{g\in\G}\|(\omega_g-\omega_\infty)|_{\A(O)}\|=0$, and
      $\|(\omega_g-\omega_\infty)|_{\A(O)}\|\le\Psi_{m_1}(d)$ whenever $g\equiv1$ on $O_d$,
      with $\Psi_{m_1}$ decaying faster than every inverse power;
\item[\rm(2)] \emph{(local normality)} $\omega_\infty|_{\A(O)}$ is normal for every $O$;
\item[\rm(3)] \emph{(ground state)} $\omega_\infty$ is a ground state of $(\A,\alpha)$ in the
      spectral sense;
\item[\rm(4)] \emph{(invariances)} $\omega_\infty\circ\tau_a=\omega_\infty$ for all $a\in\R$;
      and for even $\mathscr P$, $\omega_\infty\circ\theta=\omega_\infty$;
\item[\rm(5)] \emph{(spectra and local moment)}
      \[
       \spec H(g)\subseteq\{0\}\cup[m_1,\infty)\quad(g\in\CH),
       \qquad \dim\ker H(g)=1,
      \]
      and $\sup_{g\in\CH}\|V(h)\Om_g\|\le M$ for real $h$ with $\|h\|_\infty\le1$ supported
      in an interval of length $2$.
\end{enumerate}
The nonstandard weak-coupling estimates imported are printed GJS Theorem 1.1.7 and
the moment estimate of Theorem 1.1.8 in its working-family form $U_{\rm GJS}$
(Assumption~\ref{A:gjs}(vi), imported at the scope at which the source states and uses
it; Scope paragraph and item~(vii$'$) there).  Appendix~\ref{app:huniform} supplies
supporting scope evidence and analytic prerequisites but is not an independent proof
of the cluster expansion. In addition, the proof uses the
separately identified standard cutoff-construction inputs of
Assumptions~\ref{A:cutoff}--\ref{A:covar}. Proposition~\ref{prop:scaling} verifies that the
dimensionless weak-coupling hypothesis implies the source smallness condition. The theorem is conditional
on exactly this list, including $U_{\rm GJS}$; no other external input is used.

Provenance: src: m6/main.tex thm:MAIN (v2), transcribed; import references adapted to (A1)-(A8); Uses: A:covar, A:cutoff, A:gjs, lem:covparity, prop:normal, prop:scaling, prop:spectral, thm:G, thm:M2, thm:cauchy

Corollary 12.3 (the Glimm–Jaffe vacuum is canonical at weak coupling)

cor:canonical · page 31 · imports A8 · proof in the manuscript

Every $w^*$ limit point of the (averaged or unaveraged) finite-volume ground states
constructed in \cite[\S2]{GJ3} coincides on each $\A(O)$ with $\omega_\infty$; in
particular the construction of \cite{GJ3} is subsequence- and averaging-independent in the
weak-coupling region.

Provenance: src: m6/main.tex cor:canonical (v2), transcribed. Uses: thm:MAIN

The two-phase dichotomy

Hypothesis 13.1 (structure of a broken phase)

hyp:broken · page 31

$\mathscr P$ is even, and:
\begin{enumerate}
\item[\rm(B1)] there are translation-invariant ground states $\omega_+$ and $\omega_-$ of
      $(\A,\alpha)$ such that, for all bounded local $X,Y$,
      \[
       \omega_\pm(X\tau_a(Y))-\omega_\pm(X)\,\omega_\pm(\tau_a(Y))
       \longrightarrow0\qquad(|a|\to\infty);
      \]
\item[\rm(B2)] $\omega_+\circ\theta=\omega_-$ and $\omega_-\circ\theta=\omega_+$;
\item[\rm(B3)] there are a bounded local observable $B=B^*\in\A(O)$ and $m\ne0$ such that
      $\omega_\pm(B)=\pm m$;
\item[\rm(B4)] every $\theta$-invariant ground state of $(\A,\alpha)$ equals
      $\tfrac12(\omega_++\omega_-)$.
\end{enumerate}

Provenance: src: m6/main.tex cor:nobreak items (B1)-(B4) (v2); m3/m3.tex hyp:broken states (B4)

Theorem 13.2 (conditional exclusion of a two-phase structure)

thm:dichotomy · page 31 · imports A8 · proof in the manuscript

Assume that $\mathscr P$ is even and $0\le\lambda/m_0^2<\varepsilon_{\mathscr P}$. Then
the assertions {\rm(B1)}--{\rm(B4)} of Hypothesis~\ref{hyp:broken} cannot hold
simultaneously.

Provenance: src: m6/main.tex cor:nobreak (v2), statement transcribed. Uses: hyp:broken, lem:cluster, thm:G, thm:MAIN

Remark 13.3 (scope of the phase-transition literature)

rem:gjs7576 · page 32 · imports A8

The GJS phase-transition and mean-field papers \cite{GJS75,GJS76} prove the existence of
phase transitions and of two pure phases in specified strong-coupling regimes. As cited
here, they are context: they do not, by themselves, supply the full Hamiltonian
phase-space classification (B1)--(B4) --- in particular not the midpoint identification
(B4) --- for the state space of $(\A,\alpha)$. This manuscript therefore makes no
unconditional assertion that its state space carries the structure of
Hypothesis~\ref{hyp:broken}; Theorem~\ref{thm:dichotomy} says only that, at weak coupling,
that structure cannot coexist with the cutoff-uniform gap. The two rigorous options
recorded by the audit --- state (B1)--(B4) explicitly, or delete the corollary --- are
resolved here by the first.

Provenance: src: lamport_gap_to_main.tex \S6; audit \S4-\S5. Uses: hyp:broken, thm:dichotomy

Setting, notation, and standing imports

Definition 2.1 (cutoff classes)

def:classes · page 6

\begin{align*}
 \CE&:=\{h:\R^2\to[0,1]\ \text{measurable},\ \supp h\ \text{compact}\}
 &&\text{(Euclidean class)},\\
 \CH&:=\{g:\R\to[0,1]\ \text{measurable},\ \supp g\ \text{compact}\}
 &&\text{(Hamiltonian class)},\\
 \G&:=\{g\in C_c^\infty(\R):0\le g\le1,\ g\equiv1\ \text{on a nonempty open interval}\}
 &&\text{(plateau net class)}.
\end{align*}
The first two are the printed classes of \cite[p.~589]{GJS} and
\cite[(1.6), p.~588]{GJS}, respectively.
$\G$ is directed by $g\preccurlyeq g'\iff\{g=1\}^\circ\subseteq\{g'=1\}^\circ$. For a bounded
interval $O$ and $r\ge0$ set
\[
 O_0:=O,\qquad O_r:=\{x\in\R:\dist(x,O)<r\}\quad(r>0),\qquad
 d(g,O):=\dist\bigl(O,\R\setminus\{g=1\}^\circ\bigr).
\]

Assumption A1 (cutoff construction)

A:cutoff · page 7

For every $g\in\CH$: $K(g)=H_0+V(g)$ is essentially self-adjoint and bounded below; its closure
(again denoted $K(g)$) has $E(g)=\inf\spec K(g)$ as a \emph{simple} eigenvalue, and the
normalized eigenvector $\Om_g$ may be chosen strictly positive $d\phi_0$-a.e.\ in $Q$-space.
For every real $h\in L^1\cap L^2$ of compact support, $V(h)$ is self-adjoint on its maximal
multiplication domain.

\emph{Sources.} \cite[p.~588]{GJS}; existence and uniqueness of the cutoff vacuum:
\cite[Thms.~2.2.1, 2.3.1]{GJ2}; lower bounds and positivity: \cite{GJ71}; the semigroup
construction: \cite[Thm.~5.3]{Rosen70}.

\emph{Scope.} Strict positivity of $\Om_g$ is the standard positivity-improving semigroup
argument of the cited construction; simplicity is used below only through the two consequences
$c_g:=\ip{\Om_g}{\Om_0}>0$ and the absence of a second ground vector. \emph{Isolation of
$E(g)$ (a gap) is not imported}; the gap of \S\ref{sec:G} is an output.

\emph{Used in.} \S\ref{sec:slab} (slab limits), \S\ref{sec:M2} (weak-graph passage),
\S\ref{sec:G} (density, spectral projections), \S\ref{sec:path} (simple Perron root),
\S\ref{sec:ground} and \S\ref{sec:dichotomy} (covariance and parity via
Lemma~\ref{lem:covparity}).

{\raggedright\emph{Dossier.} \texttt{gj2-ground-existence-08}, \texttt{gjii-ground-12},
\texttt{gj71-lower-bound-02}, \texttt{gj71-theorem2-04}, \texttt{rosen-semigroup-22},
\texttt{rosen-selfadjoint-23}, \texttt{gjs-source-05/06} (E04--E06, E10--E13, E20).\par}

Uses: lem:covparity

Assumption A2 (Feynman–Kac–Nelson transfer)

A:fkn · page 8

Let $d\mu_0$ be the free Euclidean Gaussian measure with covariance
$(-\Delta_{\R^2}+m_0^2)^{-1}$, $J_t$ the sharp-time embeddings, and, for $h\in\CE$,
$\mathcal U_h:=\lambda\int h(z){:}\mathscr P(\Phi(z)){:}\,dz$. For all bounded time-zero
functions $f,h'$, $T>0$, and $g\in\CH$,
\[
 \ip{f}{e^{-TK(g)}h'}
 =\int\overline{(J_Tf)}\,(J_0h')\,e^{-\mathcal U_{\mathbf 1_{[0,T]}\otimes g}}\,d\mu_0 ,
\]
with the interaction over exactly the slab $[0,T]$ carrying the two embeddings, together
with the analogous multi-time formulas on finite slabs (used in \S\ref{sec:slab} in the
two- and one-time forms, where the symmetric slab cutoffs
$h_{T,g}:=\mathbf 1_{[-T,T]}\otimes g\in\CE$ enter through the \emph{normalized}
measures $dq_{h_{T,g}}$).

\emph{Sources.} Free-field FKN: \cite[Thm.~III.6]{SimonBook}; interacting form:
\cite[Cor.~V.14, Thm.~V.15]{SimonBook}; equivalently \cite[Thms.~II.14, II.16]{GRS75}.

\emph{Scope.} \cite[Thm.~III.12]{SimonBook} is a projection-product estimate, % negative-scope mention (whitelisted): III.12
\emph{not} an FKN theorem, and is nowhere used (audit finding S1).
The identification of sharp-time Wick functionals with $Q$-space multiplication operators is
the conventions lock, Remark~\ref{rem:conv}.

\emph{Used in.} \S\ref{sec:slab} (slab identities), \S\ref{sec:path} (path formula).

{\raggedright\emph{Dossier.} \texttt{simon-free-fkn-111}, \texttt{simon-fkn-184/185},
\texttt{grs-fkn-39/40}, \texttt{simon-wrong-iii12-119} (E27--E43 range).\par}

Uses: rem:conv

Assumption A3 (finite-volume stability)

A:stability · page 8

For every $h\in\CE$: $\mathcal U_h\in L^p(d\mu_0)$ for every $p<\infty$, and
$e^{-\varrho\,\mathcal U_h}\in L^1(d\mu_0)$ for every finite $\varrho>0$. In particular
$0<Z(h):=\int e^{-\mathcal U_h}d\mu_0<\infty$, and the interacting measures
\[
 dq_h:=Z(h)^{-1}e^{-\mathcal U_h}\,d\mu_0 ,\qquad h\in\CE ,
\]
are well-defined probability measures.

\emph{Source.} \cite[Thm.~V.7]{SimonBook} and its chapter context.

\emph{Scope.} Only finite slabs and compactly supported $h$ occur below; no infinite-volume
stability is imported. A self-contained quantitative lower bound on $Z(h)$ and the
$h$-uniform $L^p$ bound on $e^{-\mathcal U_h}$ are re-proved in Appendix~\ref{app:huniform}.

\emph{Used in.} \S\ref{sec:reduction} (Lemma~\ref{lem:classes}), \S\ref{sec:slab},
\S\ref{sec:path} (H\"older/Vitali chains), Appendix~\ref{app:huniform}.

{\raggedright\emph{Dossier.} \texttt{simon-exp-174}, \texttt{simon-transfer-178/179/180} (E33--E43 range).\par}

Uses: lem:classes

Assumption A4 (free hypercontractivity)

A:hyper · page 8

The free time-zero Markov semigroup $\mathsf P_T$ satisfies
\[
 \|\mathsf P_TF\|_{q}\le\|F\|_{p}
 \qquad\text{whenever}\qquad \frac{q-1}{p-1}=e^{2m_0T},\quad 1<p\le q<\infty .
\]

More generally (the abstract form of the same source): for the second quantization
$\Gamma(c)$ of a contraction $c$ on the one-particle space of any Gaussian $L^2$-space,
$\|\Gamma(c)F\|_{q}\le\|F\|_{p}$ whenever $\|c\|^2\le(p-1)/(q-1)$; the display is the
case $c=e^{-T\mu}$, and the Mehler case $c=e^{-t}\mathbf 1$ on $L^2(d\mu_0)$ is the form
used in Appendix~\ref{app:huniform}.

\emph{Sources.} \cite[Thm.~I.17]{SimonBook} (abstract form and the display); time-region
form \cite[Thm.~III.17]{SimonBook}.

\emph{Scope.} \cite[Thms.~V.10, V.12]{SimonBook} are, respectively, a transfer-matrix % negative-scope mention (whitelisted): V.10, V.12
application and an essential-self-adjointness theorem; neither is the hypercontractivity input
and neither is cited for it (audit finding S2).

\emph{Used in.} \S\ref{sec:path} (the pairing bound), Appendix~\ref{app:huniform} (tail
estimate).

{\raggedright\emph{Dossier.} \texttt{simon-hyper-056}, \texttt{simon-timeslice-125/126}.\par}

Assumption A5 (domain smoothing; common core)

A:domain · page 8

\emph{(i)} For every $g\in\CH$ and $t>0$,
\[
 \Ran e^{-tK(g)}\subseteq D(H_0)\cap D(V')
\]
for every polynomial multiplication operator $V'$ of the time-zero field with coefficients in
$L^1\cap L^2$ of compact support (in particular for every $V(h)$ as in
\S\ref{subsec:model}).
\emph{(ii)} For every affine path $g_s=(1-s)g+sg'$, $g,g'\in\G$, there is a common core
$\mathscr C$ for all $K(g_s)$, $s\in[0,1]$, on which
$K(g_s)\xi=K(g_{s_0})\xi+(s-s_0)V(g'-g)\xi$.

\emph{Sources.} (i) is the model-specific smoothing theorem \cite[Ch.~7, Thm.~7.4]{GJExp}.
(ii) is part of the cutoff construction; essential self-adjointness pinpoints, in their
roles per the audit: \cite[Thm.~V.12]{SimonBook}, \cite[Thm.~5.3]{Rosen70}, \cite{GJ2}. % whitelisted: V.12 in its audited positive role (esa), not the S2 misuse

\emph{Scope.} \cite[Thm.~7.3]{GJExp} alone assumes a potential bounded below % negative-scope mention (whitelisted): Thm. 7.3
and is therefore \emph{not} sufficient here; the citation is to Theorem~7.4
(audit finding S3).

\emph{Used in.} Proposition~\ref{prop:smoothing}, \S\ref{sec:slab} (dominators),
\S\ref{sec:path} (eigenvalue differentiation).

{\raggedright\emph{Dossier.} \texttt{gjexp-domain-165/166/167} (E17--E19).\par}

Uses: prop:smoothing

Assumption A6 (free propagation; patching; the dynamics $\alpha$)

A:patch · page 9

\emph{(i)} The free dynamics $\mathrm{Ad}\,e^{itH_0}$ has propagation speed one
(Klein--Gordon finite propagation), and the Trotter product formula for $e^{itK(g)}$ converges
strongly.
\emph{(ii)} There is a one-parameter automorphism group $\alpha$ of $\A$, independent of $g$,
with
\begin{equation}
 \alpha_t(\A(O))\subseteq\A(O_{|t|}),\qquad
 \alpha_t(A)=\beta^g_t(A)\ \ \text{if } g\equiv1 \text{ on } O_{|t|}\ (A\in\A(O)).
 \tag{P}\label{eq:P}
\end{equation}

\emph{Sources.} \cite[\S III]{GJ1}; \cite[\S\S3.5--3.6]{GJ2}; \cite[\S4.1 and Ch.~4]{GJExp}.

\emph{Scope.} \eqref{eq:P} is the Glimm--Jaffe patching construction verbatim; the
$g$-uniform propagation bound for the \emph{cutoff} dynamics is not imported but derived
(Proposition~\ref{prop:propagation}).

\emph{Used in.} Proposition~\ref{prop:propagation}, \S\ref{sec:filter} (locality identity),
\S\ref{sec:lppl}, \S\ref{sec:ground}.

{\raggedright\emph{Dossier.} \texttt{gj1-locality-06}, \texttt{gjexp-054/055/056},
\texttt{gj2-cutoff-independence-38}, \texttt{gj2-local-algebra-40} (E03, E06,
E14--E16).\par}

Uses: prop:propagation

Assumption A7 (covariance data)

A:covar · page 9

Let $U_a$ implement the space translation $\tau_a$ on $Q$-space and let
$\Theta:=\Gamma(-1)$, so that $(\Theta\psi)(q)=\psi(-q)$ in $Q$-space. Then, for every
$g\in\CH$,
\[
 U_aK(g)U_a^*=K(\tau_ag),\qquad \Theta H_0\Theta=H_0,\qquad
 \Theta V(g)\Theta=V(g)\ \ \text{for even }\mathscr P .
\]

\emph{Sources.} \cite[p.~398]{GJ2} (cutoff covariance); the transformation of Wick powers
under $\Gamma(-1)$ is the parity of the polynomial.

\emph{Scope.} Only the displayed operator identities are imported; the state-level
consequences are derived in Lemma~\ref{lem:covparity}.

\emph{Used in.} Lemma~\ref{lem:covparity}; thence \S\ref{sec:ground},
\S\ref{sec:dichotomy}.

{\raggedright\emph{Dossier.} \texttt{gj2-cutoff-independence-38} (E06).\par}

Uses: lem:covparity

Assumption A8 (the GJS package)

A:gjs · page 9 · imports A8

The Euclidean input is \cite{GJS}, used exactly as printed, as follows.

\emph{(i) Measures.} For $h\in\CE$, $dq_h=Z(h)^{-1}e^{-\mathcal U_h}d\mu_0$ as in
Assumption~\ref{A:stability}; the Hamiltonian cutoff class of \cite[(1.6), p.~588]{GJS} is
$\CH$.

\emph{(ii) Observable class.} The class (1.1.5) of \cite{GJS} consists of sharp-time monomials
$Q(x^0)=\int d\vec x\,w(\vec x)\prod_i{:}\Phi(x_i)^{m_i}{:}$ with $L^2$ kernels; equal times
are allowed, and products of individually Wick-ordered powers are admissible without
reordering. GJS bound the degree of each \emph{individual} Wick factor: $n_i<\bar n$ for a fixed
finite $\bar n$, any choice $\bar n\ge\deg\mathscr P$ being sufficient; the printed text
adds ``Since there is no restriction on $r$, $Q$ still may have an arbitrarily large
degree'' (p.~593). Footnote~9 permits $\bar n=\infty$ at the price
$N(\Delta)!\to(N(\Delta)!)^3$ in (1.1.7), (1.1.8), (2.4.5). Every observable used below
has individual factor degrees $\le\max(2p',1)$, so the fixed finite choice
$\bar n=2p'+1$ applies and the printed first-power weights are used as displayed; the
\emph{total} degrees of the observables of \S\ref{sec:G} are unbounded, exactly as the
printed sentence licenses.

\emph{(iii) Printed norms.}
\begin{equation}
\begin{gathered}
 \textup{(1.1.7)}\ \ \|Q\|_{\rm GJS}=K_1\Bigl[\prod_\Delta K_2^{2N(\Delta)}N(\Delta)!\Bigr]\|w\|_2,\\
 \textup{(1.1.8)}\ \ \|Q(x_0)\|_{\rm GJS}=K_1\Bigl[\prod_\Delta K_2^{2N(\Delta)}N(\Delta)!\Bigr]\|w(x_0,\cdot)\|_2,
\end{gathered}
 \label{eq:printednorm}
\end{equation}
where $N(\Delta)$ is the total degree localized in the unit square $\Delta$, and
\textup{(1.1.9)}: a nonlocalized polynomial is normed by summing its localized pieces.
Replacing $K_2$ by $\max\{1,K_2\}$ only enlarges right-hand sides; \emph{we fix $K_2\ge1$}.

\emph{(iv) CE2.}
\begin{srcfact}[CE2 $=$ {\cite[Thm.~1.1.7]{GJS}}, p.~594]\label{sf:CE2}
For localized monomials $Q_1,Q_2$ with disjoint localization squares separated by a strip of
width $d$ bounded by two parallel lines (any orientation),
\[
  \Bigl|\int Q_1Q_2\,dq_h-\int Q_1dq_h\int Q_2dq_h\Bigr|\le C_7e^{-m_1d}\|Q_1\|_{\rm GJS}\|Q_2\|_{\rm GJS} ,
\]
with $m_1>0$ and $C_7$ \emph{independent of $h$, $Q_1$, $Q_2$} (so stated in the source).
\end{srcfact}

\emph{(v) CE1.}
\begin{srcfact}[CE1 $=$ {\cite[Thm.~1.1.8]{GJS}}, p.~595]\label{sf:CE1}
The printed estimate is
\[
 \bigl|\int Q(x^0)\,dq_h\bigr|\le C_8\|Q(x^0)\|_{\rm GJS},
\]
stated uniformly as the source cutoff tends to one.  This item records the literal
one-sentence theorem statement; the class-uniform quantifier actually consumed below,
which the source states on p.~629 and uses on pp.~595--597 (item~(vii$'$)), is isolated
in item~(vi) rather than being silently inserted here.
\end{srcfact}

\emph{(vi) Exact working-family interface $U_{\rm GJS}$ (imported at source scope).}
For
\[
 \CE^{\rm slab}:=
 \{h_{T,g}=\mathbf1_{[-T,T]}\otimes g:T>0,\ g\in\CH\}\subset\CE,
\]
one and the same constant $C_8$ satisfies
\begin{equation}
 \left|\int Q(x^0)\,dq_{h_{T,g}}\right|
 \le C_8\|Q(x^0)\|_{\rm GJS}
 \quad(T>0,\ g\in\CH) .
 \tag{$U_{\rm GJS}$}\label{eq:UGJS}
\end{equation}
The quantifiers include every affine cutoff
$g_s=(1-s)g+sg'$ used later, because $g_s\in\CH$.  Equation
\eqref{eq:UGJS}, and no uniformity assertion for a larger class, is the CE1
uniformity needed in \S\S\ref{sec:M2} and \ref{sec:G}.

\emph{(vii) Printed evidence for (vi).}
\begin{srcfact}[{\cite[p.~629, \S4]{GJS}}]\label{sf:printed}
``It is important to work with a translation invariant Hamiltonian, in order that time
translation preserve subspaces of bounded momentum. The estimates of Theorems 1.1.8, 1.1.11,
3.1 and 4.1 are uniform in the space cutoff $h$, and the path space integrals converge as
$h\to1$. Thus these theorems hold in the infinite volume limit, and we proceed to work in the
limit $h=1$.''
\end{srcfact}

\emph{(vii$'$) Printed use of the quantifier by the source.}  The following passages
show the source stating the cutoff-uniform quantifier of \eqref{eq:UGJS} and consuming
it for arbitrary cutoff functions of its class, not only in the limit $h\to1$.  The
source's $V(g)$ is the interaction $\mathcal U_g$ of item~(i); its
$\langle F\rangle_h$ is $\int F\,dq_h$.
\begin{srcfactstar}[{\cite[pp.~594--597 and 629]{GJS}}]
\emph{(a) Proof of Theorem 1.1.1, pp.~594--595.}  ``For test functions
$f_i\in C_0^\infty(\mathcal O)$ and for cutoff functions $h_1$ and $h_2$, we assert that
\[
 \Bigl|\int\prod_i\Phi(f_i)\,dq_{h_1}-\int\prod_i\Phi(f_i)\,dq_{h_2}\Bigr|
 \le O(1)e^{-m_1d/2}
 \tag{1.1.11}
\]
where $d=\operatorname{dist}(\mathcal O,\operatorname{suppt}\,h_1-h_2)$, and then
Theorem 1.1.1 follows.  To prove (1.1.11) let $g=h_2-h_1$, and define
$g_i=g\chi_{\Delta_i}$, where $\chi_{\Delta_i}$ is the characteristic function of
$\Delta_i$.  Also we use the notation $\langle F\rangle_h=\int F\,dq_h$, and set
$Q=\prod_i\Phi(f_i)$.  Then
\begin{align*}
 \langle Q\rangle_{h_2}-\langle Q\rangle_{h_1}
 &=\int_0^1d\alpha\,\frac{d}{d\alpha}\langle Q\rangle_{h_1+\alpha g}\\
 &=-\int_0^1d\alpha\bigl[\langle QV(g)\rangle_{h_1+\alpha g}
   -\langle Q\rangle_{h_1+\alpha g}\langle V(g)\rangle_{h_1+\alpha g}\bigr]
 \tag{1.1.12}\\
 &=-\int_0^1d\alpha\sum_{i\in\mathbb Z^2}\bigl[\langle QV(g_i)\rangle_{h_1+\alpha g}
   -\langle Q\rangle_{h_1+\alpha g}\langle V(g_i)\rangle_{h_1+\alpha g}\bigr] .
\end{align*}
We apply Theorem 1.1.7 to each term in the sum to obtain
\[
 |\langle Q\rangle_{h_2}-\langle Q\rangle_{h_1}|
 \le\sum_{i\in\mathbb Z^2\cap\operatorname{supp}g}
 O(1)e^{-m_1\operatorname{dist}(\mathcal O,\Delta_i)}
 \le O(1)e^{-m_1d/2} .
\]
As a special case, the cutoff Schwinger functions $S_h$ converge as $h\to1$.''

\emph{(b) Proof of Theorem 1.1.7, pp.~596--597.}  ``Proof of Theorem 1.1.7, assuming
Theorems 1.1.8 and 1.1.11.  Take $n=0$ in Theorem 1.1.11.  Then $Q$ is a polynomial of
degree zero, i.e., a constant.  From the choice $B=I$, it follows that
\[
 Q=\int A\,dq_h+O(1)\|A\|e^{-m_0(1-\varepsilon)T} .
\]
After rotating and translating the strip separating $Q_1$ and $Q_2$ in Theorem 1.1.7,
and after choosing $A=Q_1$, $B_T=Q_2$ in Theorem 1.1.11, the proof follows from Theorem
1.1.8, (1.1.16) and the above determination of $Q$.''  The estimate (1.1.16), p.~596,
reads ``$|\int(A-Q)B_T\,dq_h|\le O(1)\|A\|\,\|B\|e^{-\gamma T}$ uniformly in $h$.''

\emph{(c) p.~629.}  ``Theorem 1.1.11 follows from this inequality, while Theorem 1.1.8
is the special case $B=I$, $n=0$.''  The uniformity sentence of the same page is Source
Fact~\ref{sf:printed}.
\end{srcfactstar}

\emph{(viii) Scaling.} The unitary space-time dilation of \cite[p.~590]{GJS} sends
$(m_0,\lambda)\mapsto(s^{-1}m_0,s^{-2}\lambda)$; the exact reduction of the dimensionless
smallness hypothesis to the printed one is Proposition~\ref{prop:scaling}.

\emph{Scope.} Theorem 1.1.7 states that its constants are independent of $h$; the
one-sentence statement of Theorem 1.1.8 says ``uniformly as $h\uparrow1$''.  The
quantifier imported in (vi) --- one constant for the whole slab family
$\CE^{\rm slab}$ --- is the one the source states and uses, by the printed record of
item~(vii$'$), in three steps.
\emph{(a)} The source proves Theorem 1.1.1 along the affine path $h_1+\alpha(h_2-h_1)$,
$\alpha\in[0,1]$, for arbitrary cutoff functions $h_1,h_2$ of its class (p.~589:
compact support in $\mathbb R^2$, $0\le h\le1$), and applies Theorem 1.1.7 at every
cutoff of that path with one $h$-independent constant.  Our path
$h_{T,g_s}=(1-s)h_{T,g}+s\,h_{T,g'}$, $g_s=(1-s)g+sg'$ (\S\S\ref{sec:M2},
\ref{sec:G}), is this family with $h_1=h_{T,g}$, $h_2=h_{T,g'}$, $\alpha=s$.
\emph{(b)} The printed proof of Theorem 1.1.7 obtains its $h$-independent constant from
Theorem 1.1.8 and (1.1.16) \emph{at the same $h$}: the bound of Theorem 1.1.8 on
$\int Q_2\,dq_h$ multiplies the remainder $O(1)\|Q_1\|e^{-m_0(1-\varepsilon)T}$ in the
determination of $Q$.  Lemma~\ref{lem:ce2strip} and Proposition~\ref{prop:discharge}
use Theorem 1.1.7 as printed at $h=h_{T,g}\in\CE^{\rm slab}$; consistency therefore
requires the constant of Theorem 1.1.8 to be uniform on the same class, which is
\eqref{eq:UGJS}.
\emph{(c)} Source Fact~\ref{sf:printed} states the uniformity of Theorems 1.1.8 and
1.1.11 in the space cutoff $h$ explicitly, and p.~629 identifies Theorem 1.1.8 as the
case $B=I$, $n=0$ of the estimate proved there uniformly in $h$.
Hence \eqref{eq:UGJS} is imported at the scope at which the source states and uses it;
it is not a quantifier strengthened beyond the source.  It is kept as a named
hypothesis of Theorem~\ref{thm:MAIN} because its statement is assembled from four
pages of the source rather than read off one theorem, and because this manuscript does
not re-derive the cluster expansion: Appendix~\ref{app:huniform} audits the source
mechanism and proves two analytic prerequisites only.  The formerly illegible norm
prefactor was settled by page-image inspection: $K_1$ enters to the first power and the
local weight is $K_2^{2N(\Delta)}$ (gate R2,
\texttt{m4/r2-check.tex}). All constants in this manuscript use the exact reading
\eqref{eq:printednorm}.

\emph{Used in.} \S\ref{sec:reduction} (scaling), \S\ref{sec:slab}, \S\ref{sec:M2} (CE1),
\S\ref{sec:norms} (norms), \S\ref{sec:G} (CE1, CE2), Appendix~\ref{app:huniform}.

{\raggedright\emph{Dossier.} \texttt{gjs-source-05/06}, \texttt{gjs-p589-06}, \texttt{gjs-scaling-07},
\texttt{gjs-theorems-10/11/12}, \texttt{gjs-core-11/12}, \texttt{gjs-uniform-46},
\texttt{gjs-uniformity-46}, \texttt{gjs-proof-14} (E20--E26, E54).\par}

Provenance: src: audit_2026/evidence/gjs-theorems-11.png (p.594), gjs-theorems-12.png (p.595),; src: gjs-proof-14.png (p.597), gjs-uniform-46.png (p.629); transcribed from the page images.; src: m4/r1-check.tex sf:printed (page image of p.629), transcribed.; src: m4/r2-check.tex, Source Fact 1.1 (page image of p.594), transcribed.; src: m6/main.tex sf:CE1 (v2), transcribed.; src: m6/main.tex sf:CE2 (v2), transcribed. Uses: A:stability, lem:ce2strip, prop:discharge, prop:scaling, sf:printed, thm:MAIN

Source Fact 2.2 (CE2 $=$ {\cite[Thm.~1.1.7]{GJS}}, p.~594)

sf:CE2 · page 10

For localized monomials $Q_1,Q_2$ with disjoint localization squares separated by a strip of
width $d$ bounded by two parallel lines (any orientation),
\[
  \Bigl|\int Q_1Q_2\,dq_h-\int Q_1dq_h\int Q_2dq_h\Bigr|\le C_7e^{-m_1d}\|Q_1\|_{\rm GJS}\|Q_2\|_{\rm GJS} ,
\]
with $m_1>0$ and $C_7$ \emph{independent of $h$, $Q_1$, $Q_2$} (so stated in the source).

Provenance: src: m6/main.tex sf:CE2 (v2), transcribed.

Source Fact 2.3 (CE1 $=$ {\cite[Thm.~1.1.8]{GJS}}, p.~595)

sf:CE1 · page 10

The printed estimate is
\[
 \bigl|\int Q(x^0)\,dq_h\bigr|\le C_8\|Q(x^0)\|_{\rm GJS},
\]
stated uniformly as the source cutoff tends to one.  This item records the literal
one-sentence theorem statement; the class-uniform quantifier actually consumed below,
which the source states on p.~629 and uses on pp.~595--597 (item~(vii$'$)), is isolated
in item~(vi) rather than being silently inserted here.

Provenance: src: m6/main.tex sf:CE1 (v2), transcribed.

Source Fact 2.4 ({\cite[p.~629, \S4]{GJS}})

sf:printed · page 10

``It is important to work with a translation invariant Hamiltonian, in order that time
translation preserve subspaces of bounded momentum. The estimates of Theorems 1.1.8, 1.1.11,
3.1 and 4.1 are uniform in the space cutoff $h$, and the path space integrals converge as
$h\to1$. Thus these theorems hold in the infinite volume limit, and we proceed to work in the
limit $h=1$.''

Provenance: src: m4/r1-check.tex sf:printed (page image of p.629), transcribed.

Remark 2.5 (conventions lock)

rem:conv · page 12

The sharp-time restriction of the Euclidean covariance equals $C$:
$\int\frac{dk_0}{2\pi}(k_0^2+\mu(k)^2)^{-1}=(2\mu(k))^{-1}$ exactly. Hence sharp-time
$d\mu_0$-Wick ordering coincides, constant by constant, with the $C$-Wick ordering used in
$V(h)$, and sharp-time functionals of $\Phi(0,\cdot)$ are multiplication operators on $\HH$.
No Wick-mass conversion arises anywhere below.

Provenance: src: m6/main.tex rem:conv (v2), transcribed.

Proposition 2.6 (domain smoothing at the ground state)

prop:smoothing · page 12 · proof in the manuscript

$\Om_g\in D(V(h))$ for every $g\in\CH$ and every real $h\in L^1\cap L^2$ of compact support.

Uses: A:domain

Proposition 2.7 (cutoff propagation, uniformly in $g$)

prop:propagation · page 12 · proof in the manuscript

$\beta^g_t(\A(O))\subseteq\A(O_{|t|})$ for every $g\in\CH$ and $t\in\R$, with propagation
speed $\le1$ independent of $g$.

Uses: A:patch

Lemma 2.8 (covariance and parity of the cutoff states)

lem:covparity · page 12 · proof in the manuscript

For every $g\in\CH$ and $a\in\R$:
\begin{equation}
 \omega_{\tau_ag}=\omega_g\circ\tau_{-a} .
 \tag{T}\label{eq:T}
\end{equation}
For even $\mathscr P$: $\omega_g\circ\theta=\omega_g$.

Uses: A:covar, A:cutoff

Dimensionless weak-coupling reduction

Lemma 3.1 (class compatibility)

lem:classes · page 13 · proof in the manuscript

\emph{(i)} $\G\subset\CH$.
\emph{(ii)} For every $g\in\CH$ and every compact interval $I\subset\R$, the slab
cutoff $\mathbf 1_I\otimes g$ belongs to $\CE$; in particular
$h_{T,g}=\mathbf 1_{[-T,T]}\otimes g\in\CE$ and $\mathbf 1_{[0,T]}\otimes g\in\CE$.
\emph{(iii)} For $g,g'\in\CH$ and $s\in[0,1]$, the affine path $g_s:=(1-s)g+sg'$ stays in
$\CH$, and $\mathbf 1_I\otimes g_s=(1-s)\,\mathbf 1_I\otimes g+s\,\mathbf 1_I\otimes g'$
for every compact interval $I$, so that
$s\mapsto\mathcal U_{\mathbf 1_I\otimes g_s}
=(1-s)\mathcal U_{\mathbf 1_I\otimes g}+s\,\mathcal U_{\mathbf 1_I\otimes g'}$ is
affine. If moreover $g,g'\in\G$ and $\{g=1\}^\circ\cap\{g'=1\}^\circ\ne\varnothing$, then
$g_s\in\G$ with $\{g_s=1\}^\circ\supseteq\{g=1\}^\circ\cap\{g'=1\}^\circ$; in particular
$d(g_s,O)\ge\min\{d(g,O),d(g',O)\}$ for every bounded interval $O$.

Uses: A:stability

Proposition 3.2 (dimensionless weak-coupling reduction)

prop:scaling · page 13 · imports A8 · proof in the manuscript

The standing inequality $0\le\lambda/m_0^2<\varepsilon_{\mathscr P}$ implies the source
smallness hypothesis of Assumption~\ref{A:gjs}. More precisely, the GJS unitary dilation
with $s=m_0/M_*$ sends
\[
  (m_0,\lambda)\longmapsto
  (s^{-1}m_0,s^{-2}\lambda)
  =\left(M_*,\frac{M_*^2}{m_0^2}\lambda\right),
\]
and the transformed coupling is strictly smaller than $\lambda_*$.

Provenance: src: m6/main.tex prop:scaling (v2) = lamport_euclidean_to_gap.tex <1>1, transcribed. Uses: A:gjs, rem:wlog

Remark 3.3 (coordinate convention and transport of the conclusions)

rem:wlog · page 14 · imports A8

The dilation behind Proposition~\ref{prop:scaling} identifies the model at
$(m_0,\lambda)$ with the model at $(M_*,\lambda')$, $\lambda'=(M_*/m_0)^2\lambda
<\lambda_*$, as follows. Let $s=m_0/M_*$, $y=sx$, and let $\sigma_s$ be the scaling
automorphism of the Weyl algebra, $\sigma_s(W(f,h))=W(s^{-1}f(\cdot/s),h(\cdot/s))$
(a symplectic map). The sharp-time covariance is scale-covariant between the two masses,
$C_{M_*}(s\,z)=C_{m_0}(z)$ (the one-dimensional analogue of the substitution in the
proof of Proposition~\ref{prop:scaling}), so $\sigma_s$ carries the mass-$m_0$ Fock
state onto the mass-$M_*$ Fock state and is unitarily implemented by some $U_s$ with
$U_s\Om_0^{(m_0)}=\Om_0^{(M_*)}$; moreover $\sigma_s(\A(O))=\A(sO)$. On the
generators, $\mu_{M_*}(k/s)=s^{-1}\mu_{m_0}(k)$ (since $sM_*=m_0$) gives
$U_sH_0^{(m_0)}U_s^*=s\,H_0^{(M_*)}$, and the Euclidean Wick identification of
Proposition~\ref{prop:scaling}, restricted to sharp time (Remark~\ref{rem:conv}), gives
$U_sV_{m_0,\lambda}(g)U_s^*=s\,V_{M_*,\lambda'}(g(\cdot/s))$; hence
\[
 U_s\,K_{m_0,\lambda}(g)\,U_s^*=s\,K_{M_*,\lambda'}(g(\cdot/s)),
 \qquad g\in\CH .
\]
Consequently $g\mapsto g(\cdot/s)$ is an order isomorphism of $\G$ onto $\G$ (and a
bijection of $\CH$), cutoff ground states correspond under $U_s$, and the two cutoff
nets of states are carried onto each other. Every conclusion of
Theorem~\ref{thm:MAIN}, proved in the working (scaled) coordinates, therefore holds for
the original model with the dictionary: localization $O\leftrightarrow sO$; plateau
distance $d\leftrightarrow s\,d$, so the rate becomes $\Psi_{m_{1,*}}(s\,d)$, again
decaying faster than every inverse power of $d$; dynamics
$\alpha_t\leftrightarrow\alpha_{st}$, the light cone being form-invariant; gap
$m_1:=s\,m_{1,*}$; and the local-moment clause of item (5) transports to supports of
length $2/s$ --- equivalently, it holds for supports of length $2$ after splitting $h$
by a partition of unity into at most $\lceil s\rceil+1$ pieces of support length
$\le2/s$ (finite additivity of $V$), with constant $(\lceil s\rceil+1)$ times the
transported one. All displayed constants of \S\S\ref{sec:slab}--\ref{sec:lppl} and of
Appendices~\ref{app:constants}, \ref{app:huniform} are the constants of the working
coordinates, in which the unit-lattice geometry of Assumption~\ref{A:gjs} is literal.

Uses: A:gjs, prop:scaling, rem:conv, thm:MAIN

Slab transfer

Lemma 4.1 (slab FKN; bounded nonnegative arguments)

lem:slabFKN · page 15 · proof in the manuscript

For $T>0$, $t\in[0,2T]$, $s\in[-T,T]$, and bounded nonnegative measurable functions
$F_1,F_2$ of the time-zero field:
\begin{align}
  \int F_1\bigl(\Phi(-\tfrac t2,\cdot)\bigr)F_2\bigl(\Phi(\tfrac t2,\cdot)\bigr)dq_{h_{T,g}}
  &=\frac{\ip{F_1\psi_{T-t/2}}{e^{-tH(g)}F_2\psi_{T-t/2}}}{\|\psi_T\|^2},\label{eq:fkn2}\\
  \int F_1\bigl(\Phi(s,\cdot)\bigr)\,dq_{h_{T,g}}
  &=\frac{\ip{\psi_{T-s}}{F_1\,\psi_{T+s}}}{\|\psi_T\|^2};\label{eq:fkn1}
\end{align}
all energy shifts cancel in the ratios.

Provenance: src: m6/main.tex lem:FKN-main (v2), statement split; = lamport_euclidean_to_gap.tex <1>2<2>1. Uses: A:fkn, A:stability, lem:classes, rem:conv

Lemma 4.2 (signed bounded extension)

lem:slabsigned · page 15 · proof in the manuscript

Equations \eqref{eq:fkn2}--\eqref{eq:fkn1} hold for bounded signed measurable $F_1,F_2$.

Provenance: src: m6/main.tex lem:FKN-main proof (v2) = lamport_euclidean_to_gap.tex <1>2<2>2. Uses: lem:slabFKN

Lemma 4.3 (unbounded extension)

lem:slabunbdd · page 15 · imports A8 · proof in the manuscript

\emph{(i)} For nonnegative measurable $F_1,F_2$, the identities
\eqref{eq:fkn2}--\eqref{eq:fkn1} hold in $[0,\infty]$.
\emph{(ii)} For real measurable $F$, define the clipped truncation
$F^{[\ell]}:=(-\ell)\vee(F\wedge\ell)$, $\ell>0$. Whenever $F\psi_a\in\HH$,
\[
 \|(F-F^{[\ell]})\psi_a\|^2
 =\int |F-F^{[\ell]}|^2|\psi_a|^2\,d\phi_0\longrightarrow0
 \qquad(\ell\uparrow\infty),
\]
by dominated convergence with dominator $|F|^2|\psi_a|^2$; and on path space
\[
 |F_1(\Phi(s_1,\cdot))F_2(\Phi(s_2,\cdot))|
 \le\tfrac12\bigl(F_1(\Phi(s_1,\cdot))^2+F_2(\Phi(s_2,\cdot))^2\bigr)
\]
is a dominated-convergence majorant whenever the two square moments are finite. Consequently
the signed identities used below are limits of the bounded signed identities of
Lemma~\ref{lem:slabsigned}, with no formal manipulation of products of unbounded operators.

Provenance: src: m6/main.tex lem:FKN-main proof (v2) = lamport_euclidean_to_gap.tex <1>2<2>3; audit repairs L3, L4. Uses: A:domain, lem:slabFKN, lem:slabsigned, lem:transfer, thm:M2

Lemma 4.4 (slab vacuum; simplicity only)

lem:slabvac · page 16 · proof in the manuscript

$\hat\psi_s\to\Om_g$ in norm, $\|\psi_s\|\downarrow c_g$, and
$\|\psi_{s'}\|/\|\psi_s\|\in[1,1/c_g]$ for $0\le s'\le s$; the ratio tends to $1$ whenever
$s,s'\to\infty$. \emph{No isolation of the ground-state eigenvalue is used.}

Provenance: src: m6/main.tex lem:vac-main (v2), transcribed; = lamport_euclidean_to_gap.tex <1>3. Uses: A:cutoff

The uniform local interaction moment

Theorem 5.1 (uniform local interaction moment (M$_2$))

thm:M2 · page 16 · imports A8 · proof in the manuscript

Let $0\le\lambda/m_0^2<\varepsilon_{\mathscr P}$. For every $g\in\CH$ and every real
measurable $h$ with $\|h\|_\infty\le1$ and $\supp h$ contained in an interval of length
$2$,
\begin{equation}
 \|V(h)\Om_g\|\le M,\qquad
 M^2:=9\,C_8\,\mathfrak K(p')\,\lambda^2\Bigl(\sum_{n=0}^{2p'}|a_n|\Bigr)^2,
 \qquad
 \mathfrak K(p'):=K_1K_2^{8p'}(4p')! .
 \tag{M$_2$}\label{eq:M2}
\end{equation}

Provenance: src: lamport_euclidean_to_gap.tex <1>4; constant m4/r2-check.tex Prop. 2.1, Cor. 2.2. Uses: A:gjs, lem:slabunbdd, lem:slabvac, rem:conv

Corollary 5.2 ($\varphi^4$ instance)

cor:M2phi4 · page 17

For $\mathscr P(\xi)=\xi^4$ ($p'=2$, $\sum_n|a_n|=1$; degrees exactly $4+4=8$),
\[
 M^2=9\cdot8!\;C_8K_1K_2^{16}\lambda^2=362\,880\;C_8K_1K_2^{16}\lambda^2 .
\]

Provenance: src: m4/r2-check.tex Cor. 2.2, transcribed.

GJS norms of sharp-time polynomial observables

Lemma 6.1 (cell count)

lem:cells · page 17 · proof in the manuscript

$N_I\le\lfloor L\rfloor+2\le L+2$. The bound $L+1$ is % negative-scope mention (whitelisted): L+1
false for nonintegral $L$: the interval $I=(-0.1,0.1)$ has length $0.2$ and meets both
$[-1,0)$ and $[0,1)$ in positive measure.

Provenance: src: lamport_euclidean_to_gap.tex <1>5 <2>1; audit repair L1.

Proposition 6.2 (GJS norms of polynomial observables)

prop:gjsnorms · page 18 · imports A8 · proof in the manuscript

\begin{align}
 \|Q\|_{\rm GJS}
 &\le K_1K_2^{2r}r!\,N_I^{r/2}\prod_{i=1}^r\|f_i\|_2,\label{eq:normQ}\\
 \|Q^2\|_{\rm GJS}
 &\le K_1K_2^{4r}(2r)!\,N_I^{r}\prod_{i=1}^r\|f_i\|_2^2
   =:\mathfrak n(Q)^2 .\label{eq:normQ2}
\end{align}

Provenance: src: lamport_euclidean_to_gap.tex <1>5 <2>2, (5.1)-(5.2). Uses: A:gjs

Remark 6.3 (row independence)

rem:row · page 18

The norm of a sharp-time monomial is independent of the common sharp time $s$: at every $s$
all factors occupy one temporal row, and changing $s$ changes only that common row label,
not the spatial cell assignments, local degrees, kernel norms, or the product of weights.
This is the precise statement; arbitrary time translation does not literally preserve the
fixed lattice of unit squares.

Provenance: src: lamport_euclidean_to_gap.tex <1>5 <2>3.

The uniform gap

Lemma 7.1 (moment transfer)

lem:transfer · page 18 · imports A8 · proof in the manuscript

$\displaystyle\sup_{T>0}\|Q\hat\psi_T\|^2\le C_8\,\mathfrak n(Q)^2$; moreover
$\Om_g\in D(Q)$ and $\|Q\Om_g\|^2\le C_8\,\mathfrak n(Q)^2$.

Provenance: src: lamport_euclidean_to_gap.tex <1>6 <2>1 (6.1). Uses: lem:slabunbdd, rem:row

Lemma 7.2 (one-point limit)

lem:onepoint · page 18 · imports A8 · proof in the manuscript

For every fixed $s\in\R$,
\[
 \int Q(s)\,dq_{h_{T,g}}\longrightarrow\ip{\Om_g}{Q\Om_g}
 \qquad(T\to\infty).
\]

Provenance: src: lamport_euclidean_to_gap.tex <1>6 <2>2 (6.2)-(6.4); audit repair L2. Uses: lem:slabunbdd, lem:slabvac, lem:transfer, rem:row

Lemma 7.3 (two-point lower semicontinuity)

lem:twopoint · page 19 · imports A8 · proof in the manuscript

For every $t\ge0$, with the Euclidean integrals over slabs of half-width $T\ge t/2$
(so that \eqref{eq:fkn2} applies),
\[
 \ip{Q\Om_g}{e^{-tH(g)}Q\Om_g}
 \le\liminf_{T\to\infty}\int Q(-t/2)\,Q(t/2)\,dq_{h_{T,g}} .
\]

Provenance: src: lamport_euclidean_to_gap.tex <1>6 <2>3 (6.5)-(6.6). Uses: lem:slabunbdd, lem:slabvac, lem:transfer, rem:row

Lemma 7.4 (CE2 across a horizontal strip)

lem:ce2strip · page 19 · proof in the manuscript

For $t>2$ and every $h\in\CE$,
\[
 \Bigl|\int Q(-t/2)Q(t/2)\,dq_h
 -\int Q(-t/2)\,dq_h\int Q(t/2)\,dq_h\Bigr|
 \le C_7e^{2m_1}e^{-m_1t}\,\|Q\|_{\rm GJS}^2 .
\]

Provenance: src: lamport_euclidean_to_gap.tex <1>6 <2>4 (6.7). Uses: rem:row, sf:CE2

Proposition 7.5 (semigroup decay of centered observables)

prop:semidecay · page 20 · imports A8 · proof in the manuscript

Let $\psi_Q:=Q\Om_g-\ip{\Om_g}{Q\Om_g}\Om_g$. Then
\[
 \ip{\psi_Q}{e^{-tH(g)}\psi_Q}\le\widehat C_Q\,e^{-m_1t}\qquad(t\ge0),
 \qquad
 \widehat C_Q:=\max\bigl\{C_7e^{2m_1}\|Q\|_{\rm GJS}^2,\;e^{3m_1}\|\psi_Q\|^2\bigr\} .
\]

Provenance: src: lamport_euclidean_to_gap.tex <1>6 <2>5 (6.8). Uses: lem:ce2strip, lem:onepoint, lem:twopoint

Lemma 7.6 (exponential moments)

lem:expmom · page 20 · imports A8 · proof in the manuscript

Let $d\mu_g:=|\Om_g|^2\,d\phi_0$ and $X_f:=\varphi_0(f)$ for real
$f\in C_c^\infty(\R)$, $f\ne0$, supported in an interval of length $L$, and put
$K':=K_2^{2}N_I^{1/2}\|f\|_2>0$. Then
\[
 \E_{\mu_g}\bigl[X_f^{2n}\bigr]\le C_8K_1\,(K')^{2n}(2n)! \qquad(n\ge1),
\]
and consequently
\[
 \E_{\mu_g}e^{s|X_f|}
 \le2\max\{1,C_8K_1\}\sum_{n=0}^\infty(sK')^{2n}<\infty
 \qquad(0\le s<1/K') .
\]
The factor $C_8K_1$ affects only the prefactor, not the radius $1/K'$.

Provenance: src: lamport_euclidean_to_gap.tex <1>7 <2>1 (7.1)-(7.2); audit repair L5. Uses: lem:transfer

Theorem 7.7 (density of polynomial vectors)

thm:dense · page 21 · imports A8 · proof in the manuscript

Cylinder polynomials are dense in $L^2(d\mu_g)$. Equivalently, since $\Om_g>0$ a.e.\ makes
multiplication by $\Om_g$ a unitary from $L^2(d\mu_g)$ onto $\HH$, the linear span of
$\Om_g$ and the vectors $Q\Om_g$ ($Q$ a cylinder monomial) is dense in $\HH$.

Provenance: src: lamport_euclidean_to_gap.tex <1>7 <2>2-<2>5. Uses: lem:expmom

Theorem 7.8 (uniform gap (G))

thm:G · page 21 · imports A8 · proof in the manuscript

Let $0\le\lambda/m_0^2<\varepsilon_{\mathscr P}$. For every $g\in\CH$,
\begin{equation}
 \spec H(g)\subseteq\{0\}\cup[m_1,\infty),
 \tag{G}\label{eq:G}
\end{equation}
and $0$ is a simple eigenvalue.

Provenance: src: lamport_euclidean_to_gap.tex <1>8; audit repair L6. Uses: A:cutoff, prop:semidecay, thm:dense

Affine-path regularity

Proposition 8.1 (path regularity of the semigroup)

prop:pathreg · page 22 · proof in the manuscript

For each $T>0$, the family $s\mapsto e^{-TK_s}$ is norm-continuous on $[0,1]$ and
norm-$C^1$ on $(0,1)$, with derivative given by the FKN kernel of $-\,\mathcal U_vw_s$
in the notation of the proof.

Provenance: src: lamport_gap_to_main.tex <1>1 <2>1. Uses: A:fkn, A:hyper, A:stability, lem:classes

Proposition 8.2 (projection and eigenvector regularity; derivative formulas)

prop:projreg · page 23 · proof in the manuscript

\emph{(i)} $s\mapsto P_s$ is norm-continuous on $[0,1]$ and norm-$C^1$ on $(0,1)$.
\emph{(ii)} Locally on $(0,1)$ one may choose normalized $C^1$ vectors $\Om_s$ in the
parallel gauge $\ip{\Om_s}{\dot\Om_s}=0$, and then
\begin{equation}
 \dot E_s=\ip{\Om_s}{V(v)\Om_s},\qquad
 \dot\Om_s=-H_s^{-1}Q_sV(v)\Om_s ,
 \label{eq:derivform}
\end{equation}
with $\|H_s^{-1}Q_s\|\le\gamma^{-1}$.

Provenance: src: lamport_gap_to_main.tex <1>1 <2>2-<2>3. Uses: A:cutoff, A:domain, prop:pathreg, prop:smoothing

Filter, spectral separation, and clustering

Lemma 9.1 (exact inverse-energy filter)

lem:filter · page 24 · proof in the manuscript

Choose an even $\chi\in C^\infty(\R;[0,1])$ with $\chi=0$ on $[-\gamma/2,\gamma/2]$ and
$\chi=1$ outside $(-\gamma,\gamma)$, and set
\begin{equation}
 \widehat W_\gamma(E):=\begin{cases}\chi(E)/E,&E\ne0,\\0,&E=0,\end{cases}
 \qquad
 W_\gamma(t):=\frac1{2\pi}\int_\R e^{-itE}\,\widehat W_\gamma(E)\,dE .
 \label{eq:filterdef}
\end{equation}
Then:
\emph{(i)} $W_\gamma\in L^1(\R)$ and, for every $q\ge0$,
$\int_\R(1+|t|)^q|W_\gamma(t)|\,dt<\infty$; in particular
\[
 T_\gamma(r):=\int_{|t|>r}|W_\gamma(t)|\,dt
 \le C_{q,\gamma}(1+r)^{-q}\qquad(q\ge0,\ r\ge0).
\]
\emph{(ii)} If $H$ is self-adjoint with
$\spec H\subseteq\{0\}\cup[\gamma,\infty)$, then
\begin{equation}
 H^{-1}(1-P_{\ker H})=\int_\R W_\gamma(t)\,e^{itH}(1-P_{\ker H})\,dt ,
 \label{eq:filterid}
\end{equation}
a norm-convergent Bochner integral.

Provenance: src: lamport_gap_to_main.tex <1>2.

Lemma 9.2 (spectral separation)

lem:separation · page 25 · proof in the manuscript

Let
\[
 F(t)=\int_{[\gamma,\infty)}e^{itE}\,d\rho(E),\qquad
 G(t)=\int_{(-\infty,-\gamma]}e^{itE}\,d\sigma(E),
\]
with complex measures obeying $|\rho|(\R),|\sigma|(\R)\le\mathfrak m$, and suppose
$F=G$ on $(-R,R)$ with $\gamma R\ge1$. Then
\begin{equation}
 |F(0)|\le2\,\mathfrak m\,e^{-\gamma R/2} .
 \label{eq:sep}
\end{equation}

Provenance: src: lamport_gap_to_main.tex <1>3; variation bound renamed M_0 -> \mathfrak m per the freeze.

Lemma 9.3 (clustering with one unbounded local argument)

lem:cluster · page 25 · proof in the manuscript

Let $g\in\CH$, write $H=H(g)$, $\Om=\Om_g$, $\beta_t=\beta^g_t$, and assume
\eqref{eq:Ggamma}. Let $B\subset\R$ be compact, let $X=X^*$ be affiliated with $\A(U)$ for
every bounded open $U\supseteq B$, with $\Om\in D(X)$, and let $A\in\A(O)$ for a bounded
interval $O$. If $R:=\dist(B,O)>0$ satisfies $\gamma R\ge1$, then
\begin{equation}
 \bigl|\ip{X\Om}{A\Om}-\ip{X\Om}{\Om}\ip{\Om}{A\Om}\bigr|
 \le2\,\|X\Om\|\,\|A\|\,e^{-\gamma R/2} .
 \label{eq:cluster}
\end{equation}

Provenance: src: lamport_gap_to_main.tex <1>4. Uses: lem:separation, prop:propagation

$h$-uniformity: source audit and analytic prerequisites

Proposition C.1 (consequence of the audited source mechanisms)

prop:struct · page 36 · proof in the manuscript

Within mechanisms M1--M5 as recorded above, every displayed quantitative bound is
unchanged when $h$ ranges over $0\le h\le1$: M3 replaces its only vertex occurrence by
$|h|\le1$, while M4--M5 use identities or exact cancellation.  Consequently the
constants visible in those mechanisms depend on
$(m_0,K_2,K_1,\lambda,n,\varepsilon,\mathscr P)$ and not on $h$.

Provenance: src: m4/r1-check.tex prop:struct, transcribed.

Lemma C.2 (normalisation)

lem:Z · page 37 · proof in the manuscript

For every $h\in\CE$ with $\supp h\subseteq\Lambda$:
$Z(h)\ge e^{-\lambda|a_0|\,|\Lambda|}>0$, and $Z(h)<\infty$ by
Theorem~\ref{thm:stability}. Hence $dq_h$ is a well-defined probability measure on the
whole class $\CE$.

Provenance: src: m4/r1-check.tex lem:Z, transcribed. Uses: thm:stability

Lemma C.3 (Wick lower bound; the $h\ge0$ entry)

lem:wick · page 37 · proof in the manuscript

There is $b=b(\mathscr P)$ such that for all $c\ge0$ and $x\in\R$,
${:}\mathscr P{:}_c(x):=\sum_na_nc^{n/2}\operatorname{He}_n(x/\sqrt c)\ge-b\,(1+c)^{p'}$.
Consequently, for every $h\in\CE$ with $\supp h\subseteq\Lambda$ and every
$\kappa\ge2$,
\[
  \mathcal U_{h,\kappa}\ \ge\
  -\lambda\,b\,|\Lambda|\,\bigl(1+\tfrac1{2\pi}\log\kappa+C_*\bigr)^{p'}
  \ \ge\ -c_1(\lambda,\mathscr P,\Lambda)\,(\log\kappa)^{p'} .
\]

Provenance: src: m4/r1-check.tex lem:wick, transcribed.

Lemma C.4 (ultraviolet difference; the $h\le1$ entry)

lem:uv · page 37 · proof in the manuscript

There is $c_2=c_2(\lambda,\mathscr P,\Lambda)$ such that for all $h\in\CE$ with
$\supp h\subseteq\Lambda$ and all $\kappa\ge2$,
\[
  \bigl\|\mathcal U_h-\mathcal U_{h,\kappa}\bigr\|_{L^2(d\mu_0)}^2
  \ \le\ c_2\,\kappa^{-1}(\log\kappa)^{2p'} .
\]

Provenance: src: m4/r1-check.tex lem:uv, transcribed.

Theorem C.5 ($h$-uniform stability)

thm:stability · page 38 · proof in the manuscript

For every $p<\infty$ and compact $\Lambda$,
\[
  \sup\bigl\{\|e^{-\mathcal U_h}\|_{L^p(d\mu_0)}\ :\ h\in\CE,\
  \supp h\subseteq\Lambda\bigr\}\ <\ \infty .
\]

Provenance: src: m4/r1-check.tex thm:stability, transcribed. Uses: A:hyper, lem:uv, lem:wick

Remark C.6 (why the class is what it is)

rem:whyclass · page 38

The two halves of the constraint $0\le h\le1$ are used in complementary places:
positivity in the pointwise lower bound (Lemma~\ref{lem:wick} would fail for $h$ of
variable sign --- the interaction density is unbounded above \emph{and} below), and
boundedness in the $L^2$ kernel estimates (Lemma~\ref{lem:uv} and M3). Nothing else about
$h$ --- smoothness, shape, time extent, monotonicity along a sequence --- is touched
anywhere. This is the structural content of Source Fact~\ref{sf:printed}.

Provenance: src: m4/r1-check.tex, closing remark of \S4, transcribed. Uses: lem:uv, lem:wick, sf:printed

Proposition C.7 (coverage of every CE application)

prop:discharge · page 38 · imports A8 · proof in the manuscript

Assume $U_{\rm GJS}$.  Then every use of CE1 in
\S\S\ref{sec:slab}--\ref{sec:G} has a cutoff in $\CE^{\rm slab}$ and is covered by
\eqref{eq:UGJS}; every use of CE2 is covered directly by Source
Fact~\ref{sf:CE2}, whose constants are independent of $h$.  Lemma~\ref{lem:Z} and
Theorem~\ref{thm:stability} supply the normalization and integrability needed to define
the same measures.  Hence no stronger cutoff-uniformity assertion is consumed by the
proof.

Provenance: src: m4/r1-check.tex thm:verdict, transcribed. Uses: lem:Z, lem:ce2strip, lem:classes, lem:transfer, lem:twopoint, sf:CE2, thm:M2, thm:stability

This site is open source. Improve this page.