\section{Roadmap of the appendix}\label{app:roadmap}

The appendix proves the results of the main text, in the order of the sections, and its subsections follow those of
the body. Eight short results are proved where they are stated: Corollaries~\ref{cor:sampling}, \ref{cor:exponent},
\ref{cor:parity}, \ref{cor:precision} and~\ref{cor:barrier} and Remarks~\ref{rem:pm}, \ref{rem:entries2}
and~\ref{rem:forced}. \Cref{fig:dependency} shows how the results depend on each other.

\Cref{app:threshold} starts with \cref{lem:perturb}, which bounds how far a small change of the logits moves an
output. \Cref{app:sampling} analyzes uniform sampling with Bernstein's inequality (\cref{thm:sampling}).
\Cref{app:ldov-lb} builds attention instances with a dummy key from the gap instances of \cref{fact:chen} and proves
hardness above the threshold (\cref{thm:ldovlb}). \Cref{rem:entries} writes these instances in the normalization
of~\cite{AS23}, and \cref{cor:additive} repeats the proof with the gap $\tau=\lceil\log n\rceil$, which reaches spread
$\ln n+O(1)$ in polylogarithmic dimension. \Cref{app:curve} proves hardness below the threshold (\cref{thm:curve}): it
applies the same gadget to a group of keys and copies every key, which leaves the outputs and the spread unchanged.
\Cref{cor:exponent} combines the two sides, and this gives \cref{thm:A}.

\Cref{app:parity} proves the precision lower bound (\cref{thm:parity}): attention at high precision reveals the number
of orthogonal partners modulo $r+1$, where intersections are counted over blocks of coordinates. \Cref{app:polymethod}
proves the polynomial method with the dependence on the precision and on the spread made explicit (\cref{thm:poly}),
and \cref{app:dimension} carries that proof over to higher dimension (\cref{prop:polyhigh}).
\Cref{cor:parity} chooses the parameters, and with \cref{cor:precision} this gives \cref{thm:B}.

\Cref{app:sat} starts with the proof of Williams' reduction (\cref{fact:williams}). \Cref{app:cnfseth} combines it with
an exact embedding (\cref{thm:cnfseth}). \Cref{app:below-two} turns Rubinstein's protocol (\cref{fact:rub}) into gap
instances (\cref{lem:magap}) and places them in the attention instance from the proof of \cref{thm:ldovlb}. This proves
\cref{thm:belowtwo} under $\mathrm{CNF\text{-}SETH}_{c_0}$, without \cref{hyp:ldov}. These two results give
\cref{thm:C}. \Cref{app:barrier} derives Klauck's tradeoff between the proof length and the communication
(\cref{lem:klauck}) from Razborov's corruption bound (\cref{fact:razborov}). \Cref{thm:barrier} then turns a gap
embedding into a Merlin--Arthur protocol for disjointness through random-sign projections, and with \cref{cor:barrier}
this gives \cref{thm:D}. \Cref{rem:forced} combines \cref{lem:magap} with \cref{lem:klauck} to show that the exponent $2$ in
\cref{thm:belowtwo} is a limit of the reduction.

\paragraph{How to read the proofs.}
We write the proofs in the structured style of Lamport~\cite{Lam95,Lam12}. A proof is a list of numbered steps, and
$\pflab{k}{j}$ is the $j$-th step at level $k$. Each step states a claim, and a proof of the claim follows it. This proof
is a short paragraph or a list of steps at the next level. The last step of each list, \textsc{q.e.d.}, proves the goal
of the list from the earlier steps. \textsc{Assume} and \textsc{Prove} state the hypothesis and the goal of a step, and
\textsc{Let} introduces a symbol. A reader who wants only the main idea can read the level-1 steps and skip their
proofs. Each restated result keeps its number from the main text.

\begin{figure}[!t]
\centering
\newcommand{\res}[2]{\hyperref[#2]{#1~\ref*{#2}}}
\begin{tikzpicture}[x=2.25cm,y=-1.12cm,font=\scriptsize,
    box/.style={align=center,rounded corners=2pt,inner sep=1.5pt,minimum width=2.04cm,minimum height=0.78cm,thin,draw=black!55},
    hyp/.style={box,fill=black!12},
    imp/.style={box,dashed},
    tool/.style={box},
    up/.style={box,fill=easy!22,draw=easy!85!black},
    low/.style={box,fill=hard!18,draw=hard!85!black},
    both/.style={box,left color=easy!22,right color=hard!18},
    bar/.style={box,fill=refcool!14,draw=refcool!85!black},
    head/.style={box,line width=1pt,draw=black},
    dep/.style={-stealth,thin,black!65},
    gadget/.style={dep,dashed}]
  % Theorems A and B
  \node[imp]  (factchen)      at (1,0)      {\res{Imp.\ Thm}{fact:chen}\\Chen};
  \node[hyp]  (hypldov)       at (2.95,0)   {\res{Hyp}{hyp:ldov}\\LDOV};
  \node[tool] (lemperturb)    at (3.95,0)   {\res{Lem}{lem:perturb}\\perturbation};
  \node[low]  (thmldovlb)     at (1,1.5)    {\res{Thm}{thm:ldovlb}\\above threshold};
  \node[low]  (thmcurve)      at (1,2.5)    {\res{Thm}{thm:curve}\\below threshold};
  \node[low]  (rempm)         at (1,3.5)    {\res{Rem}{rem:pm}\\values $\{-1,1\}$};
  \node[low]  (coradditive)   at (2.15,3.5) {\res{Cor}{cor:additive}\\additive version};
  \node[low]  (rementries)    at (3,2.35)   {\res{Rem}{rem:entries}\\entries};
  \node[up]   (thmsampling)   at (3.95,1.5) {\res{Prop}{thm:sampling}\\sampling};
  \node[up]   (corsampling)   at (3.95,3.9) {\res{Cor}{cor:sampling}\\spread $\kappa\ln n$};
  \node[both] (corexponent)   at (2.5,4.5)  {\res{Cor}{cor:exponent}\\the exponent};
  \node[head] (thmA)          at (2.5,5.5)  {\res{Theorem}{thm:A}};
  \node[low]  (thmparity)     at (5,1.5)    {\res{Thm}{thm:parity}\\mod $r+1$};
  \node[up]   (thmpoly)       at (6.4,1.5)  {\res{Prop}{thm:poly}\\polynomial method};
  \node[low]  (corparity)     at (5,2.6)    {\res{Cor}{cor:parity}\\parameter choices};
  \node[up]   (proppolyhigh)  at (7,2.6)    {\res{Prop}{prop:polyhigh}\\higher dimension};
  \node[low]  (rementriestwo) at (5,3.7)    {\res{Rem}{rem:entries2}\\bounded entries};
  \node[both] (corprecision)  at (6.2,3.7)  {\res{Cor}{cor:precision}\\precision decides};
  \node[head] (thmB)          at (5.6,5.5)  {\res{Theorem}{thm:B}};
  % Theorems C and D
  \node[hyp]  (hypcnfsethc)   at (1.15,6.75){\res{Hyp}{hyp:cnfsethc}\\CNF-SETH$_{c_0}$};
  \node[imp]  (factwilliams)  at (2.15,6.75){\res{Imp.\ Thm}{fact:williams}\\Williams};
  \node[hyp]  (hypcnfseth)    at (3.15,6.75){\res{Hyp}{hyp:cnfseth}\\CNF-SETH};
  \node[imp]  (factrub)       at (4.4,6.75) {\res{Imp.\ Thm}{fact:rub}\\Rubinstein};
  \node[imp]  (factrazborov)  at (5.7,6.75) {\res{Imp.\ Thm}{fact:razborov}\\Razborov};
  \node[low]  (thmcnfseth)    at (2.65,7.85){\res{Prop}{thm:cnfseth}\\exact embedding};
  \node[head] (thmCi)         at (3.7,7.85) {\hyperref[thm:C]{Theorem~\ref*{thm:C}(i)}};
  \node[low]  (thmbelowtwo)   at (1.65,8.95){\res{Thm}{thm:belowtwo}\\clause exponent $<2$};
  \node[low]  (lemmagap)      at (4.4,8.95) {\res{Lem}{lem:magap}\\gap instances};
  \node[head] (thmCii)        at (1.65,10.05){\hyperref[thm:C]{Theorem~\ref*{thm:C}(ii)}};
  \node[bar]  (remforced)     at (5,10.05)  {\res{Rem}{rem:forced}\\the exponent $2$};
  \node[bar]  (lemklauck)     at (5.7,7.85) {\res{Lem}{lem:klauck}\\Klauck's tradeoff};
  \node[bar]  (thmbarrier)    at (7,7.85)   {\res{Thm}{thm:barrier}\\barrier};
  \node[bar]  (corbarrier)    at (7,8.95)   {\res{Cor}{cor:barrier}\\entry bound};
  \node[head] (thmD)          at (7,10.05)  {\res{Theorem}{thm:D}};
  % arrows
  \draw[dep] (factchen) -- (thmldovlb);
  \draw[dep] (hypldov) -- (thmldovlb);
  \draw[dep] (hypldov) -- (thmparity);
  \draw[dep] (lemperturb) -- (thmsampling);
  \draw[dep] (lemperturb) -- (thmparity);
  \draw[dep] (lemperturb.east) -- (thmpoly.north);
  \draw[dep] (thmldovlb) -- (thmcurve);
  \draw[dep] (thmldovlb.south east) -- (coradditive.north);
  \draw[dep] (thmldovlb.east) -- (rementries.north west);
  \draw[dep] (thmcurve) -- (rempm);
  \draw[dep] (rempm) -- (corexponent);
  \draw[dep] (thmsampling) -- (corsampling);
  \draw[dep] (corsampling) -- (corexponent);
  \draw[dep] (corexponent) -- (thmA);
  \draw[dep] (rementries.east) -- (rementriestwo.north west);
  \draw[dep] (thmparity) -- (corparity);
  \draw[dep] (corparity) -- (rementriestwo);
  \draw[dep] (corparity) -- (corprecision);
  \draw[dep] (thmpoly) -- (corprecision);
  \draw[dep] (thmpoly) -- (proppolyhigh);
  \draw[dep] (rementriestwo) -- (thmB);
  \draw[dep] (corprecision) -- (thmB);
  \draw[dep] (hypcnfsethc) -- (thmbelowtwo);
  \draw[dep] (factwilliams) -- (thmbelowtwo);
  \draw[dep] (factwilliams) -- (thmcnfseth);
  \draw[dep] (hypcnfseth) -- (thmcnfseth);
  \draw[dep] (thmcnfseth) -- (thmCi);
  \draw[dep] (factrub) -- (lemmagap);
  \draw[dep] (lemmagap) -- (thmbelowtwo);
  \draw[dep] (lemmagap) -- (remforced);
  \draw[dep] (thmbelowtwo) -- (thmCii);
  \draw[dep] (factrazborov) -- (lemklauck);
  \draw[dep] (lemklauck) -- (thmbarrier);
  \draw[dep] (lemklauck) -- (remforced);
  \draw[dep] (thmbarrier) -- (corbarrier);
  \draw[dep] (corbarrier) -- (thmD);
  \draw[gadget,rounded corners=5pt] (thmldovlb.west) -- ++(-0.42cm,0) |- (thmbelowtwo.west);
\end{tikzpicture}
\caption{Dependencies between the results. An arrow from $X$ to $Y$ means that the proof of $Y$ uses $X$; arrows implied
by a longer path are omitted. The arrow into \cref{thm:belowtwo} is dashed because its proof reuses the attention instance
from the proof of \cref{thm:ldovlb}, not the statement, so it does not need \cref{hyp:ldov}. Gray boxes are hypotheses,
dashed boxes imported theorems and thick boxes the theorems of the introduction. Green marks upper bounds, orange lower
bounds and blue the barrier; a box with both green and orange states both bounds. \Cref{rem:pm} also applies to
\cref{thm:ldovlb,cor:additive,thm:belowtwo}, which gives \cref{thm:C}(ii) at every nontrivial constant precision; only its
use in \cref{cor:exponent} is drawn.}
\label{fig:dependency}
\end{figure}
\newpage