% Constructive proof of the upper bound. \section{The upper bound: a complete constructive proof}\label{sec:tools} For $4\le n\le10$ we use the exhaustive BFS in Section~\ref{sec:certificate}. Throughout the construction below, $n\ge11$. The complete finite certificate is in Appendix~\ref{app:code}. Here $p$ denotes the parity of $n$, $q$ counts nontrivial cycles, and $p_i$ is the position of token $i$ in the target list. Put \begin{longtable}{@{}p{.28\textwidth}p{.67\textwidth}@{}} \toprule Notation & Definition or role\\\midrule $m,p,h$ & $n=2m+p$, $p\in\{0,1\}$, $h=\floor{(n-1)/2}$.\\ $Q,N$ & $Q=\floor{n^2/4}=m(m+p)$, $N=2Q-m=\binom n2$.\\ $F,d_i$ & $F(i)=i+d_i$ is the balanced periodic destination map.\\ $\Delta,C$ & $\Delta=\sum_i|d_i|$; $C$ is affine length~\eqref{eq:C}.\\ $f,q,\rk$ & $f=\#\{i:d_i=0\}$, $q$ counts nontrivial cycles; $\rk=n-f-q$.\\ $Z,\mathcal L$ & $Z=\Delta-C-\rk$, $\mathcal L=\sum_B(|B|-2)$.\\ $\eps,\delta,A$ & $\eps=Q-\Delta$, $\delta=Q-m-C$, $A=2\eps+p-f$.\\ $D$ & $D=N-C-\Delta=\delta+\eps$, the available rotation excess.\\ \bottomrule \end{longtable} Packet and gap parameters ($r,k,b_i,w_i,U,S,K$) are defined where used. The head coordinate $H$ in Section~\ref{sec:buffer} is local to that construction; later $H$ denotes a displacement deficit. It suffices to construct a word with at most $\Delta+D$ rotations: after deleting redundant exchanges, its length is at most $C+\Delta+D=N$. We call an estimate paid when its excess $\Rot-\Delta$ is at most $D$. Every route below allows arbitrary initial and final physical cursors. Only the cursor of each individual service procedure is closed. Connected load is settled in Section~\ref{sec:connected}. A zero edge permits a finite cut in Section~\ref{sec:bridges}. We then settle small invariant blocks and a large shallow packet before separating the two-component case (Section~\ref{sec:two}) from the remaining case (Sections~\ref{sec:many}--\ref{sec:certificate}). \begin{figure}[ht] \centering \includegraphics[width=\textwidth,height=.48\textheight,keepaspectratio]{proof_map_en.pdf} \caption{Dependencies in the upper proof. The connected and finite-load branches cover all lifts; within the latter, the final case uses the bounded certificate.} \label{fig:proof-map} \end{figure} \subsection{Choosing a lift and its affine invariants}\label{sec:lift} \subsubsection{Minimization over the final phase} If token $i$ has position $p_i$ in the target list, its final physical position at cursor $c$ is $p_i+c\pmod n$. Choose integers $d_i$ with \begin{equation}\label{eq:lift} \sum_i d_i=0,\qquad i+d_i\equiv p_i+c\pmod n. \end{equation} Such a lift exists: take $c=0$ and $d_i=p_i-i$. Minimize the nonnegative integer energy $\mathcal E(d)=\sum_i d_i^2$ over all lifts and phases. Extend $d_i$ periodically and put $F(i)=i+d_i$ on $\Z$. Distinct residues of $F(i)$ give a bijection with $F(i+n)=F(i)+n$; balance places it in the affine symmetric group. Its standard length is \cite[Proposition~3.1]{bjorner-brenti} \begin{equation}\label{eq:C} C(F)=\sum_{0\le i0\}. \] A positive packet port below always means a port in $\mathcal E_{\mathcal P}$. This incidence condition is needed to apply the service lemma. Load components are the components of positive edges; isolated unloaded vertices are not counted. For a balanced cluster, its signed edge flux (the number of clockwise crossings minus counterclockwise crossings) is constant: at each vertex one incoming and one outgoing arrow cancel. Summing over the $n$ edges shows that this constant is $\sum_i d_i/n=0$. Thus its load $\lambda(a)$ is even on every edge. Also \[ \Delta=\sum_{a=0}^{n-1}\lambda(a), \] since an arrow of length $|d_i|$ contributes to exactly $|d_i|$ edges. A half-load means $\lambda(a)/2$; a half-peak is its maximum. A lift is finite if it preserves some window of $n$ consecutive integer positions; its inversion number is then the ordinary one in that window. \subsubsection{Deleting redundant exchanges} Periodic adjacent transpositions form a Coxeter system \cite[Proposition~3.3]{bjorner-brenti}. By the deletion property \cite[Proposition~1.4.7]{coxeter}, pairs of $X$ letters can be deleted from any word with lift $F$ until exactly $C(F)$ exchanges remain. Every $L,R$ letter and the lifted endpoint are preserved: the location of a remaining exchange depends only on the rotations already traversed. Appendix~\ref{app:affine} gives the application and its trajectory interpretation. \subsubsection{Sorting across fixed intervals and the defect} For a finite permutation $\pi$ on $b$ positions put \[ I(\pi)=\#\{(i,j):0\le i\pi(j)\}. \] Its reflection length is $\rk(\pi)=b-\#\{\text{all cycles of }\pi\}$, the standard length in arbitrary transpositions \cite[Section~2]{diaconis-graham}; its proof is retained in Appendix~\ref{app:finite}. For the residue permutation of a lift this is $n-f-q$. If the lift preserves a common finite window,~\eqref{eq:C} is the ordinary inversion number in that window. Choose consecutive active positions $u,v$ whose residual displacements are $a>0$ and $-b<0$; all intermediate positions are fixed. If their chosen arc has length $\ell$, then $a,b\ge\ell$: a shorter displacement would have a destination already occupied by a fixed intermediate token. The palindrome of adjacent exchanges on edges $u,\ldots,v-1,v-2,\ldots,u$ exchanges the endpoints and restores the intermediate tokens. The new residuals are $\ell-b,a-\ell$. Every exchange is a descent: the destinations of the moving tokens lie on opposite sides of the fixed intermediate destinations. Hence \begin{equation}\label{eq:macro} \Delta_{\rm old}-\Delta_{\rm new}=2\ell, \qquad C_{\rm old}-C_{\rm new}=2\ell-1. \end{equation} Active positions only disappear; a token keeps its sign until its residual vanishes, and $\ell\le h$. Balance supplies another such pair until the identity is reached. If there are $M$ endpoint transpositions, then \begin{equation}\label{eq:depth} M=\Delta-C,\quad M\ge n-f-q,\quad M\equiv n-f-q\pmod2. \end{equation} The last two assertions are the usual reflection length and parity of a product of transpositions. Thus $Z\ge0$ and $Z$ is even. On the finite line the same proof needs no half-circle restriction. There $\Delta$ is Spearman's footrule (total displacement), and $\Delta=2\operatorname{dp}$ identifies it with twice the depth \cite[Theorem~1.1, Remark~1.2]{depth}. The inequality $I+\rk\le\Delta$ is the Diaconis--Graham inequality \cite[Theorem~2]{diaconis-graham}. We have proved the affine version needed here. \begin{lemma}\label{lem:reserves} For an original lift, \begin{equation}\label{eq:reserves} \eps\ge0,\quad 4\eps\ge f^2-p,\quad A\ge0,\quad D=m-q+Z+A,\quad 2\delta=\mathcal L+2Z+A, \end{equation} where $\mathcal L=\sum_B(|B|-2)$ over nontrivial cycles. Also $\Delta$ is even, $\eps\equiv Q\pmod2$, and $\eps\ge f-1$. \end{lemma} \begin{proof} If the sign counts are $a,b$, with $a+b=n-f$,~\eqref{eq:lorenz} gives $\Delta\le\min(a(n-a),b(n-b))\le(n^2-f^2)/4$. This proves the first two bounds. For $f\ge2$, $2\eps\ge(f^2-p)/2\ge f-p$; for $f=0$, $A=2\eps+p\ge0$; for $f=1,p=0$, integrality gives $\eps\ge1$. Thus $A\ge0$. Substitute $\mathcal L=n-f-2q$ to get the identities. Balance makes $\Delta$ twice the positive sum. Finally, $f^2-p\ge4(f-1)$ for $f\ge3$; the cases $f=0,1,2$ follow directly using integrality. \end{proof} \subsection{Original root packets}\label{sec:packets} For a nontrivial cycle $B$, the union $E_B$ of its arrows is a connected proper arc or the whole circle. For distinct nontrivial cycles put $B\to C$ when $E_B$ contains a vertex of $C$. That vertex is strictly inside an arrow of $B$, since the cycle supports are disjoint. These arrows define the passage graph on nontrivial cycles. A cycle reaches itself by the empty path. A source strongly connected component has no incoming edge from another strongly connected component; we call it a root packet when it is the source in Lemma~\ref{lem:source}. \begin{lemma}\label{lem:source} Each positive-load component has a unique source strongly connected component $\mathcal P$ in the passage graph. Every cycle in it reaches all other cycles of the load component. Cycles outside $\mathcal P$ lie in invariant open gaps of its support. If the original load is connected, the packet is balanced. \end{lemma} \begin{proof} If $E_B$ meets $E_C$ without being contained in it, then $B\to C$: inspect the endpoints of proper arcs; a full circle contains all vertices. Proper arcs have distinct endpoints because cycle supports are disjoint. Choose an inclusion-maximal arc. If it does not reach everything, some intersecting pair $E_B,E_C$ has $B$ reached and $C$ unreached. Necessarily $E_B\subset E_C$. Along a path from the chosen maximal arc to $B$, the first entry into an arc contained in $E_C$ gives a passage from the preceding cycle to $C$, a contradiction. Thus some cycle reaches all, and the source strongly connected component is unique. An outside cycle cannot pass through a packet vertex, since that would give reverse reachability. Its arrows and vertices therefore lie in a single open gap of the packet support; its winding is zero. With connected load, all nonzero windings belong to the packet: such a cycle covers the circle and passes through every other cycle. The windings of the whole lift sum to zero, so the packet is balanced. \end{proof} Let the packet have $r$ active vertices and $k$ cycles. The quantities $\Delta_{\mathcal P},C_{\mathcal P},Z_{\mathcal P}$ refer to the map retaining the packet and fixing its complement. Its internal gaps have sizes $b_i$ and constant even packet loads $w_i\ge2$. When the entire positive load is connected and the packet does not cover the circle, its external gap contains only fixed positions: an active cycle there would form a separate load component. Denote their number by $e$; otherwise put $e=0$. An arrow crossing an internal gap has length at least $b_i+1$, so \begin{equation}\label{eq:gapcap} b_i\le h-1=m+p-2. \end{equation} \begin{lemma}\label{lem:packetdefect} For connected original load, \begin{equation}\label{eq:packetreserve} Z_{\mathcal P}\ge k-1,\quad Z\ge Z_{\mathcal P},\quad \delta\ge\ceil{r/2}+Z_{\mathcal P}-k\ge\ceil{r/2}-1. \end{equation} For a finite packet, the stronger bound $Z_{\mathcal P}\ge2(k-1)$ holds. \end{lemma} \begin{proof} Apply~\eqref{eq:macro} to the packet alone. Its event graph has the initial active packet positions as vertices and one undirected edge $\{u,v\}$ for each endpoint transposition; repeated events are counted with multiplicity. The chords of this graph do not cross: no active vertex is inside the arc of an event, and the endpoints of later events are already active at that time. Different graph components form a noncrossing circular partition. Each original cycle lies in a graph component: the product of the endpoint transpositions preserves every graph component. Moreover, the residual displacement of a token never changes sign in~\eqref{eq:macro}. Its successive event arcs therefore cover its original arrow monotonically. If an original arrow from one graph component passes a vertex of another, noncrossing places the whole second component in an open gap between consecutive vertices of the first. The monotone event path covering that arrow contains an event crossing the entire gap; otherwise it would have an endpoint inside the gap belonging to the first component. That event has length at most $h$, so the gap has width at most $hs/2$. Let $c$ be the sum of the other internal lengths, $t=b-c-e=2b-s>0$, and $u=t-\eta$. Using $S_2\le b^2+c^2$ and $4G=(s+\eta)^2-p$ gives \begin{equation}\label{eq:dominant} 2T\le u^2+p-2\eta-4H. \end{equation} The discarded terms are $-4\eta(c+e)-4ce-2e^2\le0$. The core occupies $n-b$ consecutive positions in the complement of the gap. Represent its residue permutation in this finite interval, retaining the physical distances. Original arrows are shortest, so their lengths are at most the corresponding finite lengths. A permutation on $L$ positions with $r=2l+\eta$ active vertices has displacement at most $2l(L-l)$: the smaller sign count $z$ is at most $l$, its length sum is at most $z(L-z)$, and this increases up to $L/2$. Consequently \begin{equation}\label{eq:complement} \Delta_{\mathcal P}\le2l(n-b-l),\qquad H\ge l(u-l). \end{equation} No original majorization is assumed for this finite map. The inequalities $b\le n/2$ and $t\ge1$ give $0\le u\le2l$. Together with $H\ge0$,~\eqref{eq:dominant}--\eqref{eq:complement} imply \begin{equation}\label{eq:Tcap} 2T\le\min\{u^2,(2l-u)^2\}+p-2\eta\le l^2+1. \end{equation} This bound also holds in the nondominant case. If~\eqref{eq:internalroute} is not paid, then $K_i-w_i>\delta+\eps$. Equation~\eqref{eq:packetreserve} and integrality give $K_i\ge l+\eps+2$. But~\eqref{eq:localenergy} then implies \[ T\ge(l+\eps+2)^2-2\eps =(l+2)^2+\eps(2l+\eps+2)>(l^2+1)/2, \] a contradiction. Every internal gap is paid. Together with the external case and~\eqref{eq:connected-arcs}, this proves the following. \begin{theorem}\label{thm:connected} Every original lift with connected positive load admits an exact LRX word of length at most $N$ for any two physical cursors. A common finite cut and zero individual windings are not required. \end{theorem} \subsection{Joining components and transferring a word}\label{sec:bridges} Suppose positive load has $\rho\ge2$ components. No cycle has nonzero winding, since it would cover the circle. Cut at a zero edge to get finite invariant intervals. The size of a component counts positions from its first through its last vertex, including any internal fixed positions. Call a component small if its size is at most $\ceil{n/2}$ and large otherwise; at most one component can be large. Choose a packet in each component by Lemma~\ref{lem:source}. If their union has $r$ vertices and $k$ cycles, then $Z_{\mathcal P}\ge k-\rho$, $\delta\ge r/2-\rho$, and $r\ge2\rho$. \subsubsection{Bridges between components} Let $g_1,\ldots,g_\rho\ge1$ be the zero separator widths in edges; their internal vertices are fixed. Leave a widest separator $g_*$ as the window cut and join across the others. Put $B=\sum_jg_j-g_*\le f+\rho-1$. For one join let $u$ be the rightmost vertex of the left component and $v$ the leftmost vertex of the next, with $g=v-u$. Their incoming arrows have origins ordered $at\}$ for $0\le i,t2h$ in $g$. Every pair therefore joins the two arcs between the fixed points; a pair inside one arc would enclose an adjacent leaf. The arcs have equal size and the matching reverses their order. In both cases $\sigma$, and hence $T\bmod n$, is a circular reflection. Writing it as $i\mapsto c-i\pmod n$ shows that its shortest arrows reverse two consecutive arcs of sizes $m,n-m$. Every load component has size at most $\ceil{n/2}$, contrary to the retained original packet of the large component. This proves strictness. \end{proof} \subsubsection{Small invariant blocks} \begin{lemma}\label{lem:smallblocks} If the original map preserves consecutive blocks of size at most $\ceil{n/2}$, it has a word of length at most $N$ for any two cursors. \end{lemma} \begin{proof} First take two invariant blocks of sizes $a,b\ge2$, $a+b=n$. Put $H=\binom a2+\binom b2=N-ab$ and let $I$ be the target inversion count. On vertices $u,\ldots,v$, define a comparison sequence recursively by \[ W[u,v]=(u,u+1,\ldots,v-1)(v-2,v-3,\ldots,u)W[u+1,v-1], \] with $W[u,v]$ empty for $u\ge v$ and empty sweeps omitted. Each entry is an edge at which to compare. The first sweep places the maximum at $v$, the return sweep the minimum at $u$, and recursion sorts the interior. Thus $W$ sorts every list, uses $\binom k2$ comparisons on $k$ vertices, and moves one step between successive comparisons. For example, $W[0,3]=(0,1,2,1,0,1)$. On a reversed list every comparison exchanges, so $W$ is a reduced word for reversal. Its reverse also sorts every list by Lemma~\ref{lem:bruhat}, since reversal is the maximum in the finite Bruhat order \cite[Proposition~2.3.1]{coxeter}. Sort the first block from its middle to the boundary and the second from that boundary to its middle. The extreme internal edges of the blocks are two steps apart, so internal movements total $[\binom a2-1]+2+[\binom b2-1]=H$. The two boundaries and two orders give endpoint pairs $(A_1,B_0),(B_0,A_1),(A_0,B_1),(B_1,A_0)$, where \[ A_0=\floor{(a-2)/2},\ A_1=\floor{(a-1)/2},\quad B_0=a+\floor{(b-2)/2},\ B_1=a+\floor{(b-1)/2}. \] For even $n$, $B_i=A_i+m$, so the mean approach cost over the four pairs is $m$. For odd $n$, one block has a single centre $A$ and the other has centres $A+m,A+m+1$. Then \[ \min_{v\in\{A+m,A+m+1\}}\dist(x,v)=m-\dist(x,A). \] Choosing the order gives cost $m-|\dist(s,A)-\dist(t,A)|\le m$. Exactly $I$ exchanges are made, so the word length is at most $I+H+m$. Now let $L$ be the largest original block size. For $L=1$ the map is the identity. For $2\le L\le m$ take $a=L$, $b=n-L$. Then \[ I\le\sum_j\binom{l_j}2\le n(L-1)/2\le L(n-L)-m, \] since the difference between the last upper bound and its predecessor is $L(n/2-L)+(n/2-m)\ge0$. For $n=2m+1,L=m+1$, we have $I\le m^2$ and $H+m=m^2+m$. In either case $I+H+m\le N$. \end{proof} \subsubsection{Shallow cycles and adjacent ranks}\label{subsec:shallow} A finite permutation is \emph{shallow} if $Z=\Delta-I-\rk=0$ \cite[Definition~2]{berman-tenner}. We use the following literature result: write a shallow cycle starting with its maximum; the remaining word is a separable permutation \cite[Corollary~31]{berman-tenner}. Separable permutations are built by direct and skew sums of singletons: for sizes $u,v$, these are $(\alpha,\beta+u)$ and $(\alpha+v,\beta)$. Reflecting the order gives the corresponding characterization for a cycle starting with its minimum. The sum tree has a node with two singleton children, giving adjacent letters of consecutive ranks. Thus a shallow cycle has an arrow between consecutive vertices of its ordered support. Inserting a fixed position at a cut of half-load $w$ increases both $\Delta$ and $I$ by $2w$ and preserves reflection length; rank compression of the support preserves $Z$. \begin{lemma}\label{lem:unit} A nonempty finite permutation without fixed points or unit arrows has $Z\ge2$. \end{lemma} \begin{proof} Suppose $Z=0$ and choose a nonempty load component. Additivity over components and invariant packet gaps gives zero defect to its packet and every filling. Lemma~\ref{lem:packetdefect} then makes the packet a single shallow cycle. If a gap contains active vertices, descend to a nonempty load component of that filling. Its interval is strictly smaller, so this descent terminates at a shallow cycle with no active filling. There are no fixed points, hence its support fills its interval. The preceding shallow-cycle characterization supplies adjacent ranks, which are now adjacent physical positions: a unit arrow, a contradiction. Nonnegativity and evenness of $Z$ give $Z\ge2$. \end{proof} For a finite component with a packet of $k$ cycles define \begin{equation}\label{eq:componentcredit} c=Z_{\rm component}-k+\eta_{\rm in},\qquad \eta_{\rm in}=\sum_{C\text{ in fillings}}(U_C-1). \end{equation} Always $c\ge-1$; $c<0$ is possible only if $k=1$ and $Z=\eta_{\rm in}=0$. \begin{lemma}\label{lem:rigidity} If a component has no fixed points or unit arrows, then $c\ge0$. Equality requires a packet with $k=Z_{\mathcal P}=2$ and no nonempty internal gaps. If arrows of length two are also absent and some internal gap is nonempty, then $c\ge2$. \end{lemma} \begin{proof} Lemma~\ref{lem:packetdefect} gives $Z_{\mathcal P}\ge2(k-1)$. If $Z_{\mathcal P}=0$, then $k=1$: with no gaps Lemma~\ref{lem:unit} would give a unit arrow, while a nonempty gap has $Z\ge2$, hence $c\ge1$. If $Z_{\mathcal P}>0,k=1$, then $Z_{\mathcal P}-k\ge1$. If $k\ge3$, then $Z_{\mathcal P}-k\ge k-2\ge1$. Only $k=2,Z_{\mathcal P}=2$ remains, and every nonempty gap adds at least two to $c$. This proves the first part. We need one further observation. If every arrow of a finite permutation has length at least three and each cycle has half-peak one, then $Z\ge4$. Take a last packet in the nested decomposition, with empty internal gaps. Its support fills an interval since there are no fixed positions. The arrows of the first three positions are positive and cross the cut after the third position. Its half-load is at least three, so the packet contains at least three cycles. Its defect is at least $2(3-1)=4$. If $Z_{\mathcal P}>0$ and a gap is nonempty, $c\ge2$ follows from $Z_{\mathcal P}-k\ge0$ and $Z_{\rm gap}\ge2$. If $Z_{\mathcal P}=0$ and $c\le1$, then $k=1$, $\sum Z_{\rm gap}=2$, and $\eta_{\rm in}=0$. All filling cycles would have half-peak one, contradicting the preceding observation on a nonempty gap. \end{proof} A cycle of half-peak one is bitonic: its positive arrows form a chain from minimum to maximum, and its negative arrows a chain back. Otherwise some cut would have half-load at least two. Such a cycle is shallow, also seen by successively contracting unit rank arrows in the two chains. A packet with at least two cycles has half-peak at least two: at combined peak one, cycle intervals have disjoint interiors and cannot form a strongly connected component. \subsubsection{Combined filling capacity} For a filling of size $b$ put $\kappa=\binom b2-I+S$, where $S=\sum_C U_C$, and $z=b-2S\ge0$. Its half-load profile is bounded by $\min(j,b-j,S)$, hence $\Delta\le2S(b-S)$. By~\eqref{eq:depth}, \begin{equation}\label{eq:kappa} \kappa\ge\rk+Z+\frac{z(z-1)}2,\qquad b\le2\kappa+f-2Z. \end{equation} Since $\rk\ge S$, we get $\kappa\ge S+\floor{z/2}=\floor{b/2}$. Thus $b\le2\kappa+1$ and $\Delta\le2\kappa(\kappa+1)$. For a family of gaps with $\sum\kappa_i\le T$ and total size $x$, \begin{align}\label{eq:kappasum} x&\le2T+\sum f_i-2\sum Z_i,\nonumber\\ \sum\Delta_i&\le2T(T+1),\nonumber\\ \sum\Delta_i&\le2(T-\sum Z_i)^2\le2T^2\quad\text{if }\sum f_i=0. \end{align} For the first displacement bound sum the individual bounds and use $\sum\kappa_i^2\le T^2$. For the second, use $b_i\le2(\kappa_i-Z_i)$ and $\Delta_i\le b_i^2/2$. \subsection{A large shallow shell}\label{sec:shell} Assume $n\ge11$, the load is finite, and a large component has an outer packet of defect zero. This packet is a single shallow cycle $A$. Let its extreme positions be $0,W$, with $W>h$, and its support size $r=2l+\eta\ge4$. Write $b_i$ for internal gap sizes and $e=n-1-W\ge2$ for the external interval containing another component. Put $s=n-r=\sum b_i+e$. These intervals are invariant and their fillings are arbitrary. Define \begin{gather*} H=l(n-l)-\Delta_A\ge0,\qquad \max\lambda_A=2U,\\ g=(b_1,\ldots,b_{r-1},e),\qquad o=\#\{i:g_i\text{ odd}\},\\ T=2\floor{(s+\eta)^2/4}-\sum_i g_i^2. \end{gather*} The same averaging of zero-winding cycles as in Section~\ref{sec:connected} proves $H\ge0$. \subsubsection{A route through reversed gaps} Reverse each interval $g_i$ and retain $A$, obtaining $\overline F\succeq F$. Exchange adjacent target values $W,W+1$. The outer reversal pair $(W+1,n-1)$ merges with $A$, giving a root spanning the entire finite window. Its peak remains $2U$; the other cycles are nested pairs. The resulting map $G$ satisfies \[ \Delta_G=\Delta_{\overline F}+2,\quad I_G=I_{\overline F}+1, \quad I_{\overline F}+\Delta_{\overline F} =2\Delta_A-r+1+\sum_i\bigl(g_i^2-\ceil{g_i/2}\bigr). \] Here $I_A=\Delta_A-r+1$, and a reversed interval of $b$ positions has $I+\Delta=b^2-\ceil{b/2}$. There remain $j=(s-o)/2-1$ pairs. The two-arc excess for $G$ is $m-U-j-1=\floor{(r+o)/2}-U\ge0$. Internal excesses are no greater: for a reversal,~\eqref{eq:quadratic} gives $K^2\le b\bmod2$, and the root load is at least two. The new bridge is empty; the external gap of a root spanning all $n$ positions has excess zero. Service and Lemma~\ref{lem:bruhat} now give an original word with \begin{equation}\label{eq:shellE} |w|-N\le E:=3-U-2H-p-T. \end{equation} \subsubsection{Two rank adjacencies and controlled contractions} A shallow cycle without an arrow joining its minimum and maximum has arrows across two distinct adjacent-rank gaps. To see this, write the cycle starting at its minimum; its suffix is separable. Reverse the cycle direction if needed to make its top decomposition a direct sum $\alpha\oplus\beta$. The last, upper part $\beta$ has length at least two: otherwise the maximum would be last, giving the prohibited extreme arrow. There is a rank adjacency inside $\beta$. If $|\alpha|\ge2$ there is another inside $\alpha$; if $|\alpha|=1$, the arrow from rank $0$ to rank $1$ supplies the second. Here the extreme arrow is prohibited by $W>h$. Also $r>2U$: if $r=2U$, every arrow would cross a maximum-load cut, whereas at most one adjacent-rank gap straddles that cut. In the following contractions, first replace the ordered support by ranks $0,\ldots,r-1$. Record the original physical arrow before each contraction; its physical length is retained when estimating $S_{\rm sel}$. Contracting a unit rank arrow of a shallow cycle preserves its defect. For an arrow $i\to i+1$, remove the corresponding permutation point and standardize rows and values. If the cut has half-load $w$, then $\Delta$ drops by $2w$, $I$ by $2w-1$, and rank by one. Reflection handles negative arrows. After successive contractions, each vertex represents an interval of original ranks; the selected arrows form a path within it. Arrows between blocks are original arrows with their original signs. Choose positive thresholds $a,z$ for the two signs and stop when either threshold is reached. At most $k\le a+z-1$ arrows have been selected. If the sign with threshold $a$ is reached, let $S_{\rm sel}$ count only the total original physical length of selected arrows of that sign. The sum of their original rank lengths is at most $az$. Indeed a block of $A_i$ ranks, with $a_i$ selected arrows of that sign and $k_i=A_i-1$ selected arrows in all, contributes at most $a_i(A_i-a_i)$, since sources and targets are distinct. Thus \[ \sum_i a_i(A_i-a_i)=a+\sum_i a_i(k_i-a_i) \le a+a(k-a)\le az. \] At most $\min(a,z)$ of the selected arrows cross a given hole: in a block, arrows of that sign form $A_i-a_i$ monotone paths, and $A_i-a_i\le k-a+1\le z$. If the available holes have total length $c$, we obtain the physical length bound \begin{equation}\label{eq:selected} S_{\rm sel}\le az+\min(a,z)c. \end{equation} \subsubsection{A dominant internal gap} Figure~\ref{fig:contraction-blocks} distinguishes the ranks being contracted from the physical gaps whose lengths remain in~\eqref{eq:selected}. \begin{figure}[t] \centering \includegraphics[width=\textwidth]{contraction_blocks_en.pdf} \caption{A local rank contraction merges two consecutive support vertices into an interval block. A gap avoided by all selected arrows remains between blocks.} \label{fig:contraction-blocks} \end{figure} Suppose $b>s/2$, put $c=s-b-e$, and $v=2b-s>0$. Contract only adjacencies avoiding the distinguished gap. After $k\le v-2$ contractions an extreme arrow in the rank cycle would have original physical length at least $r-1-k+b\ge n-b+1>h$, which is impossible. There are therefore two distinct rank adjacencies, at least one avoiding the gap. Since $b+1\le h$, we have $v\le r-3$; before each required selection ($k\le v-2$), the current cycle has at least five vertices. Whenever the stopping thresholds leave $l-j$ original arrows of the attained sign, their original displacement sum and~\eqref{eq:lorenz} give \[ \Delta_A-2S_{\rm sel}\le(l-j)(n-l+j),\qquad H\ge j(s+\eta+j)-2S_{\rm sel}. \] This uses the remaining original arrows, rather than a new majorization claim for the contracted cycle. After reflection if needed, the original sign counts are $l+\eta+d,l-d$, with $d\ge0$. Put $j=\floor{(v-\eta)/2}$. If $j\le d$, the original sign capacity gives $H\ge d(s+\eta)+d^2\ge j(v+2e-\eta-j)$. If $j>d$, use thresholds $j+\eta+d$ and $j-d$. Their sum is $2j+\eta\le v$, so the required contractions are allowed. The sign reaching its threshold has $l-j$ original arrows left. Apply~\eqref{eq:lorenz} to these arrows and then~\eqref{eq:selected}: \begin{align*} H&\ge j(s+\eta+j)-2S_{\rm sel}\\ &\ge j(v+2e-\eta-j)+2d(d+\eta)+2dc. \end{align*} In either case, \begin{equation}\label{eq:shellinternalH} H\ge j(v+2e-\eta-j),\qquad 4H\ge(v-\eta)^2-((v-\eta)\bmod2)+8je. \end{equation} If every $g_i\le s/2$, then $T\ge0$. For $U=1$ the cycle is bitonic, $\Delta_A=2W$, and \[ H=(l-2)^2-2+(l-2)(\eta+\sum b_i)+le\ge2(e-1)\ge2. \] For $U\ge3$,~\eqref{eq:shellE} is also paid. Only $U=2,H=p=T=0$ remains. If $\eta=1$, then $T\ge s\ge2$, a contradiction. If $\eta=0$, equality $T=0$ forces exactly two nonempty intervals of equal size: the external $e$ and one internal gap. Equality $H=0$ forces equal sign counts; removing any one arrow from~\eqref{eq:lorenz} gives $|d_i|\ge e+1$ for every root arrow. But one of the two rank adjacencies crosses an empty gap and is a unit arrow, a contradiction. For an internal $b>s/2$,~\eqref{eq:shellE} gives \begin{equation}\label{eq:shellinternalE} 2E\le6-2U-p-4H+v^2-\eta(2s+1). \end{equation} Substituting~\eqref{eq:shellinternalH}, for $\eta=1$ we get $2E\le4-2U-4(c+e)-8je<0$; for $\eta=0,j\ge1$ we get $2E\le6-2U-8je<0$. If $\eta=0,j=0$, then $v=p=1$ and $2E\le6-2U-4H$. The cases $U\ge3$ and $U=1$ are already paid. For $U=2,H=0$, the original prefix bound requires $|d_i|\ge\ceil{(s+1)/2}>c+1$. Yet a rank adjacency avoiding the dominant gap has length at most $c+1$, again a contradiction. \subsubsection{A dominant external interval} Suppose $e>c:=\sum b_i$, and put $t=e-c\ge1$. Since $W>h$, $t\le r-2-p$. Now contract any unit rank arrow. If the threshold sum is at most $t$, stopping takes at most $t-1\le r-3$ contractions, so unit rank arrows do not run out. Use sign counts $l+\eta+d,l-d$, $d\ge0$, as above. With $j=\floor{(t-\eta)/2}$, the preceding sign argument, applied to all holes of total length $c$, gives the following. When $j>d$, $S_{\rm sel}\le(j+\eta+d)(j-d)+(j-d)c$, so \[ H\ge j(t-\eta-j)+2d(d+\eta)+2dc \ge\floor{(t-\eta)^2/4}. \] When $j\le d$, the sign-capacity bound $H\ge d(s+\eta)+d^2$ is at least the same quantity. Hence \begin{equation}\label{eq:externalH} H\ge\floor{(t-\eta)^2/4}. \end{equation} We have $2E\le6-2U-p-4H+t^2-\eta(2s+1)$. For $\eta=1$ this gives $2E\le4-2U-4c$; for $\eta=0$ it gives $2E\le6-2U$. Only $U=1$, or $\eta=0,U=2$, remains. For $U=1$, $\Delta_A=2(r+c-1)$. If $r=2l$, $l\ge2$, then \[ E\le-2l^2+8l-2-4(l-1)c-2lt+t^2/2-p/2. \] The function $t^2/2-2lt$ decreases on $1\le t\le2l-2$. For $l\ge3$ even its value at $t=1,c=0$ is negative. For $l=2$ only $t=1,2$ occur. At $t=1$, $e\ge2$ implies $c\ge1$; at $t=2$, substitution gives $E\le0$. If $r=2l+1$, $l\ge2$, then \[ E\le3/2-2l^2+6l-(4l-2)c-(2l+1)t+t^2/2-p/2. \] Here $t\le2l-1$. For $l\ge3$ it suffices to take $t=1,c=0$. For $l=2,t=1$ we have $c\ge1$; for $t\ge2$, use $t=2,c=0$. All these values are nonpositive. Finally suppose $r=2l,U=2$. Put $K_*=H-\floor{t^2/4}\ge0$. Exactly, \[ E=1-2K_*-(c^2-\sum b_i^2). \] If $E>0$, then $K_*=0$ and at most one internal gap is nonempty. The root displacement is at most $4(r+c-2)$, hence \[ K_*\ge l^2-8l+8+lt-\floor{t^2/4}+(2l-4)c. \] The expression $lt-\floor{t^2/4}$ strictly increases on $1\le t\le2l-2$. For $l\ge6$, the lower bound is at least $l^2-7l+8\ge2$. For $l=5,t=1$, we need $c\ge1$, giving $K_*\ge4$; for $t\ge2$, $K_*\ge2$. The value $l=2$ is excluded by $r>2U$. For $l=3$, only $(t,c)=(1,1),(1,2),(2,0),(2,1),(3,0)$ remain; for $l=4$, only $(1,1),(2,0)$ remain. At $t=1$ we have $H=0$: the original prefix bound requires $|d_i|\ge c+1>1$, but the single nonempty gap and the two rank adjacencies force a unit arrow. All other cases have $n=8,9,10$, contrary to $n\ge11$. \begin{proposition}\label{prop:shell} For $n\ge11$, a large finite component with a shallow outer packet and arbitrary fillings is paid within length $N$ for every pair of cursors. \end{proposition} \subsection{Exactly two finite components}\label{sec:two} Let $n\ge11$. If both components are small, apply Lemma~\ref{lem:smallblocks}; otherwise there is a unique large component. Proposition~\ref{prop:shell} handles a large packet of defect zero. It remains to consider positive defect of the large packet. Let $g\le g_*$ be the separator widths, $a=g+g_*-2\le f$, and $v\ge2$ the size of the smaller component. For every internal gap of either original packet put $\gamma_i=\binom{b_i}2-I_i$. Retain the large packet, reverse its gaps, and reverse the entire external interval of length $v+a$. Lemma~\ref{lem:invcap} and additivity give \begin{equation}\label{eq:twocap} \delta\ge\sum_i\gamma_i+av+a(a-1)/2+1. \end{equation} To include gaps of the smaller component, use $I_{\rm other}+\sum_{i\text{ other}}\gamma_i\le\binom v2$. The positive-defect large packet has at least four vertices; Lemma~\ref{lem:packetdefect}, including the other component's contribution, gives $\delta\ge2$. For the component contributions~\eqref{eq:componentcredit}, \begin{equation}\label{eq:twocredit} U+c_{\rm big}\ge2,\qquad c_{\rm other}\ge-1. \end{equation} For $k\ge2$ use $Z_{\mathcal P}-k\ge k-2\ge0$ and $U\ge2$. For $k=1$, positive defect is at least two, and the peak is not one, since a cycle of half-peak one is shallow. \subsubsection{All gaps} Lemma~\ref{lem:reserves} gives $\eps\ge f-1$. If $\delta\ge3$, then $\gamma_i\le\delta-1$ and Lemma~\ref{lem:triangle} imply $K_i\le\delta-1$: $K_i\ge\delta$ would give $\delta(\delta-1)\le2(\delta-1)$. Therefore \[ 2g+K_i-w_i\le\delta+2g-3\le\delta+\eps, \] since $2g-2\le a\le f$. If $\delta=2$,~\eqref{eq:twocap} forces $a=0$, so $g=g_*=1$, $\gamma_i\le1$, and $K_i\le2$; the old-gap excess is at most $2\le D$. The unpaid external excess satisfies $E_{\rm ext}\le a+g+1-\delta-\eps$. Using $2g\le a+2$, $v\ge2$, and~\eqref{eq:twocap}, we obtain \[ 2E_{\rm ext}\le2-a^2-2\eps. \] If $(a,\eps)\ne(0,0)$, integrality gives $E_{\rm ext}\le0$. If $a=\eps=0$, then $g=1$ and $E_{\rm ext}\le2-\delta\le0$. A new bridge costs no more than the external arc. \subsubsection{The two-arc peak and the single activity exception} Rewrite~\eqref{eq:Pdef} using component contributions: \begin{equation}\label{eq:twopeak} P=2g-U-c_{\rm big}-c_{\rm other}-A-1\le2g-A-2. \end{equation} The activity bounds give $A\ge2g-2$, except for \begin{equation}\label{eq:twoexception} f=a=2,\quad p=0,\quad\eps=1,\quad g=g_*=2,\quad A=0. \end{equation} Here is the exhaustive check. For $f\ge4$, $\eps\ge f$ and $A\ge f$; for $f\le1$, $g=1$; for $f=3$, $A\ge2$ and $g\le2$. For $f=2,p=1$, the parity of $\eps$ and the activity bounds give $\eps\ge2$. For $f=2,p=0$, only~\eqref{eq:twoexception} remains. In this exceptional tuple there are no fixed positions inside components, and both sign counts are $m-1$: a smaller count at most $m-2$ would give $\Delta\le m^2-4$, whereas $\Delta=m^2-1$. A unit arrow, together with the prefix of the other arrows of that sign, would require $\eps\ge2^2-2=2$. Thus unit arrows are absent. By Lemma~\ref{lem:rigidity}, both component contributions are nonnegative. If $P>0$,~\eqref{eq:twopeak} forces $U=2,c_{\rm big}=c_{\rm other}=0$. The same lemma excludes internal gaps in both components. Their sizes $L_1,L_2$ satisfy $L_1+L_2=2m-2$, and \[ \Delta\le4(L_1-2)+4(L_2-2)=8m-24\ceil{n/2}$ whose packet has positive defect. Let the other $t=\rho-1\ge2$ components have sizes $l_j\ge2$, put $v=\sum_j l_j$, and let $a$ count fixed positions outside all components. Then \begin{equation}\label{eq:manygeom} L=2m+p-a-v,\quad v+a\le m-1,\quad B\le a+t-\ind{a>0}. \end{equation} The last bound follows from $\sum g_j=a+t+1$ and $g_*\ge1+\ind{a>0}$. \subsubsection{Inversion reserve between outside components} Retain the large packet, reverse its internal gaps, and reverse the entire external interval of size $v+a$. The strict part of Lemma~\ref{lem:invcap} gives \begin{align}\label{eq:crossreserve} \delta&\ge\sum_{\rm all}\gamma_i+M_{\rm actual}+1, &M_{\rm actual}&=\binom{v+a}2-\sum_j\binom{l_j}2\ge M,\nonumber\\ M&=2(t-1)(v-t)+av+a(a-1)/2. \end{align} The sum includes internal gaps of all packets. Reversing gaps inside an outside interval cannot exceed its full capacity $\binom{l_j}2$. For the last inequality write $l_j=2+x_j$, $x_j\ge0$; the discarded remainder is $\sum_{ih$, while two nontrivial cycles require at least four vertices. Take all nonempty internal gaps of the large packet and all $t$ outside components. Denote their lengths by $s_i$, including singleton gaps, and put \[ r=R_0+a,\quad V=\sum_i s_i=n-r,\quad S_2=\sum_i s_i^2,\quad H_0=V^2-2S_2. \] Each length is at most $m-1$, $V\le2(m-1)$, and at least $t$ lengths are at least two. The bound on $V$ follows from $R_0\ge4$. For a finite interval of size $s_i$ with $f_i$ fixed points, $2\Delta_i\le s_i^2-f_i^2$: the smaller sign count is at most $(s_i-f_i)/2$. Remove the arrows of all these intervals from the original sign prefixes. If $y_+,y_-$ are $m$ minus the remaining sign counts, then \[ \eps+\Delta_{\rm intervals}\ge y_\pm(y_\pm+p),\qquad y_++y_-=V+a-p. \] Adding and completing the square gives $4\eps+p\ge(V+a)^2-4\Delta_{\rm intervals}$, whence \begin{equation}\label{eq:density} 2A\ge H_0+2(V-1)a+a^2+2\sum_i f_i(f_i-1)+p \ge H_0+2(V-1)a+a^2+p. \end{equation} The discarded sum is nonnegative since every $f_i$ is an integer. The large packet's half-profile is bounded by $\min(j,L-j,U)$. Even if the maximum $U$ occurs in another component, $2U\le L$, since that component is smaller. Thus \begin{equation}\label{eq:area} \Delta_{\rm core}\le2U(L-U),\qquad 2(Q-\eps)\le4U(L-U)+S_2. \end{equation} Each outside component has an arrow of each sign of length at most $l_j-1$. Removing one of each, with $x=m-\min(k_+,k_-)\ge0$, gives \[ \eps\ge(x+t)(x+t+p)-2(v-t),\qquad f\le2x+p. \] Since $t\ge2$, the expression $x^2+px+(2t-4)x+p(t-2)$ is nonnegative. Therefore \begin{equation}\label{eq:shortexternal} \eps\ge2f+t^2-2(v-t). \end{equation} \subsubsection{Absolute bounds for an unpaid case} Suppose $P\ge1$. From~\eqref{eq:Pbounds}, the activity bounds, and~\eqref{eq:shortexternal}, we obtain \begin{align}\label{eq:absolutebounds} 2\eps+p&\le3f+3t-2,&(f-3)^2&\le6t+5-p,\nonumber\\ f&\le t+5,&\eps&\le3t+6,& U&\le3t+1,\nonumber\\ 4v&\ge2t^2+t+2. \end{align} The first row follows from $A\le2a+3t-2\le2f+3t-2$ and $f^2\le4\eps+p$. If $f\ge t+6$, the square bound contradicts $(t+3)^2>6t+5$. The bound on $\eps$ follows. If $a=0$, $U\le3t-1$. If $a>0$, then $U\le3f+3t-3-2\eps-p$, so $2U\le6t+3-(f-3)^2-p\le6t+3$. The last row compares the upper and lower bounds on $2\eps$. For $t\ge3$, integrality gives $2v\ge t^2+3$. The second bound in~\eqref{eq:Pbounds} and~\eqref{eq:manygeom} give $m\ge2(t-1)v-2t^2+4$. Hence \begin{equation}\label{eq:cubic} m\ge t^3-3t^2+3t+1\quad(t\ge3). \end{equation} Since $V\ge2t\ge4$,~\eqref{eq:density} and $A\le2a+3t-2$ give $H_0\le6t-3$. Either $m\le42t+23$, or $m\ge42t+24\ge12U+2\eps$. In the latter case, $S_2\le(m-1)V$ and~\eqref{eq:area} imply \begin{equation}\label{eq:rbound} r\le8U-2-p\le24t+6-p. \end{equation} Here is the algebra. Weaken $L\le n$ in the area bound to get \[ (m-1)(r-(8U-2-p))+4U^2-8U-4Up+2+2p-2\eps\le0. \] If $r\ge8U-1-p$, the left side is at least $m+4U^2-8U-4Up+1+2p-2\eps>0$, since $m\ge12U+2\eps$. This proves~\eqref{eq:rbound}. \begin{lemma}[Square envelope]\label{lem:squareenvelope} Suppose the lengths sum to $V\le2M_0$, their maximum is $x\le M_0$, and $S_2\le x^2+(V-x-w)^2+w^2$ for $w\ge0$. Then \begin{equation}\label{eq:squareenvelope} S_2\le M_0^2+(V-M_0-w)^2+w^2,\qquad H_0\ge4M_0w-(2M_0-V+2w)^2. \end{equation} \end{lemma} \begin{proof} If $x\ge V-M_0-w$, use convexity of $z^2+(V-z-w)^2+w^2$ on $[V-M_0-w,M_0]$. Its endpoint values coincide, so its value at $x$ is at most that value. If $x0$. In the small branch $m\le42t+23$, the contradiction is $t^3-3t^2-39t-22>0$ for $t\ge13$; after $t=13+z$, all coefficients are positive. For $t=3,\ldots,12$, the maxima of the small bound and~\eqref{eq:largecutoff} are, respectively, $802,731,772,842,923,1010,1100,1192,1285,1379$. Thus \begin{equation}\label{eq:finitebox} P\ge1\quad\Longrightarrow\quad 2\le t\le12,\quad m\le1379, \quad n\le2759. \end{equation} This analytic cutoff is proved before any computation is used. \section{The complete finite certificate}\label{sec:certificate} Appendix~\ref{app:code} contains the full program. We now justify its ranges and each kind of rejection. The code first enumerates necessary integer parameters, then the small actual outside components. \subsection{Scalar parameters and necessary filters} The code accepts a threshold $k=1$ or $k=2$; the proof uses $k=1$. If $P\ge k$, replace the actual $B$ by its upper bound: every estimate used below is thereby weakened. Put \begin{align*} B&=a+t-\ind{a>0},& M&=2(t-1)(v-t)+av+a(a-1)/2,\\ L&=2m+p-a-v,&x&=L-R_0,&h_0&=m+p-2,\\ T&=2B+m-U-2-M-\eps-k,& E_2&=(v-2t+2)^2+4(t-1). \end{align*} Equation~\eqref{eq:crossreserve} and the definition of $P$ give $\sum_{\rm all}\kappa_i\le T$, in particular $T\ge0$. Here $\kappa_i=\gamma_i+S_i$ ranges over internal gaps of all packets. Besides~\eqref{eq:absolutebounds}--\eqref{eq:finitebox}, we need even $Q-\eps$, $x\le2T+f-a$, and \begin{align}\label{eq:filters} \sum_{\rm big}b_i^2&\le\min\{J(x),4T^2+2T+x\},\nonumber\\ 2\Delta_{\rm external}&\le E_2-(v\bmod2),\nonumber\\ 2\Delta_{\rm big\ fill}&\le4T\bigl(T+\ind{f>a}\bigr),\nonumber\\ (x+v+a)^2&\le4\eps+p+4(\Delta_{\rm external}+\Delta_{\rm big\ fill}), \end{align} where $J(x)=x^2$ for $0\le x\le h_0$, and $J(x)=h_0^2+(x-h_0)^2$ for $h_0\le x<2h_0$. Indeed $x\le L-4<2h_0$. Concentrating lengths subject to $b_i\le h_0$ gives $J$. Since $\floor{b_i/2}\le\kappa_i$, we have $b_i^2\le4\kappa_i^2+2\kappa_i+b_i$; summation gives the other square bound. Outside lengths are at least two, hence $\sum l_j^2\le E_2$ and $2\Delta_{\rm external}\le E_2-(v\bmod2)$. The remaining estimates are~\eqref{eq:kappasum} and the original sign prefixes used to derive~\eqref{eq:density}. The program loops over the following ranges: \[ \begin{gathered} 2\le t\le12,\quad p\in\{0,1\},\quad0\le f\le t+5, \quad0\le\eps\le3t+6,\\ 0\le a\le f,\quad1\le U\le3t+1,\quad 2t+a+1\le m\le1379,\quad2t\le v\le m-a-1, \quad0\le x\le L-4. \end{gathered} \] For $t\ge3$,~\eqref{eq:cubic} strengthens the lower bound on $m$. Equation~\eqref{eq:shortexternal} strengthens the lower bound on $v$, and $T\ge0$ its upper bound. Exact square-root bounds accelerate the loop over $x$ while preserving all admissible rows. If \begin{gather*} B_0=4T^2+2T,\qquad E_0=E_2-(v\bmod2),\\ E_1=4T(T+\ind{f>a}),\qquad W=2(Q-\eps)-4U(L-U), \end{gather*} then necessarily \begin{align*} J(x)+E_2&\ge W,&x+B_0+E_2&\ge W,\\ (x+v+a-1)^2+2v-1+p-2(B_0+E_2)&\le2A,\\ (x+v+a)^2&\le4\eps+p+2E_1+2E_0. \end{align*} These follow directly from~\eqref{eq:area},~\eqref{eq:density}, and~\eqref{eq:filters}, and give the integer square roots in the code. The square argument is nonnegative on each branch of $J$; every remaining $x$ is tested against the full density bound~\eqref{eq:density}. Duplicate rows from the two branches are removed by a set. \subsection{All outside permutations and the sign tests} For each scalar row the program checks $v-2(t-1)\le5$. This is an outcome of the complete scalar enumeration, not an imposed restriction. Thus every outside component has size two through five. The function \texttt{make\_catalogue} enumerates all permutations of those sizes and retains exactly those with connected load. The function \texttt{describe} computes cycles, passages, the root packet, and its load independently from the permutation. For an outside family compute $I_e,\Delta_e,S_e,c_e,f_e$. Here $S_e$ includes only fillings of outside packets, and $c_e$ sums the component contributions~\eqref{eq:componentcredit}. Put $f_b=f-a-f_e$, the number of fixed points in the large component. The exact form of~\eqref{eq:Pdef} and strict inversion capacity require \begin{align}\label{eq:exactrefine} c_{\rm big}&\le2B-U-c_e-A-1-k,\nonumber\\ \sum_{\rm big}\kappa_i&\le2B+m-U-2-\eps-k -\bigl[\binom{v+a}2-I_e\bigr]-S_e. \end{align} Filling length, displacement, and density are tested again using these exact outside quantities. The restriction $R_0\ge2U$ is used only when no outside packet attains $U$. Rounding the displacement capacity down to $2\floor{S_2/4}$ is valid: finite displacement is even and at most $S_2/2$. For a sign $s$, put $x_s=m-k_s$, where $k_s$ counts its arrows. Then $x_++x_-=f-p$. If $r$ arrows of that sign have been selected, with total absolute length $b$, majorization of the remaining arrows gives \begin{equation}\label{eq:tailsigns} \eps\ge(x_s+r)(x_s+r+p)-2b. \end{equation} The function \texttt{signs\_ok} tests every prefix of the sorted absolute outside arrow lengths and every possible $x_s$. The inequality $x_s(x_s+p)\le\eps$ implies $-\eps-2\le x_s\le\eps+2$, so the range is exhaustive. Adding a hypothetical arrow of length one or two tests whether such an arrow can occur in the large component. If both signs fail, that length is excluded. After these necessary tests, the code uses only the two parts of Lemma~\ref{lem:rigidity} and the explicit route below: \begin{center} \begin{tabular}{@{}p{.21\textwidth}p{.74\textwidth}@{}}\toprule Branch & Mathematical basis\\\midrule \texttt{creditCuts} & $f_b=0$, no unit arrows: $c\ge0$; $c=0$ requires $x=0$.\\ \texttt{bitonicCuts} & No lengths $0,1,2$, $x>0$: $c\ge2$.\\ \texttt{tourCuts} & The direct three-port route below.\\ \bottomrule\end{tabular} \end{center} Thus every rejection has a necessary mathematical justification. No independent global majorization is assumed for the outside maps. \subsection{Enumeration output and the remaining routes} For $k=1$ there are 757 distinct scalar rows and 13\,009 outside families. The geometric and sign tests retain 691 families. The first part of Lemma~\ref{lem:rigidity} rejects 682, and its second part rejects seven. The two remaining rows have \[ n\in\{16,20\},\quad p=f=\eps=a=0,\quad U=4, \quad x=0,\quad c_{\rm big}=0, \] with two adjacent unit pairs outside. By rigidity the large packet has $k=Z=2$ and no gaps. Altogether $q=4$, $Z=2$, and $A=0$, so $D=m-2$. Since $a=0$, place the two outside pairs at positions $0,\ldots,3$; their ports are $0,2$. Serving the large root at a peak port costs $\Delta_{\rm core}-8$ rotations, while each pair needs zero internal rotations. For $n=16,20$, \texttt{three\_port\_max} checks every position of the third port and both cursors. For each of the six orders of the three ports, it adds shortest circular distances. The maximum over cursor and port positions of the minimum of these six lengths is $n$. These are explicit admissible walks; they need not be optimal among all walks. After redundant $X$ letters are deleted, \[ |w|\le C+\Delta-12+n =N-(m-2)-12+2m=N+m-10\le N. \] The number of untreated rows, \texttt{survivors}, is zero. Together with the already paid gaps, this completes $\rho\ge3$. \subsection{Reproducibility and exact arithmetic} The program uses the C++17 standard library and signed 64-bit integers. Assertions must remain enabled. In the proved ranges, square-root radicands are less than $3\cdot10^7$; even the square of an intermediate binary-search value is less than $9\cdot10^{14}<2^{63}$. All other products have absolute value below $10^{16}$. If the numerator of the upper bound on $v$ is negative, there is no admissible positive $v$, so that pass is empty. For small sizes, BFS enumerates all $n!$ permutations for $4\le n\le10$ using bijective Lehmer ranks, checking all three outgoing edges. It asserts that exactly $n!$ states were reached. The diameters are \begin{center} \begin{tabular}{@{}rrrrrrrr@{}}\toprule $n$ &4&5&6&7&8&9&10\\\midrule $D_n$ &6&10&15&21&28&36&45\\\bottomrule \end{tabular} \end{center} This checks ordinary permutations; it makes no bound assertion for an arbitrarily prescribed affine lift at small $n$. \section{Completion of the proof and reproduction}\label{sec:finish}\label{sec:computer} \begin{proof}[Proof of Theorem~\ref{thm:main}] BFS covers $4\le n\le10$. Let $n\ge11$ and choose an arbitrary target list. Choose the lift and final phase $c$ as in Section~\ref{sec:lift}. They satisfy the original constraints~\eqref{eq:lorenz}. If the load is connected, apply Theorem~\ref{thm:connected}. Otherwise a zero edge gives a common finite window. Lemma~\ref{lem:smallblocks} covers small components; Proposition~\ref{prop:shell} covers a large shallow component; Section~\ref{sec:two} covers two components; and Sections~\ref{sec:many}--\ref{sec:certificate} cover all remaining cases. A zero lift needs only a shortest rotation, at most $m\le N$ letters. Every construction for $n\ge11$ allows arbitrary initial and final physical cursors. Take them to be $0$ and the chosen $c$. Token $i$ ends at physical position $p_i+c$, so reading from cursor $c$ gives exactly the target list, without an extra rotation. Thus $D_n\le N$. Theorem~\ref{thm:lower} gives the reverse inequality. The sizes $n=1,2,3$ are checked directly. \end{proof} To reproduce the finite part, save the complete C++17 program from Appendix~\ref{app:code} as \texttt{upper\_bound.cpp}, then run: \begin{Verbatim}[fontsize=\small,breaklines=true] c++ -O3 -std=c++17 upper_bound.cpp -o /tmp/lrx-certificate /tmp/lrx-certificate 1 \end{Verbatim} Assertions must remain enabled: do not use \texttt{-DNDEBUG}. Compare the output with the complete reference output printed after the program in Appendix~\ref{app:code}. The final refinement check must report \texttt{survivors=0}. \section{Formalization} We have also formalized the proof of the main result in Lean 4. It is available at the repository~\cite{lrxformalization} and was created with the help of our agentic system discussed in the Introduction.