\section{Remarks on effectivity}
\label{sec:effective}

Theorem~\ref{thm:main} asserts that a threshold $\epsilon(g)$ exists, and its
proof gives no value for it. In this section we locate the non-effective
steps of that proof, show that those of a structural nature can be replaced
by terminating searches, and state precisely which quantitative information
is missing. The outcome is a conditional statement,
Theorem~\ref{thm:conditional-threshold}; it is not an effective form of
Theorem~\ref{thm:main}.

The proof of Theorem~\ref{thm:main} is non-effective in four places.
\begin{enumerate}[(a)]
\item \emph{Approach to the boundary family.}
 Theorems~\ref{thm:compactness} and~\ref{thm:classification} show that along
 a sequence $a\downarrow0$ the long measures accumulate only on
 $\mathcal B_g$. This is a compactness statement and comes without a modulus.
\item \emph{Stabilization.} The arguments of Sections~\ref{sec:kernels}
 and~\ref{sec:collision} begin by fixing the numbers of states in finitely
 many windows by Corollary~\ref{cor:cluster-stabilization}, which holds for
 all sufficiently small $a$ in a given sequence, below an unspecified
 threshold.
\item \emph{Finite certificates.} The tests of
 Theorem~\ref{thm:origin-certificate} and
 Proposition~\ref{prop:moving-certificate} are built from a linear identity
 supplied by Lemma~\ref{lem:finite-rows}, which asserts that a row lies in a
 span without exhibiting the combination. The finite-dimensional estimate of
 Proposition~\ref{prop:grid-projection} likewise comes with a constant that
 is not exhibited.
\item \emph{Constants.} The analytic estimates carry unnamed constants $C$,
 $c$, $\kappa$.
\end{enumerate}
We remove (a) in the sense of recursion theory
(Proposition~\ref{prop:eff-coarse-modulus}), turn (b) into an explicit
hypothesis (Definition~\ref{def:eff-local-exclusion}), and remove (c) for the
origin certificates (Propositions~\ref{prop:eff-row-search}
and~\ref{prop:eff-algebraic-rows}). Source (d) is not addressed;
Subsection~\ref{subsec:eff-remains} lists the estimates concerned.

Throughout this section an \emph{algorithm} is a Turing machine acting on
finite data: integers, rational numbers, and real algebraic numbers, the
latter given by their minimal polynomial over $\QQ$ and an isolating interval
with rational endpoints. ``Computable'' is meant in this sense only, and no
bound on the running time of any search below is implied.

\subsection{Observables and certified local exclusions}
\label{subsec:eff-observables}

Let $\mathcal Y=\{(\Delta,s)\in\RR\times\ZZ:\Delta\geq|s|\}$. By a
\emph{state measure} we mean a positive measure
$\rho=\sum_jA_{h_j}\otimes A_{\bar h_j}$ on $\RR^2$ with
$h_j,\bar h_j\geq0$, integer spins, and finitely many states below every
dimension; its states are points $(\Delta_j,s_j)\in\mathcal Y$, repeated
according to multiplicity. The long measure $\rho_a$ of an admissible
partition function is a state measure, and so is $\sigma(R,t)$ for every
half-integer $R\geq1$ and every real $t\geq1$, by
Theorem~\ref{thm:classification}(ii) applied with a sufficiently small gap.

\begin{definition}[Rational tests and observables]\label{def:eff-test}
A \emph{rational test} is a function $\varphi:\RR\times\ZZ\to\RR$ such that
$\varphi(\cdot,s)=0$ for all but finitely many $s$ and each
$\varphi(\cdot,s)$ is continuous, compactly supported and piecewise
polynomial, with rational breakpoints and rational coefficients. For a state
measure $\rho$ we put
$\langle\rho,\varphi\rangle=\sum_j\varphi(\Delta_j,s_j)$, and for a finite
family $\Phi$ of rational tests we write
$\Phi(\rho)=(\langle\rho,\varphi\rangle)_{\varphi\in\Phi}\in\RR^\Phi$, with
the norm $\|\cdot\|_\infty$ on $\RR^\Phi$.
\end{definition}

The number $\langle\rho,\varphi\rangle$ is the integral against $\rho$ of the
continuous, compactly supported, even function
$X\mapsto\sum_s\varphi(|X|^2,s)\max\{0,1-2|P^2-Q^2-s|\}$, so the observables
are continuous for the vague convergence of
Theorem~\ref{thm:compactness}(a). A rational test is a finite rational
datum, from which one computes a rational $E_\varphi\geq1$ with
$\varphi(\Delta,s)=0$ for $\Delta>E_\varphi$ and a rational Lipschitz
constant for $\varphi$ in $\Delta$; we put
$E_\Phi=\max_{\varphi\in\Phi}E_\varphi$. Any class of continuous compactly
supported tests with computable values and computable moduli of continuity
would serve equally well.

For the boundary measures, \eqref{eq:circle-measures},
\eqref{eq:physical-measures} and \eqref{eq:sigma-R-t} give
\begin{equation}\label{eq:eff-reference-pairing}
 \langle\sigma(R,t),\varphi\rangle
 =\tfrac12\!\!\sum_{(m,n)\in\ZZ^2\setminus\{0\}}\!\!
 \bigl[\varphi(E_{m,n}(R),mn)+\varphi(E_{m,n}(t),mn)\bigr]
 +\varphi(1,1)+\varphi(1,-1)-\varphi(2,0),
\end{equation}
where $E_{m,n}(r)=\frac12(m^2r^2+n^2r^{-2})$; the lattices $\Lambda_r$ and
$\Lambda_{1/r}$ contribute equally. Only charges with $m^2\leq2E_\varphi$ and
$n^2\leq2E_\varphi r^2$ contribute. Hence, for a half-integer $R$, the map
$t\mapsto\Phi(\sigma(R,t))$ is continuous on $[1,\infty)$, has a computable
Lipschitz constant on every interval $[1,\bar r]$ with $\bar r$ rational, and
takes rational, exactly computable values at rational $t$. We put
$r_g=(2g)^{-1/2}$ and
\[
 \Pi_g=\{(R,t):2R\in\ZZ,\ 1\leq R\leq r_g,\ 1\leq t\leq r_g\},
\]
so that $\mathcal B_g=\{\sigma(R,t):(R,t)\in\Pi_g\}$, because
$\sigma(R,t)=\sigma(t,R)$.

Sharp cluster counts are not continuous observables, but they are determined
by open conditions on continuous ones.

\begin{lemma}[Cluster counts from continuous tests]
\label{lem:eff-cluster-counts}
Let $s\in\ZZ$, let $I\subset\RR$ be a bounded open interval, and let
$\chi^-,\chi^+$ be rational tests vanishing off the spin $s$ with
\[
 0\leq\chi^-(\cdot,s)\leq\one_I\leq\one_{\overline I}\leq\chi^+(\cdot,s).
\]
Let $\rho$ be a state measure and $n_0\geq0$ an integer. If
$|\langle\rho,\chi^-\rangle-n_0|<\frac14$ and
$|\langle\rho,\chi^+\rangle-n_0|<\frac14$, then $\rho$ has exactly $n_0$
states of spin $s$ with dimension in $I$, and no further state of spin $s$
with dimension in $\overline I$. For $n_0=0$ the condition on $\chi^+$ alone
suffices.
\end{lemma}
\begin{proof}
Let $n^-$ and $n^+$ be the numbers of states of spin $s$ with dimension in
$I$ and in $\overline I$. Then
$n^-\geq\langle\rho,\chi^-\rangle>n_0-\frac14$ and
$n^+\leq\langle\rho,\chi^+\rangle<n_0+\frac14$, while $n^-\leq n^+$ are
integers. Hence $n^-=n^+=n_0$.
\end{proof}

\begin{definition}[Certified local exclusions]
\label{def:eff-local-exclusion}
Let $g\in(0,\frac12]$ be rational. A \emph{local exclusion datum} is a triple
$(\Phi,O,\alpha)$ consisting of a finite family $\Phi$ of rational tests, an
open box $O=\prod_{\varphi\in\Phi}(o^-_\varphi,o^+_\varphi)\subset\RR^\Phi$
with $o^-_\varphi<o^+_\varphi$ in $\QQ\cup\{\pm\infty\}$, and a rational
$\alpha>0$. It is a \emph{certified local exclusion for the gap $g$} if no
admissible partition function of gap $g$ at $c=1+12a$ with $0<a<\alpha$
satisfies $\Phi(\rho_a)\in O$. It \emph{covers} $\sigma\in\mathcal B_g$ if
$\Phi(\sigma)\in O$.
\end{definition}

``Certified'' refers to the truth of the exclusion, which is a statement
about all admissible partition functions; it cannot be read off from the
finite datum. By Lemma~\ref{lem:eff-cluster-counts}, a box can prescribe the
number of states in each of finitely many windows and the emptiness of
others. Such a box contains $\Phi(\sigma)$, with $n_0$ the number of states
of $\sigma$ in the window, whenever no state of $\sigma$ of the spin in
question lies in the support of $\chi^+-\chi^-$; for then both pairings
equal $n_0$. In this way the conclusions of
Corollary~\ref{cor:cluster-stabilization}, available along a sequence below
an unknown threshold, become hypotheses on a single partition function.

\subsection{A computable modulus for the approach to the boundary}

The following elementary fact is the only verification device used by the
searches of this section.

\begin{lemma}[Certifying strict positivity]\label{lem:eff-positivity}
Let $\mathsf Q$ be a finite union of closed boxes $\prod_i[p_i,p_i']$ with
rational $p_i\leq p_i'$, possibly of different dimensions, and let
$G:\mathsf Q\to\RR$. Suppose we are given a rational $\lambda$ with
$|G(w)-G(w')|\leq\lambda\|w-w'\|_\infty$ whenever $w,w'$ lie in the same box,
and an algorithm which, for a rational point $w\in\mathsf Q$ and an integer
$n\geq1$, returns a rational $G_n(w)$ with $|G_n(w)-G(w)|\leq2^{-n}$.
Then there is a procedure, uniform in these data, which halts if and only if
$G>0$ everywhere on $\mathsf Q$.
\end{lemma}
\begin{proof}
Let $\ell$ be the largest side length of the boxes. At stage $n$, consider
in each box the finitely many points whose coordinates are
$p_i+k2^{-n}(p_i'-p_i)$, $0\leq k\leq2^n$; every point of the box is
within $2^{-n}\ell$ of one of them. The procedure halts at stage $n$ if
$G_n(w)>(1+\lambda\ell)2^{-n}$ at all these points $w$. If it halts,
then for $w'$ in a box and $w$ a nearest such point,
$G(w')\geq G_n(w)-2^{-n}-\lambda\ell2^{-n}>0$. Conversely $G$ is
continuous, so if $G>0$ on $\mathsf Q$ then $G\geq\mu$ for some $\mu>0$, and
the procedure halts as soon as $(2+\lambda\ell)2^{-n}<\mu$.
\end{proof}

\begin{proposition}[A computable modulus]\label{prop:eff-coarse-modulus}
There is an algorithm which, given a rational $g\in(0,\frac12]$, a finite
family $\Phi$ of rational tests and a rational $\gamma>0$, halts and returns
a rational $a_\gamma\in(0,g^2/4]$ with the following property: for every
admissible partition function of gap $g$ at $c=1+12a$ with
$0<a\leq a_\gamma$ there is $\sigma\in\mathcal B_g$ with
$\|\Phi(\rho_a)-\Phi(\sigma)\|_\infty<\gamma$.
\end{proposition}
\begin{proof}
Put $a_0=g^2/4$ and $\mathsf c_g=3^8(1+\lceil18g^{-2}\rceil)$. For $j\geq1$ let
$k_j$ be the largest integer $k\geq0$ with $\mathsf c_g2^k\leq j$, or $k_j=0$ if
$j<\mathsf c_g$, and let $\lambda_j=\max\{g,k_j^2/256\}$. At most
$\mathsf c_g2^{k+1}$ indices $j$ have $k_j=k$.

\smallskip\noindent\emph{Step 1: a compact container.}
Let $Z$ be admissible of gap $g$ with $0<a\leq a_0$, and number its states so
that $\Delta_1\leq\Delta_2\leq\cdots$. We claim that
$\Delta_j\geq\lambda_j$. For $E\geq1$, \eqref{eq:thermal-high} with
$y=E^{-1/2}$ gives
\[
 N_a(E)\leq e^{2\pi yE}P_a(y)
 \leq(1+C_g)\sqrt E\,e^{2\pi(1+a)\sqrt E}\leq(1+C_g)\,e^{8\sqrt E},
\]
because $a\leq\frac1{16}$, $2\pi\cdot\frac{17}{16}<7$ and
$\sqrt E\leq e^{\sqrt E}$; for $E<1$ we use $N_a(E)\leq N_a(1)$. Since
$e^8<3^8$ and $C_g=2e^{\pi/2}g^{-2}<18g^{-2}$, we get
$N_a(E)\leq\mathsf c_ge^{8\sqrt E}$ for all $E\geq0$. Now $j\leq N_a(\Delta_j)$,
so $\mathsf c_g2^k\leq j$ implies $8\sqrt{\Delta_j}\geq k\log2\geq k/2$, that
is, $\Delta_j\geq k^2/256$. Together with $\Delta_j\geq g$ this proves the
claim.

Let $Y_j=\{\infty\}\cup\{(\Delta,s)\in\mathcal Y:\Delta\geq\lambda_j\}$, the
one-point compactification of a closed subset of $\RR\times\ZZ$, and let
\[
 \mathfrak K_g=[0,a_0]\times\prod_{j\geq1}Y_j ,
\]
a compact metrizable space. We write its points as $\xi=(a,(w_j)_{j\geq1})$
and call the entries $w_j\neq\infty$ the states of $\xi$. By the claim,
every admissible $Z$ of gap $g$ with $0<a\leq a_0$ defines a point
$\xi_Z\in\mathfrak K_g$, by listing its states in nondecreasing order of
dimension and filling up with $\infty$ if there are finitely many. For a
rational test $\varphi$ put
$\langle\xi,\varphi\rangle=\sum_{w_j\neq\infty}\varphi(w_j)$; only the
finitely many $j$ with $\lambda_j\leq E_\varphi$ contribute, so this is a
continuous function on $\mathfrak K_g$, and $\Phi(\xi_Z)=\Phi(\rho_a)$. For
$\tau=x+iy\in\HH$ put
\[
 \widehat Z(\tau;\xi)=\sqrt y\,e^{2\pi ay}\Bigl(
 \bigl|1-e^{2\pi i\tau}\bigr|^2
 +\sum_{w_j=(\Delta_j,s_j)\neq\infty}e^{2\pi ixs_j-2\pi y\Delta_j}\Bigr),
 \qquad
 \mathsf F_\tau(\xi)=\widehat Z(\tau;\xi)-\widehat Z(-1/\tau;\xi).
\]
The $j$th term is continuous on $Y_j$, with value $0$ at $\infty$, and is
bounded by $e^{-2\pi y\lambda_j}$; since
$\sum_je^{-\beta\lambda_j}\leq\mathsf c_g\sum_{k\geq0}2^{k+1}e^{-\beta k^2/256}
<\infty$ for every $\beta>0$, the series converges uniformly on
$\mathfrak K_g$, locally uniformly in $\tau$. Thus $\mathsf F_\tau$ is
continuous on $\mathfrak K_g$, and $\tau\mapsto\mathsf F_\tau(\xi)$ is
continuous on $\HH$. By \eqref{eq:reduced-trace},
$\widehat Z(\tau;\xi_Z)=\widehat Z_a(\tau)$, so that
\begin{equation}\label{eq:eff-defect-zero}
 \mathsf F_\tau(\xi_Z)=0\qquad\text{for all }\tau\in\HH .
\end{equation}

\smallskip\noindent\emph{Step 2: truncation.}
Let $k\geq12$ be an integer, $E_k=k^2/256\geq g$ and
$J_k=\mathsf c_g2^{k+1}-1$, so that $\lambda_j\leq E_k$ exactly for
$j\leq J_k$. Put
\[
 \mathfrak K_{g,k}=\prod_{j=1}^{J_k}Y_{j,k},\qquad
 Y_{j,k}=\{\ast\}\cup\{(\Delta,s)\in\mathcal Y:
 \lambda_j\leq\Delta\leq E_k\}.
\]
Each $Y_{j,k}$ is the union of an isolated point and finitely many closed
intervals with rational endpoints, one for each admissible spin, so
$[0,a_0]\times\mathfrak K_{g,k}$ is a finite union of boxes with rational
vertices. Let $\iota_k:[0,a_0]\times\mathfrak K_{g,k}\to\mathfrak K_g$
replace $\ast$ by $\infty$ and put $w_j=\infty$ for $j>J_k$, and let
$\pi_k:\mathfrak K_g\to[0,a_0]\times\mathfrak K_{g,k}$ keep $a$ and the
states $w_j$, $j\leq J_k$, with $\Delta_j\leq E_k$, replacing the other
entries by $\ast$. A state of $\xi$ with $\Delta_j\leq E_k$ has
$\lambda_j\leq E_k$, hence $j\leq J_k$; so $\iota_k\pi_k\xi$ is obtained
from $\xi$ by deleting exactly the states with $\Delta_j>E_k$. Consequently,
if $E_k\geq E_\Phi$ then
\begin{equation}\label{eq:eff-truncation-tests}
 \Phi(\iota_k\pi_k\xi)=\Phi(\xi).
\end{equation}
Among the deleted states, fewer than $\mathsf c_g2^{k+1}$ have $j\leq J_k$,
each with $\Delta_j>k^2/256$, and those with $j>J_k$ have
$\Delta_j\geq k_j^2/256$ with $k_j>k$. Therefore, with
$\vartheta(\beta,k)=\sum_{k'\geq k}2^{k'+1}e^{-\beta k'^2/256}$ and
$y'=\operatorname{Im}(-1/\tau)$,
\begin{equation}\label{eq:eff-truncation-defect}
 |\mathsf F_\tau(\xi)-\mathsf F_\tau(\iota_k\pi_k\xi)|
 \leq\mathsf c_g\Bigl(\sqrt y\,e^{2\pi a_0y}\vartheta(2\pi y,k)
 +\sqrt{y'}\,e^{2\pi a_0y'}\vartheta(2\pi y',k)\Bigr).
\end{equation}
The right side is a computable real number which tends to zero as
$k\to\infty$.

\smallskip\noindent\emph{Step 3: certificates.}
Fix enumerations $\tau_1,\tau_2,\dots$ of $\QQ(i)\cap\HH$ and
$t_1,t_2,\dots$ of $\QQ\cap[1,r_g]$; membership in the latter set is the
decidable condition $t\geq1$, $2gt^2\leq1$. For $i\leq k$ compute a rational
$\varepsilon_{i,k}$ which is at least the right side of
\eqref{eq:eff-truncation-defect} at $\tau=\tau_i$ and exceeds it by at most
$2^{-k}$; thus $\varepsilon_{i,k}\to0$ as $k\to\infty$. Let
$k_\Phi=\max\{12,\lceil16\sqrt{E_\Phi}\,\rceil\}$, so that $E_k\geq E_\Phi$
for $k\geq k_\Phi$. For integers $k\geq k_\Phi$ and $l$ with
$2^{-l}\leq a_0$ define, on
$\mathsf Q_{l,k}=[0,2^{-l}]\times\mathfrak K_{g,k}$,
\[
 G_{l,k}(a,w)=\max\Bigl\{\gamma-\min_{R,\,i\leq k}
 \|\Phi(\iota_k(a,w))-\Phi(\sigma(R,t_i))\|_\infty,\
 \max_{i\leq k}\bigl(|\mathsf F_{\tau_i}(\iota_k(a,w))|
 -\varepsilon_{i,k}\bigr)\Bigr\},
\]
where $R$ ranges over the half-integers in $[1,r_g]$. We claim: \emph{if
$G_{l,k}>0$ on $\mathsf Q_{l,k}$, then $a_\gamma=2^{-l}$ has the property
stated in the proposition.} Indeed, let $Z$ be admissible of gap $g$ with
$0<a\leq2^{-l}$ and put $(a,w)=\pi_k\xi_Z\in\mathsf Q_{l,k}$. By
\eqref{eq:eff-defect-zero} and \eqref{eq:eff-truncation-defect},
$|\mathsf F_{\tau_i}(\iota_k(a,w))|\leq\varepsilon_{i,k}$ for all $i\leq k$,
so the first entry of the maximum is positive: there are $R$ and $i$ with
$\|\Phi(\iota_k(a,w))-\Phi(\sigma(R,t_i))\|_\infty<\gamma$. By
\eqref{eq:eff-truncation-tests} the first vector is $\Phi(\rho_a)$, and
$\sigma(R,t_i)\in\mathcal B_g$.

\smallskip\noindent\emph{Step 4: a certificate exists.}
Fix $l_0$ with $2^{-l_0}\leq a_0$. We show that $G_{l_0+k,k}>0$ on
$\mathsf Q_{l_0+k,k}$ for some $k\geq k_\Phi$. Suppose not, and choose for
every $k\geq k_\Phi$ a point $(a_k,w_k)$ with $G_{l_0+k,k}(a_k,w_k)\leq0$.
Let $\xi_k=\iota_k(a_k,w_k)$. By compactness of $\mathfrak K_g$ a
subsequence converges to some $\xi_\infty=(a_\infty,(w_j))$. Since
$a_k\leq2^{-l_0-k}$, we have $a_\infty=0$. Since
$|\mathsf F_{\tau_i}(\xi_k)|\leq\varepsilon_{i,k}$ for $k\geq i$ and
$\varepsilon_{i,k}\to0$, continuity gives $\mathsf F_{\tau_i}(\xi_\infty)=0$
for every $i$, hence $\mathsf F_\tau(\xi_\infty)=0$ for all $\tau\in\HH$.
Since $\|\Phi(\xi_k)-\Phi(\sigma(R,t_i))\|_\infty\geq\gamma$ for $k\geq i$,
continuity in $\xi$ and in $t$ and density of the $t_i$ give
\begin{equation}\label{eq:eff-limit-far}
 \|\Phi(\xi_\infty)-\Phi(\sigma(R,t))\|_\infty\geq\gamma
 \qquad\text{for all }(R,t)\in\Pi_g .
\end{equation}
On the other hand, let $(h_j,\bar h_j)$ be the weights of the states of
$\xi_\infty$ and $H_0=(1-q)(1-\bar q)+\sum_jq^{h_j}\bar q^{\bar h_j}$. Then
$h_j,\bar h_j\geq0$, the spins are integers,
$\Delta_j\geq\lambda_j\geq g$, and the sum converges on $\HH$, so $H_0$ has
the form \eqref{eq:cls-boundary-long}. The function $Z_0=H_0/|\eta|^2$ is
invariant under $\tau\mapsto\tau+1$ because the spins are integers, and
under $\tau\mapsto-1/\tau$ because
$\sqrt y\,H_0(\tau)=\widehat Z(\tau;\xi_\infty)$ and
$\mathsf F_\tau(\xi_\infty)=0$. The proofs of
Lemma~\ref{lem:gaussian-identity} at $a=0$, of Lemmas~\ref{lem:cls-growth}
and~\ref{lem:cls-mixture}, and of Theorem~\ref{thm:classification}(i) use no
property of a limit other than these. Hence the state measure of
$\xi_\infty$ equals $\sigma(R,t)$ for some $(R,t)\in\Pi_g$, which
contradicts \eqref{eq:eff-limit-far}.

\smallskip\noindent\emph{Step 5: the search.}
On each box of $\mathsf Q_{l,k}$ the function $G_{l,k}$ is obtained by
finitely many operations $\max$, $\min$, $|\cdot|$ from rational constants,
from the piecewise polynomial functions
$\langle\iota_k(a,w),\varphi\rangle$, from the rational numbers
$\langle\sigma(R,t_i),\varphi\rangle$ given by
\eqref{eq:eff-reference-pairing}, and from the finite sums
$\mathsf F_{\tau_i}(\iota_k(a,w))$ of exponentials. A Lipschitz constant and
approximate values at rational points are therefore computable, and
Lemma~\ref{lem:eff-positivity} applies. The algorithm runs the procedures of
that lemma for all pairs $(l,k)$ with $2^{-l}\leq a_0$ and $k\geq k_\Phi$ in
an interleaved fashion and returns $a_\gamma=2^{-l}$ for the first pair at
which one of them halts. It halts by Step~4 and its output is correct by
Step~3.
\end{proof}

\begin{remark}\label{rem:eff-modulus}
The algorithm of Proposition~\ref{prop:eff-coarse-modulus} is an unbounded
search, and ``computable'' has only its recursion-theoretic meaning. The
correctness of the output (Step~3) is elementary. That the search halts
(Step~4) is proved by compactness together with
Theorem~\ref{thm:classification}, and therefore rests on the reduction
quoted from \cite{EL} in Proposition~\ref{prop:cls-reduction}. The proof
provides no bound for the halting time and no lower bound for $a_\gamma$ in
terms of $g$, $\Phi$ and $\gamma$; the dimension of $\mathsf Q_{l,k}$ is of
order $\mathsf c_g2^k$. The proposition concerns the approach to the whole of
$\mathcal B_g$ and cannot be improved in this respect by the same method:
every element of $\mathcal B_g$ is a common zero of the functions
$\mathsf F_\tau$ at $a=0$.
\end{remark}

\subsection{Gluing certified local exclusions}

\begin{theorem}[Conditional threshold]\label{thm:conditional-threshold}
There is an algorithm $\mathcal A$ with the following property. Its input
is a rational $g\in(0,\frac12]$ together with a sequence
$(\Phi_i,O_i,\alpha_i)_{i\geq1}$ of local exclusion data, presented by a
program, or an oracle, that returns the $i$th datum on input $i$. Suppose
that
\begin{enumerate}[(i)]
\item every $(\Phi_i,O_i,\alpha_i)$ is a certified local exclusion for the
 gap $g$, and
\item every $\sigma\in\mathcal B_g$ is covered by at least one of them:
 there is $i$ with $\Phi_i(\sigma)\in O_i$.
\end{enumerate}
Then $\mathcal A$ halts, and its output is a rational $\epsilon(g)>0$ such
that no admissible partition function of gap $g$ has central charge in
$(1,1+\epsilon(g))$.
\end{theorem}
\begin{proof}
For a box $O$ as in Definition~\ref{def:eff-local-exclusion} and
$v\in\RR^\Phi$ let
\[
 \operatorname{depth}_O(v)=\min\bigl\{1,\
 \min_{\varphi}(v_\varphi-o^-_\varphi),\
 \min_{\varphi}(o^+_\varphi-v_\varphi)\bigr\}.
\]
This function is $1$-Lipschitz for $\|\cdot\|_\infty$, and $v\in O$ if and
only if $\operatorname{depth}_O(v)>0$.

\smallskip\noindent\emph{First search.} For an integer $i_0\geq1$, a
rational $\gamma\in(0,1)$ and a rational $\bar r$ with $2g\bar r^2>1$, that
is, $\bar r>r_g$, consider the function
\[
 G(R,t)=\max_{i\leq i_0}
 \operatorname{depth}_{O_i}\bigl(\Phi_i(\sigma(R,t))\bigr)-\gamma
\]
on the finite union of the intervals $\{R\}\times[1,\bar r]$, $R$ a
half-integer in $[1,r_g]$. By the discussion following
\eqref{eq:eff-reference-pairing} it has a computable Lipschitz constant and
computable values at rational $t$. The algorithm interleaves the procedures
of Lemma~\ref{lem:eff-positivity} for all triples $(i_0,\gamma,\bar r)$ and
stops at the first triple for which $G>0$ is certified. Such a triple
exists. Indeed, by (ii) the open sets
$\{(R,t)\in\Pi_g:\Phi_i(\sigma(R,t))\in O_i\}$ cover the compact set
$\Pi_g$; hence for some $i_0$ the continuous function
$\max_{i\leq i_0}\operatorname{depth}_{O_i}(\Phi_i(\sigma(R,t)))$ is
positive on $\Pi_g$, so it exceeds some rational $2\gamma$ there, and by
uniform continuity it exceeds $\gamma$ on $\{R\}\times[1,\bar r]$ for every
$R$ once $\bar r$ is close enough to $r_g$.

\smallskip\noindent\emph{Second search.} Let $\Phi$ be the disjoint union of
$\Phi_1,\dots,\Phi_{i_0}$, apply the algorithm of
Proposition~\ref{prop:eff-coarse-modulus} to $(g,\Phi,\gamma)$, and let
$a_\gamma$ be its output. The algorithm $\mathcal A$ returns
\[
 \epsilon(g)=12\min\{a_\gamma,\alpha_1,\dots,\alpha_{i_0}\}.
\]

\smallskip\noindent\emph{Correctness.} Suppose $Z$ is admissible of gap $g$
at $c=1+12a$ with $0<12a<\epsilon(g)$. Since $a\leq a_\gamma$, there is
$\sigma=\sigma(R,t)$ with $(R,t)\in\Pi_g$ and
$\|\Phi(\rho_a)-\Phi(\sigma)\|_\infty<\gamma$. By the first search there is
$i\leq i_0$ with $\operatorname{depth}_{O_i}(\Phi_i(\sigma))>\gamma$. As
$\|\Phi_i(\rho_a)-\Phi_i(\sigma)\|_\infty<\gamma$ and the depth is
$1$-Lipschitz, $\operatorname{depth}_{O_i}(\Phi_i(\rho_a))>0$, that is,
$\Phi_i(\rho_a)\in O_i$. Since $a<\alpha_i$, this contradicts (i).
\end{proof}

\begin{remark}\label{rem:eff-real-gap}
For an arbitrary real $g>0$ one applies the theorem to a rational
$g'<\min\{g,\frac12\}$: an admissible partition function of gap $g$ is
admissible of gap $g'$ (compare Remark~\ref{rem:gap-range}). Rationality of
the gap is used only so that the input and the conditions $2gR^2\leq1$,
$2gt^2\leq1$ are handled exactly.
\end{remark}

\begin{remark}\label{rem:eff-content}
For a single fixed $g$, the existence of an algorithm that prints a valid
threshold is a trivial consequence of Theorem~\ref{thm:main}; likewise (i)
and (ii) can be met trivially once a valid threshold is known, by a single
datum whose box is all of $\RR^\Phi$. The content of
Theorem~\ref{thm:conditional-threshold} is that one explicitly described
algorithm, with $g$ as input, converts local information near each point of
$\mathcal B_g$ into a threshold, and that the validity of its output is
established without Theorem~\ref{thm:main}: it uses hypothesis (i) and
Step~3 of the proof of Proposition~\ref{prop:eff-coarse-modulus}, while the
classification enters only in the proof that $\mathcal A$ halts. The
algorithm verifies (ii) for the data it uses, with a margin; it does not
and cannot verify (i). If (ii) fails it does not halt. If (ii) holds and
(i) fails it halts, and its output need not be valid.
\end{remark}

\subsection{A smallness cutoff}

Once an estimate has an explicit constant, the absorption of logarithms
into a power can be made explicit as well.

\begin{lemma}[A rational smallness cutoff]\label{lem:eff-cutoff}
Let $p>0$, $C\geq1$ and $0<\gamma\leq1$ be rational, let $b\geq0$ be an
integer, and let $k$ be an integer with
\[
 k\geq\max\Bigl\{2,\ \frac{8b^2}{p^2},\ \frac{4C2^b}{p\gamma}\Bigr\}.
\]
Then $C\,x^p\,(1+\log(1/x))^b<\gamma$ for every $0<x\leq2^{-k}$.
\end{lemma}
\begin{proof}
Let $\ell=\log(1/x)\geq k\log2\geq k/2\geq1$. Since $\log\ell\leq\sqrt\ell$
and $\ell\geq4b^2/p^2$,
\[
 (1+\ell)^b\leq(2\ell)^b\leq2^b e^{b\sqrt\ell}
 \leq2^b e^{p\ell/2}.
\]
With $\zeta=C2^b/\gamma$ we have $p\ell/2\geq pk/4\geq\zeta$, so
\[
 C\,x^p(1+\ell)^b=C\,e^{-p\ell}(1+\ell)^b\leq C2^b e^{-p\ell/2}
 \leq C2^b e^{-\zeta}=\gamma\,\zeta e^{-\zeta}<\gamma .
\qedhere
\]
\end{proof}

A finite list of such inequalities is satisfied below $2^{-k}$ for the
largest of the corresponding integers $k$. The third entry of the maximum
is wasteful: the proof shows that any integer exceeding
$(4/p)\log(C2^b/\gamma)$ may take its place. The form stated avoids
logarithms of the data.

\subsection{Computable origin certificates}
\label{subsec:eff-certificates}

We turn to source (c). Fix integers $d,q\geq1$. Let $\mathcal R_d$ be the
set of radii of Lemma~\ref{lem:grid-circles},
$\Sigma_0=\bigcup_{r\in\mathcal R_d}\Lambda_r\subset d^{-1}\Lambda_1$, and
\[
 \Sigma_d(t)=d^{-1}\Lambda_1\cup\Lambda_t\cup\Lambda_{1/t}
 \supset\Sigma_0\cup\Lambda_t\cup\Lambda_{1/t},\qquad t>0 ;
\]
in light-cone coordinates $d^{-1}\Lambda_1=d^{-1}\ZZ^2$. The single grid
$d^{-1}\Lambda_1$ is a transverse family adapted to $\mathcal R_d$, with
phase exponent $\nu=d^2$ (Definition~\ref{def:rig-transverse-family}). We
use the conventions of Section~\ref{sec:rigidity} for translations $\tau_w$,
multi-indices and the sets $\mathcal A_q$, write $s(X)=P^2-Q^2$,
$e_P=(1,0)$, $e_Q=(0,1)$, and denote multi-indices by
$\beta=(\beta_P,\beta_Q)$ and distributions by $\mathsf T$.

The phase rows \eqref{eq:rig-phase-row} used in
Section~\ref{sec:rigidity} have coefficients involving powers of $\pi i$.
They can be replaced by equations with rational coefficients.

\begin{lemma}[The local phase equation]\label{lem:eff-local-phase}
Let $x=(x_P,x_Q)\in\RR^2$, let
$\mathsf T_x=\sum_{|\beta|\leq q}c_\beta\,\partial^\beta\delta_x$, and put
$\varpi_x=s-s(x)$. If $\nu$ is a nonzero integer with $\nu s(x)\in\ZZ$, then
$\mathcal C^\nu\mathsf T_x=\mathsf T_x$ if and only if
$\varpi_x\mathsf T_x=0$. Moreover, with $c_{\beta'}=0$ for $|\beta'|>q$,
\begin{equation}\label{eq:eff-phase-row}
\begin{aligned}
 \varpi_x\mathsf T_x=\sum_{|\beta|\leq q-1}\bigl[
 &-2x_P(\beta_P+1)c_{\beta+e_P}+(\beta_P+2)(\beta_P+1)c_{\beta+2e_P}\\
 &+2x_Q(\beta_Q+1)c_{\beta+e_Q}-(\beta_Q+2)(\beta_Q+1)c_{\beta+2e_Q}
 \bigr]\partial^\beta\delta_x .
\end{aligned}
\end{equation}
The coefficients of this equation are polynomials over $\QQ$ in the
coordinates of $x$; no power of $\pi$ occurs.
\end{lemma}
\begin{proof}
Let $V_q$ be the space of distributions supported at $x$ of order at most
$q$. For a smooth function $f$,
$f\,\partial^\beta\delta_x=\sum_{\beta'\leq\beta}(-1)^{|\beta-\beta'|}
\binom{\beta}{\beta'}(\partial^{\beta-\beta'}f)(x)\,
\partial^{\beta'}\delta_x$. Hence multiplication by $f$ on $V_q$ depends
only on the Taylor polynomial of $f$ of degree $q$ at $x$, and
multiplication by a function vanishing at $x$ lowers the order. In
particular the operator $\mathsf m$ of multiplication by $\varpi_x$
satisfies $\mathsf m^{q+1}=0$ on $V_q$. Write
$e^{2\pi i\nu z}-1=2\pi i\nu z\,\mathsf E(z)$ with $\mathsf E$ entire and
$\mathsf E(0)=1$. Since $e^{2\pi i\nu s(x)}=1$, on $V_q$
\[
 \mathcal C^\nu-1=e^{2\pi i\nu\varpi_x}-1
 =2\pi i\nu\,\mathsf m\,\mathsf E(\mathsf m),\qquad
 \mathsf E(\mathsf m)=\sum_{k\leq q}\frac{\mathsf E^{(k)}(0)}{k!}\,
 \mathsf m^k ,
\]
and $\mathsf E(\mathsf m)$ is the identity plus a nilpotent operator, hence
invertible, and commutes with $\mathsf m$. This proves the equivalence. For
the formula, write
$\varpi_x=2x_P(P-x_P)+(P-x_P)^2-2x_Q(Q-x_Q)-(Q-x_Q)^2$ and use
$(P-x_P)^k\partial^\beta\delta_x=(-1)^k\frac{\beta_P!}{(\beta_P-k)!}\,
\partial^{\beta-ke_P}\delta_x$ for $k\leq\beta_P$, and zero otherwise,
together with the same identity in $Q$.
\end{proof}

\paragraph{Labels and rows.}
We recall the set-up of Steps~1--3 of the proof of
Proposition~\ref{prop:moving-certificate} in the present case, in which all
data are rational. The classes are $\{0,+,-\}$, with
$\Gamma_0(t)=d^{-1}\Lambda_1$, $\Gamma_+(t)=\Lambda_t$,
$\Gamma_-(t)=\Lambda_{1/t}$. A \emph{Laurent vector} is an element of
$\QQ[t,t^{-1}]^2$, regarded as a map $(0,\infty)\to\RR^2$. The labels are
$\mathfrak L=\{0\}\sqcup\bigl(\{0,+,-\}\times(\ZZ^2\setminus\{0\})\bigr)$,
with the Laurent vectors, in light-cone coordinates,
\[
 x_0=0,\qquad x_{0,m,n}=(m/d,\,n/d),\qquad x_{+,m,n}=(mt,\,n/t),\qquad
 x_{-,m,n}=(m/t,\,nt).
\]
For every $t>0$ the map $\lambda\mapsto x_\lambda(t)$ sends $\mathfrak L$
onto $\Sigma_d(t)$. A \emph{dual vector} of the class $i$ is a Laurent
vector $x_{i,m,n}$ with $(m,n)\neq0$ and, for $i=0$, $m,n\in d^2\ZZ$; its
values lie in $\Gamma_i(t)^\vee\setminus\{0\}$. A \emph{label array} is an
element $\hat c\in\CC^{\mathfrak L\times\mathcal A_q}$, and a \emph{row} is
a finitely supported function on $\mathfrak L\times\mathcal A_q$ with
values in $\QQ[t,t^{-1}]$; for each $t>0$ it acts on label arrays. We
consider two kinds of rows.
\begin{enumerate}[(1)]
\item \emph{Translation rows.} Let $\mathbf w=(w_0,w_+,w_-)$ consist of
 dual vectors of the three classes, let $k\geq q+1$ be an integer, $Y$ a
 Laurent vector and $\beta\in\mathcal A_q$. Put
 \begin{equation}\label{eq:eff-translation-row}
 \mathsf r_{\mathbf w,k,Y,\beta}(\hat c)
 =\sum_{\kappa\in\{0,\dots,k\}^3}\ \prod_{i}
 (-1)^{k-\kappa_i}\binom k{\kappa_i}
 \sum_{\substack{\lambda\in\mathfrak L\\
 x_\lambda\equiv Y+\kappa_0w_0+\kappa_+w_++\kappa_-w_-}}
 \hat c_\beta(\lambda),
 \end{equation}
 where $\equiv$ is equality of Laurent vectors; the inner sum has at most
 one term. This is the generic row of Step~3 of the proof of
 Proposition~\ref{prop:moving-certificate} for the operator
 $\mathsf D_{\mathbf w,k}(t)=\prod_i(\tau_{w_i(t)}-I)^k$.
\item \emph{Rational phase rows.} For $\lambda\in\mathfrak L$ and
 $|\beta|\leq q-1$, the bracket in \eqref{eq:eff-phase-row}, formed with
 $c_{\beta'}=\hat c_{\beta'}(\lambda)$ and $x=x_\lambda$.
\end{enumerate}
Let $\mathcal R_{d,q}$ be the set of all these rows. Equality in
$\QQ[t,t^{-1}]$ is decidable, so each row is computable from its
parameters, and $\mathcal R_{d,q}$ can be enumerated as
$\mathsf r_1,\mathsf r_2,\dots$.

\begin{proposition}[A terminating search for the row identities]
\label{prop:eff-row-search}
For every $\beta$ with $1\leq|\beta|\leq q$ the coordinate row
$\hat c\mapsto\hat c_\beta(0)$ is a $\QQ(t)$-linear combination of finitely
many rows of $\mathcal R_{d,q}$. Consequently the search which, for
$i=1,2,\dots$, decides by exact elimination over $\QQ(t)$ whether all
these coordinate rows lie in the span of $\mathsf r_1,\dots,\mathsf r_i$
halts, and returns $i_0$ and $a_{\beta,i}\in\QQ(t)$ such that
\begin{equation}\label{eq:eff-row-identity}
 \hat c_\beta(0)=\sum_{i\leq i_0}a_{\beta,i}(t)\,\mathsf r_i(\hat c)
 \qquad(1\leq|\beta|\leq q)
\end{equation}
for all label arrays $\hat c$ and all $t>0$ that are not poles of the
$a_{\beta,i}$.
\end{proposition}
\begin{proof}
Fix a real $t_*>0$ transcendental over $\QQ$. Evaluation at $t_*$ is
injective on $\QQ[t,t^{-1}]$, so two Laurent vectors that agree at $t_*$
agree identically. Hence $\lambda\mapsto x_\lambda(t_*)$ is a bijection of
$\mathfrak L$ onto $\Sigma_d(t_*)$, and label arrays are the same as arrays
on $\Sigma_d(t_*)\times\mathcal A_q$. The radii $1$, $t_*$, $1/t_*$ are
pairwise incommensurable, so the three lattices $\Gamma_i(t_*)$ form a
transverse family of hyperbolic grids with support $\Sigma_d(t_*)$ and
phase exponent $d^2$. Lemma~\ref{lem:formal-rigidity} provides finitely
many operators $\mathsf D_l=\prod_i(\tau_{w_{i,l}(t_*)}-I)^{m_l}$, with
dual vectors $w_{i,l}$ and $m_l\geq q+1$, such that every array $c$ on
$\Sigma_d(t_*)$, of arbitrary growth, whose distribution $\mathsf T_c$
satisfies $\mathsf D_l\mathsf T_c=0$ for all $l$ and
$\mathcal C^{d^2}\mathsf T_c=\mathsf T_c$ has $c_\beta(0)=0$ for
$1\leq|\beta|\leq q$. As in Step~4 of the proof of
Proposition~\ref{prop:moving-certificate}, the coefficient
\eqref{eq:rig-translation-row} of $\partial^\beta\delta_y$ in
$\mathsf D_l\mathsf T_c$ is either zero for all $c$ or the value at $t_*$
of a row \eqref{eq:eff-translation-row} with $Y(t_*)=y$. Since $d^2s$ is
integer valued on $\Sigma_d(t_*)$, Lemma~\ref{lem:eff-local-phase} shows
that $\mathcal C^{d^2}\mathsf T_c=\mathsf T_c$ is equivalent to the
vanishing on $c$ of all rational phase rows at $t_*$. So
$c\mapsto c_\beta(0)$ vanishes on every array annihilated by all rows of
$\mathcal R_{d,q}$ evaluated at $t_*$, and by
Lemma~\ref{lem:finite-rows} it is a complex linear combination of
finitely many of them, say of the values at $t_*$ of
$\mathsf r_1,\dots,\mathsf r_i$.

Let $\mathsf M$ be the matrix of $\mathsf r_1,\dots,\mathsf r_i$ in the
finitely many columns in which these rows or the coordinate row have a
nonzero entry, and $\mathsf M'$ the matrix with the coordinate row
adjoined. Their entries lie in $\QQ[t,t^{-1}]$, so a minor vanishes if and
only if its value at $t_*$ does. Hence the ranks of $\mathsf M$ and
$\mathsf M'$ over $\QQ(t)$ equal the ranks over $\CC$ of their values at
$t_*$, which coincide. Therefore the coordinate row lies in the
$\QQ(t)$-span of $\mathsf r_1,\dots,\mathsf r_i$, and the search halts at
the first index for which this holds for all $\beta$. An identity between
rows with coefficients in $\QQ(t)$ may be evaluated at every $t>0$ that is
not a pole of a coefficient.
\end{proof}

The number $t_*$ occurs only in the proof that the search halts; the search
itself is exact linear algebra over $\QQ(t)$. The identity
\eqref{eq:eff-row-identity} can take the place of
\eqref{eq:rig-moving-row-identity} in the proof of
Proposition~\ref{prop:moving-certificate}: by
Lemma~\ref{lem:eff-local-phase} the rational phase rows vanish, like the
rows $\mathsf p^t_{\lambda,\beta}$ used there, on the label array
\eqref{eq:rig-label-array} of every distribution $\mathsf T$ supported in
$\Sigma_d(t)$, of local order at most $q$, with
$\mathcal C^{d^2}\mathsf T=\mathsf T$. The next proposition makes the
remaining data of that proof computable at an algebraic parameter.

\begin{proposition}[Algebraic parameters]\label{prop:eff-algebraic-rows}
Let $t_0>0$ be a real algebraic number.
\begin{enumerate}[(i)]
\item One can compute a transverse family
 $\Gamma_i=d_i^{-1}\Lambda_{r_i}$, with $r_i\in\QQ(t_0)$, whose support
 $S_0$ contains $\Sigma_d(t_0)$. The search analogous to that of
 Proposition~\ref{prop:eff-row-search}, over the translation rows
 \eqref{eq:rig-translation-row} of all operators
 $\prod_i(\tau_{w_i}-I)^k$ with $w_i\in\Gamma_i^\vee\setminus\{0\}$ and
 $k\geq q+1$, and the rational phase rows at the points of $S_0$, with
 exact arithmetic in $\QQ(t_0)$, halts and returns a row identity
 \eqref{eq:rig-row-identity} for $S_0$ with coefficients in $\QQ(t_0)$,
 in which the phase rows are the rational ones.
\item Given \eqref{eq:eff-row-identity}, one can compute a rational
 $\varrho\in(0,t_0/2)$, an integer $K\geq0$ and a rational $C_1$ with the
 following properties. Let $\mathsf r_\mu$ range over the translation rows
 occurring in \eqref{eq:eff-row-identity}, with coefficients $a_\mu$, and
 let $\mathfrak d_\mu$ be the function defined for $\mathsf r_\mu$ in Step~6
 of the proof of Proposition~\ref{prop:moving-certificate}. For
 $0<|t-t_0|<\varrho$ the number $t$ is neither a pole of a coefficient of
 \eqref{eq:eff-row-identity} nor a zero of a function $\mathfrak d_\mu$, and
 \[
 |a_\mu(t)|\,|\mathfrak d_\mu(t)|^{-(q+1)^2}\leq C_1\,|t-t_0|^{-K}.
 \]
 Consequently assertions (ii) and (iii) of
 Proposition~\ref{prop:moving-certificate} hold, for distributions
 supported in $\Sigma_d(t)$, with $\varepsilon_0=\varrho$, with this $K$,
 and with the tests $f_{\mu,t}=a_\mu(t)\,\omega_\mu(t)\,\mathbb S\psi_{\mu,t}$
 formed from \eqref{eq:eff-row-identity} as in Step~7 of that proof,
 $\omega_\mu(t)$ being the multiplier of the translation operator of
 $\mathsf r_\mu$.
\end{enumerate}
\end{proposition}
\begin{proof}
(i) Equality and integrality of elements of $\QQ(t_0)$ are decidable, hence
so are the rationality of $t_0$ and of $t_0^2$ and the membership of a
point with coordinates in $\QQ(t_0)$ in a lattice $d_i^{-1}\Lambda_{r_i}$.
If $t_0=p_1/p_2$ is rational, take the single grid
$\operatorname{lcm}(d,p_1p_2)^{-1}\Lambda_1$. If $t_0$ is irrational and
$t_0^2=p_1/p_2$, take $d^{-1}\Lambda_1$ and $(p_1p_2)^{-1}\Lambda_{t_0}$;
the latter contains $\Lambda_{1/t_0}$ because
$(m/t_0,nt_0)=\bigl(mp_2^2\,t_0/(p_1p_2),\,np_1^2/(p_1p_2t_0)\bigr)$. If
$t_0^2$ is irrational, take $d^{-1}\Lambda_1$, $\Lambda_{t_0}$ and
$\Lambda_{1/t_0}$. In each case the radii are pairwise incommensurable.
The rows have entries in $\QQ(t_0)$ and are computable. As in the proof of
Proposition~\ref{prop:eff-row-search},
Lemmas~\ref{lem:formal-rigidity}, \ref{lem:eff-local-phase}
and~\ref{lem:finite-rows} show that each coordinate row is a complex
combination of finitely many of them, and the rank of a matrix with
entries in $\QQ(t_0)$ is the same over $\QQ(t_0)$ and over $\CC$.

(ii) Let $\mathsf r_\mu=\mathsf r_{\mathbf w,k,Y,\beta}$ be one of the
finitely many translation rows in \eqref{eq:eff-row-identity}. In Step~6
of the proof of Proposition~\ref{prop:moving-certificate} the function
$\mathfrak d_\mu(t)$ is the product of the factors $e^{2\pi ig(t)}-1$ over
the functions $g=\mathsf v^\star_{i,\mathbf k}$ attached to the pairs
$(i,\mathbf k)$ of type two; each $g$ is the value of one of the
coordinate forms $(du,dv)$, $(u/t,tv)$, $(tu,v/t)$ on the Laurent vector
$Y+\sum_ik_iw_i$. Thus $g\in\QQ[t,t^{-1}]$, and $g$ is not an integer
constant. Types and the choices $\iota(i,\mathbf k)$ are decided by exact
computation in $\QQ[t,t^{-1}]$. On $[t_0/2,2t_0]$ each $g$ is bounded by a
computable constant, so $g(t)\in\ZZ$ holds there only at the roots of the
finitely many nonzero polynomial equations $g(t)=m$, $m$ an integer below
that bound. These roots, together with the poles of the $a_{\beta,i}$,
form a finite set of real algebraic numbers whose isolating intervals can
be computed and whose equality with $t_0$ can be decided. Choose $\varrho$
smaller than the distance from $t_0$ to the other elements of this set.
For each factor of $\mathfrak d_\mu$, either $g(t_0)\notin\ZZ$, and then
$|e^{2\pi ig(t)}-1|\geq4\dist(g(t),\ZZ)$ has a computable positive lower
bound near $t_0$; or $g(t_0)=m\in\ZZ$, and then
$g(t)-m=(t-t_0)^{k'}e(t)$ with a computable $k'\geq1$ and a rational
function $e$ over $\QQ(t_0)$ with $e(t_0)\neq0$, so that
$|e^{2\pi ig(t)}-1|\geq4|g(t)-m|\geq2|e(t_0)|\,|t-t_0|^{k'}$ after
decreasing $\varrho$ by means of a bound for $e'$. The poles of the
$a_\mu$ at $t_0$ are treated in the same way. This gives the displayed
bound, with $K$ computed from the orders of vanishing as in Step~9 of that
proof. For $0<|t-t_0|<\varrho$ the number $t$ avoids the sets
$\mathsf E'$ and $\mathsf E''$ of Steps~5 and~6, and Steps~6--9 apply without change, with
\eqref{eq:eff-row-identity} in place of \eqref{eq:rig-moving-row-identity};
they use only that the translation vectors are dual vectors, that the
exponents are at least $q+1$, and that the phase rows vanish on the label
arrays of the distributions considered.
\end{proof}

With these data the obstruction of
Theorem~\ref{thm:moving-localization} acquires a computable threshold,
relative to bounds for three families of constants that are fixed by
their proofs but are not displayed in this paper: the constants $C_k$ of
Lemma~\ref{lem:weight-derivative-bound}, the constants of
Lemma~\ref{lem:rig-mixture-family}(ii) and~(iii), and the constant of
Lemma~\ref{lem:rig-cardinal-tests}(ii). Each is a function of finitely
many integer and rational arguments. By a \emph{system of bounds}
$\mathfrak b$ we mean computable functions of these arguments that are
upper bounds for the three families.

\begin{proposition}[A computable obstruction to localization]
\label{prop:eff-obstruction}
Let $\mathfrak b$ be a system of bounds. There is an algorithm, using
$\mathfrak b$, which, given a rational $g\in(0,\frac12]$, an integer
$d\geq1$, a real algebraic $t_0>0$, a rational $p>0$, a rational $C\geq1$
and an integer $A\geq0$, returns rationals $\varrho>0$ and $\alpha>0$ with
the following property. There do not exist an admissible partition
function of gap $g$ at $c=1+12a$ with $0<a<\alpha$ and a real $t$ with
$|t-t_0|<\varrho$ such that every state with $\Delta_j\leq2L$,
$L=\log(1/a)$, admits a real point $X_j\in\Sigma_d(t)$ with
\begin{equation}\label{eq:eff-localization}
 s(X_j)=s_j,\qquad
 \bigl|\Delta_j-|X_j|^2\bigr|\leq C\,a^p(1+L)^A .
\end{equation}
\end{proposition}
\begin{proof}
\emph{Certificates.} Let $p'=\min\{p,1\}$, let $N$ be the least integer
with $(N+1)p'>2$, and $q=2N$. Run the search of
Proposition~\ref{prop:eff-row-search} and compute $\varrho$ and $K$ by
Proposition~\ref{prop:eff-algebraic-rows}(ii). By Step~9 of the proof of
Proposition~\ref{prop:moving-certificate}, the bounds of
Proposition~\ref{prop:eff-algebraic-rows}(ii) and $\mathfrak b$, one
computes a rational $M_1$ such that the tests $f_{\mu,t}$, say $n$ in
number, satisfy
\eqref{eq:rig-test-envelope} with $2N+2$ derivatives, $b=1$ and
$M=M_1|t-t_0|^{-K}$, for $0<|t-t_0|<\varrho$. Put
$\vartheta=\min\{p,1,1/(8(K+1))\}$, let $N_0$ be the least integer with
$(N_0+1)\vartheta>2$, and apply
Proposition~\ref{prop:eff-algebraic-rows}(i) with $q_0=2N_0$ in place of
$q$. As in the proof of Theorem~\ref{thm:origin-certificate}, its row
identity yields finitely many tests $f^0_l$ and a constant $C_0$ such that
\eqref{eq:rig-certificate} holds for the even tempered distributions
supported in $S_0\supset\Sigma_d(t_0)$, of local order at most $q_0$, that
are fixed by $\mathcal C$; here $C_0$ is a rational bound for the sums of
the absolute values of the coefficients, and by $\mathfrak b$ one computes
a rational $M_0$ such that the $f^0_l$ satisfy
\eqref{eq:rig-test-envelope} with $2N_0+2$ derivatives, $b=1$ and
$M=M_0$. The denominators that occur are numbers $e^{2\pi ig}-1$ with
$g\in\QQ(t_0)\setminus\ZZ$, and are bounded below by $4\dist(g,\ZZ)$.

\emph{Preliminary bounds.} Let $Z$, $a$, $t$ and the points $X_j$ be as
in the statement, with $a\leq\min\{g^2/4,1/64\}$, put
$\vartheta_a=Ca^p(1+L)^A$, and assume $\vartheta_a<g$. Since
$aL\leq\frac12$ and $2L\geq1$,
\eqref{eq:count-bound} gives
$\#\{j:\Delta_j\leq2L\}\leq2e^{2\pi}A_g(1+L)$. Since
$2\pi a\leq\frac18$, \eqref{eq:thermal-tail} with $\beta=1$ and $E_0=2L$
gives
\[
 \sum_{\Delta_j>2L}e^{-\Delta_j}\leq A_g\Bigl(\frac{16L}7+\frac{64}{49}
 \Bigr)a^{2-4\pi a}\leq3A_g(1+L)\,a^{7/4}.
\]
The set $\Sigma_d(t)$ is invariant under both reflections and contains
$\Lambda_1$.

\emph{First regime: $|t-t_0|\geq a^\vartheta$.}
Let $\mathsf T_a$ be the distribution \eqref{eq:rig-taylor-distribution}
for $\Sigma=\Sigma_d(t)$, $E_*=2L$, $\varepsilon=\vartheta_a$ and the order
$N$. By Lemma~\ref{lem:rig-taylor-distribution}(i),(ii), by
\eqref{eq:rig-moving-certificate} and by \eqref{eq:rig-defect-bound} with
$M=M_1|t-t_0|^{-K}\leq M_1a^{-K\vartheta}$,
\[
 \frac a4\leq n\,C_Ne^5M_1\,a^{-K\vartheta}\Bigl[
 2e^{2\pi}A_g(1+L)\bigl((C+1)a^{p'}(1+L)^A\bigr)^{N+1}+a^{N+1}
 +3A_g(1+L)a^{7/4}\Bigr],
\]
where $C_N$ is the constant of Lemma~\ref{lem:rig-taylor-distribution},
bounded through $\mathfrak b$. As $(N+1)p'>2$ and $K\vartheta<\frac18$,
every power of $a$ on the right is at most $a^{13/8}$. Hence
$1\leq C_1'\,a^{5/8}(1+L)^{1+A(N+1)}$ with a computable rational $C_1'$.

\emph{Second regime: $|t-t_0|<a^\vartheta$.} As in the second case of the
proof of Theorem~\ref{thm:moving-localization}, replace each $X_j$ on
$\Lambda_t\cup\Lambda_{1/t}$ by the point $X_j'$ of
$\Lambda_{t_0}\cup\Lambda_{1/t_0}$ with the same charges, and put
$X_j'=X_j$ otherwise. The spin is unchanged, and since
$t,t_0\geq t_0/2$ and $|X_j|^2\leq\Delta_j+\vartheta_a\leq2L+1$, the
estimate given there yields
$\bigl||X_j'|^2-|X_j|^2\bigr|\leq(2L+1)\bigl(e^{4a^\vartheta/t_0}-1\bigr)
\leq C_2(1+L)a^\vartheta$ with a computable $C_2$, provided
$4a^\vartheta\leq t_0$. Thus \eqref{eq:eff-localization} holds for the
points $X_j'\in\Sigma_d(t_0)$ with the right side
$\vartheta_a'=(C+C_2)a^\vartheta(1+L)^{\max\{A,1\}}$, because
$\vartheta\leq p$. Assume $\vartheta_a'<g$ and let $\mathsf T_a'$ be the
distribution \eqref{eq:rig-taylor-distribution} for
$\Sigma=\Sigma_d(t_0)$, $E_*=2L$, $\varepsilon=\vartheta_a'$ and the order
$N_0$. By Lemma~\ref{lem:rig-taylor-distribution} and
\eqref{eq:rig-certificate},
\[
 \frac a4\leq C_0C_{N_0}e^5M_0\Bigl[
 2e^{2\pi}A_g(1+L)\bigl(\vartheta_a'+a\bigr)^{N_0+1}+a^{N_0+1}
 +3A_g(1+L)a^{7/4}\Bigr].
\]
As $(N_0+1)\vartheta>2$, every power of $a$ on the right is at most
$a^{7/4}$, and $1\leq C_3'\,a^{3/4}(1+L)^{1+\max\{A,1\}(N_0+1)}$ with a
computable rational $C_3'$.

\emph{The threshold.} The requirements $\vartheta_a<g$,
$4a^\vartheta\leq t_0$, $\vartheta_a'<g$ and the negations of the two
final inequalities are finitely many conditions of the form treated in
Lemma~\ref{lem:eff-cutoff}, after the constants have been enlarged to
rational numbers. Let
$2^{-k}$ be the resulting cutoff and put
$\alpha=\min\{g^2/4,1/64,2^{-k}\}$. For $0<a<\alpha$ both regimes lead to
a contradiction; the case $t=t_0$ belongs to the second.
\end{proof}

A system of bounds exists, since the proofs of the three lemmas consist
of finitely many explicit estimates; but none is written down here, so
the algorithm of Proposition~\ref{prop:eff-obstruction} is specified only
up to this choice. By Lemma~\ref{lem:grid-circles} a point of
$d^{-1}\Lambda_1$ of integer spin lies in $\Sigma_0$, so the proposition
is a counterpart, effective relative to $\mathfrak b$, of
Corollary~\ref{cor:rig-threshold}, and thus of
Theorems~\ref{thm:fixed-localization} and~\ref{thm:moving-localization},
for $\mathcal R_0=\mathcal R_d$, $u_*=2$ and $t$ near $t_0$.

\subsection{What remains}
\label{subsec:eff-remains}

To derive an effective form of Theorem~\ref{thm:main} from
Theorem~\ref{thm:conditional-threshold} one must exhibit, for rational $g$,
an effective enumeration of local exclusion data covering $\mathcal B_g$,
together with a proof that each datum is certified. The proof of
Theorem~\ref{thm:main} indicates how this might be done. It excludes a
limit $\sigma(R,t_0)$ by three different arguments.
\begin{enumerate}[(1)]
\item If $t_0$ is not a half-integer and lies outside the finite
 exceptional set of Lemma~\ref{lem:exceptional-set}, the fixed kernel
 families of Propositions~\ref{prop:generic-localization} (for $R>1$,
 $R\neq2$) and~\ref{prop:one-two-localization} (for $R\in\{1,2\}$) apply.
 Here one box would have to serve a whole interval of values of $t_0$,
 with constants uniform on the interval.
\item At the remaining non-half-integer values of $t_0$, which are
 algebraic, the kernels are adapted to the arithmetic of $t_0$ as in the
 proof of Theorem~\ref{thm:half-integer-limits}.
\item At the finitely many pairs of half-integers, the argument of
 Section~\ref{sec:collision} applies, with its case distinctions.
\end{enumerate}
In each case the proof considers a sequence converging to $\sigma(R,t_0)$,
fixes finitely many cluster counts by
Corollary~\ref{cor:cluster-stabilization}, derives a localization of all
states with $\Delta\leq\log(1/a)$ within a power of $a$, and concludes by
Theorem~\ref{thm:moving-localization}. Three changes would turn such a
proof into a certified local exclusion covering $\sigma(R,t_0)$. First, the
stabilized counts are imposed as a box by
Lemma~\ref{lem:eff-cluster-counts}; this is unproblematic, since only
finitely many windows occur and the reference clusters are located by
rational functions of the radii. Secondly,
Theorem~\ref{thm:moving-localization} is replaced by
Proposition~\ref{prop:eff-obstruction}; since that proposition is
formulated for the window $\Delta_j\leq2L$, whereas
Sections~\ref{sec:kernels} and~\ref{sec:collision} localize the states
with $\Delta_j\leq L$, the localization steps must first be repeated in
the window $2L$, which changes only constants. Thirdly, every intermediate
estimate is proved with an explicit constant, valid for all admissible
partition functions whose observables lie in the box, after which the
finitely many smallness conditions are met by Lemma~\ref{lem:eff-cutoff}.

The third change has not been carried out. The estimates concerned are the
following.
\begin{enumerate}[(i)]
\item \emph{Peak budgets.} In Lemmas~\ref{lem:peak-budget}
 and~\ref{lem:resolved-budget}: the constants $C$ of
 \eqref{eq:ker-peak-budget} and $C_{\rm B}$ of
 \eqref{eq:col-resolved-budget} (the exponent $\pi\varrho^2/4$ and the
 restriction $a\leq\frac14\epsilon^2$ on the Gaussian width $\epsilon$
 are explicit), and the radii $\varrho$, $\varrho_a$ of the
 neighbourhoods of the Fourier centres in which states are counted or
 excluded.
\item \emph{Local zeros.} The lower bounds for the kernels near the states
 that anchor their negative peaks, in terms of the displacement of the
 state, and the radii on which these bounds hold; in the collision case,
 the constant in the lower bound $c\,|t-T|^2$ of
 Lemma~\ref{lem:quadratic-collisions} for separations and sine factors.
\item \emph{Taylor remainders and central shifts.} The constants of
 Lemma~\ref{lem:weight-derivative-bound} and
 Corollary~\ref{cor:central-shift}, and the envelope constants of each
 test function to which they are applied. The lemma makes these explicit
 in principle, since all tests are explicit Gaussian mixtures; this
 includes the system of bounds assumed in
 Proposition~\ref{prop:eff-obstruction}.
\item \emph{Row estimates.} The constants of the scalar-row estimate of
 Proposition~\ref{prop:scalar-row}; the constants and smallness
 conditions of Lemma~\ref{lem:three-projection} are already explicit.
\item \emph{The normal form.} The constants of
 Proposition~\ref{prop:grid-projection}, Lemmas~\ref{lem:normal-form}
 and~\ref{lem:moment-matching} and Theorem~\ref{thm:comparison} at the
 fixed Taylor order $n$ used, including the power of the logarithm.
 Source (c) was removed above only for the origin certificates; the
 finite-dimensional estimate of Proposition~\ref{prop:grid-projection}
 would require a certified search of its own.
\item \emph{The collision scale.} The two constants in the comparison
 $c\,\delta_a\leq\theta_a\leq C\delta_a$ between the collision scale and
 the four-scalar displacement, and the threshold in $\delta_a$ below which
 Theorem~\ref{thm:comparison} places the selected states in the
 neighbourhoods of (i) and (ii).
\end{enumerate}
Apart from the explicit ones just noted, none of these constants is
derived in this paper. Consequently no certified
local exclusion has been exhibited at any point of $\mathcal B_g$,
hypothesis (i) of Theorem~\ref{thm:conditional-threshold} has not been
verified for any $g$, and no value of $\epsilon(g)$ has been computed.
Deriving the constants is a finite task, but until it is done the
effectivity of $\epsilon(g)$ is open.

Even with these constants the output of the algorithm of
Theorem~\ref{thm:conditional-threshold} would not be self-certifying. The
searches of Propositions~\ref{prop:eff-coarse-modulus},
\ref{prop:eff-row-search} and~\ref{prop:eff-algebraic-rows} and the first
search of Theorem~\ref{thm:conditional-threshold} verify what they find: a
cover with a margin, or an exact linear identity. The thresholds
$\alpha_i$, by contrast, enter as data, and their validity rests on the
proofs of the local exclusions; an error in one of those proofs would not
be detected by the algorithm (Remark~\ref{rem:eff-content}).

Two features of the bookkeeping are sound independently of the missing
constants. First, no step of the procedures compares transcendental
quantities for exact equality. Exact decisions are made only in $\QQ$,
$\QQ(t)$ and $\QQ(t_0)$; real numbers such as values of the functions
$\mathsf F_\tau$ enter only through strict inequalities verified with a
margin by Lemma~\ref{lem:eff-positivity}, and a verification that does not
succeed is never read as an equality. Secondly, no step requires deciding
the order of the dimensions of states of an unknown partition function.
The boxes are open conditions on continuous observables. The ordering of
the states in Step~1 of the proof of
Proposition~\ref{prop:eff-coarse-modulus}, and the case distinctions of
Sections~\ref{sec:kernels} and~\ref{sec:collision} (for instance which of
the two radii is pinned, or whether $\delta_a$ is below a fixed power of
$a$), occur only in correctness proofs, where the exclusion must be established in every case; they are
not branches of an algorithm.

Finally, the finite orders involved indicate that no practical bound should
be expected from this route. The argument of Section~\ref{sec:collision}
is run with the following fixed choices
(Remark~\ref{rem:col-quantifiers}): separations bounded below by
$c\,\theta_a^2$ (Lemma~\ref{lem:quadratic-collisions}); losses of at most
$\theta_a^{-36}$ in the resolved estimates; matching of the selected
clusters to accuracy $\theta_a^{60}$ and the bound $a\leq\theta_a^{1000}$
(Definition~\ref{def:col-resolved}); the inequality
$a\leq\delta_a^{20000}$ from Theorem~\ref{thm:four-scalar-slow}; and
Taylor order $n=20000$ in the normal form, the matching bound
\eqref{eq:col-comparison-matching} of Theorem~\ref{thm:comparison}
carrying the exponent $\frac1{84}=\frac13\cdot\frac14\cdot\frac17$ (the
last factor being the loss in Lemma~\ref{lem:moment-matching}), and
$20000/84$ exceeding $200$. The final localization exponents are then
$\frac{29}{500}$ and $\frac{119}{1125}$, so that
Proposition~\ref{prop:eff-obstruction} would be used with
$p=\frac{29}{500}$, that is, with Taylor order $N=34$ and moving
certificates of local order $68$, and with certificates at $t_0$ of
local order $2N_0$, where
$(N_0+1)\min\{\frac{29}{500},\frac1{8(K+1)}\}>2$. The normal form at $n=20000$ concerns distributions of
local order $40000$ on the rational grid. These orders are fixed before
$a$ and serve an existence proof; they were not chosen with a view to
computation.