\section{The probability of a safe repair menu}\label{sec:safe}

We retain the potential target sets~\eqref{eq:potential-targets}, the safety condition~\eqref{eq:safe-rotation}, and the predetermined menu from Section~\ref{sec:repair}.
The variable order is sampled uniformly; the decorations remain fixed.

\begin{proposition}\label{prop:safe-menu}
Fix $\beta>0$, an integer $k\ge2$, and a decoration bound $B\ge1$.
Put $M=4k$ and $\eta=\min\{\beta,1/6\}$.
There are constants $m_{\mathrm{safe}}(k)$ and $C_{k,B}$ such that, whenever $m\ge m_{\mathrm{safe}}(k)$, $p\ge m^{1+\beta}$, and $x$ is a uniform ordering of an arbitrary $m$-element set $X\subseteq\Fp$,
\begin{equation}\label{eq:menu-failure}
\Pr(\mathcal R_{\mathrm{menu}}^c)
\le C_{k,B}m^{1-\eta k}.
\end{equation}
The threshold $m_{\mathrm{safe}}(k)$ depends only on $k$ and the absolute constant $C$ of Theorem~\ref{thm:scalar}, and not on $\beta$.
The bound is uniform over $X$ and all fixed decorations of size at most $B$.
In particular the failure probability tends to zero if $\eta k>1$.
\end{proposition}

\begin{proof}
First fix one source configuration, with cyclic order $(q_1,\ldots,q_\ell)$, where $k\le\ell\le2k$.
If all its rotations fail, choose one collision for each rotation.
For the rotation starting at $q_i$, this specifies a nonempty proper prefix $I_i$, a remote anchor $t_i$ with $\lvert t_i-b\rvert>2M$, a set
\begin{equation*}
J_i\subseteq\{t_i+1,\ldots,\min(m,t_i+M)\},
\end{equation*}
and source and target decorations of equal parity.
Writing $z_i$ for target coordinate minus source coordinate, its equation is
\begin{equation}\label{eq:collision-witness}
s_b+\sum_{u\in U}x_u+\sum_{j\in I_i}x_j
-s_{t_i}-\sum_{j\in J_i}x_j=z_i.
\end{equation}
After these choices are fixed, the system is $Hx=z$ with~\eqref{eq:witness-matrix}.
We sum over fixed witness tuples, rather than condition on the failure of other rotations.

Set
\begin{equation*}
h=2k,\qquad
\gamma=\frac1{2(2k+1)},\qquad
P=P_{2k,\gamma}.
\end{equation*}
Choose $m$ large enough for Lemma~\ref{lem:pooling}, for $L\ge M$, for $m\ge2(2k+1)L$, and for $m>2k$.
These conditions depend only on $k$ and the absolute scalar constant; they hold eventually.
The prime-size condition gives $p>2k$.
If the anchors have $q$ free clusters, Lemma~\ref{lem:witness-columns} gives affine dimension at least $(\ell+q)/2$, a baseline of multiplicity at least $\gamma m$, and $q$ repeated independent directions.
Pad $H$ with zero rows to height $2k$.
Neither its affine dimension nor its column multiplicities change.
Lemma~\ref{lem:pooling} therefore gives
\begin{equation}\label{eq:fixed-witness-probability}
\Pr(Hx=z)\le Pm^{-(\ell+q)/2-\eta q}.
\end{equation}

For fixed $b,\ell,q$, Lemma~\ref{lem:anchor-count} bounds the anchor tuples by $A_\ell m^qL^{\ell-q}$.
The remoteness restrictions only reduce this count.
For each rotation, the prefix has at most $2k$ choices, each decoration has at most $B(M+1)$ choices, and $J_i$ has at most $2^M$ choices.
Thus, for fixed anchors, the remaining witness choices number at most $E_{k,B}^{\ell}$, where
\begin{equation*}
E_{k,B}=2k[B(M+1)]^2 2^M.
\end{equation*}
Counting pairs of incompatible parities only enlarges this bound.
Combining the counts with~\eqref{eq:fixed-witness-probability} gives
\begin{align*}
\Pr(\text{the fixed source has no safe rotation})
&\le PA_\ell E_{k,B}^{\ell}
\sum_{q=0}^{\ell}m^qL^{\ell-q}
m^{-(\ell+q)/2-\eta q}\\
&\le PA_\ell E_{k,B}^{\ell}
\sum_{q=0}^{\ell}m^{-(\ell-q)/6-\eta q}\\
&\le D_{k,B}m^{-\eta\ell},
\end{align*}
where
\begin{equation*}
D_{k,B}=P\max_{k\le\ell\le2k}
(\ell+1)A_\ell E_{k,B}^{\ell}.
\end{equation*}
The second inequality uses $L\le m^{1/3}$; the last uses $\eta\le1/6$.
The case $q=0$ is included.

By~\eqref{eq:menu-size}, the predetermined menu has at most $(1+4k^2)m/k$ entries.
A union bound proves~\eqref{eq:menu-failure} with
\begin{equation*}
C_{k,B}=\frac{1+4k^2}{k}D_{k,B}.
\end{equation*}
All configurations are listed before sampling, so the later selection of rotations introduces no additional conditioning.
\end{proof}

The scalar saving $1/6$ and the clustered-anchor saving $1/6$ coincide at the cube-root scale.
More generally, $L=m^\rho$ gives gains $\rho/2$ and $1/2-\rho$, whose minimum is maximised at $\rho=1/3$.
The estimate is uniform on every fibre fixing the nonvariable entries and variable coordinate set of the cell construction.
The local-separation event is intersected with this event only after averaging the fibre bounds.