Proof. Prefixing a symbol selects the interval \((d+[0,1])/B\). These intervals lie in \([0,1]\), and two of them have a gap at least \(B^{-1}\). Further prefixing selects nested affine copies. At the first difference in position \(j\), the gap is at least \(B^{-j}\), which proves both interval separation and injectivity. The series identity follows by splitting its first \(|v|\) terms. Two product cylinders with the same state are disjoint precisely when the prefixes on at least one stack are incompatible: otherwise their compatible prefixes have common infinite extensions. This proves rectangle separation. Finally the affine map preserves each normalized tail coordinate \(E(L_*),E(R_*)\), which proves its action on codes. Codes of \(v\square^\infty\) are rational, equal to \(E(v)+B^{-|v|}d(\square)/(B-1)\). Digit gaps allow recovery of every finite prefix to sufficiently high finite precision, including zero-digit boundary codes. ◻

Proof. Differentiating \(\det D=1\) gives \(\operatorname{tr}A=0\). With \(Y=x-c\), \[\nabla\times(\dot c\times Y)=2\dot c,\qquad \nabla\times((AY)\times Y)=3AY.\] The second identity follows by expanding the curl and using \(\operatorname{div}(AY)=0\). Thus on the plateau \(V=\dot c+AY\), and (4) solves its ODE. If \(M\ge1\) bounds \(\|D\|\) and the collar width is \(\eta\), an initial perturbation smaller than \(\eta/(2M)\) remains on that plateau. For a finite sequence, decrease this radius by the product of the preceding affine norms. Smooth ODE uniqueness proves the assertion, and disjoint supports prevent interference. ◻

Proof. For \(N=0\) take zero. Write \(p_i,q_i\) for the centers and \(w_i^0,w_i^1\) for side-length vectors. In three successive stages, lift to \(z_i=1/2+i/[4(N+1)]\), transform there, and lower to \(z_0\). During the middle stage, with a flat progress parameter \(s\in[0,1]\), put \[p_i(s)=(1-s)p_i+sq_i,\quad w_i(s)=(1-s)w_i^0+sw_i^1,\] \[D_i(s)=\operatorname{diag}\left(\frac{w_{i1}(s)}{w_{i1}^0}, \frac{w_{i2}(s)}{w_{i2}^0}, \frac{w_{i1}^0w_{i2}^0}{w_{i1}(s)w_{i2}(s)}\right).\] All scales are positive and their product is one. Give the sheets a sufficiently small rational thickness. The reciprocal scale is bounded by \(\max_i[\min(1,w_{i1}^1/w_{i1}^0) \min(1,w_{i2}^1/w_{i2}^0)]^{-1}\), so an effective positive thickness keeps the middle-stage boxes apart vertically. During lifting use the source separation, and during lowering the target separation. Choose a rational collar smaller than a quarter of the corresponding coordinate gaps and boundary clearances. Lemma 7 now supplies the three local motions on disjoint supports, including a positive initial neighborhood. A sheet point has zero normal displacement relative to its center. Its fixed fractional coordinate in the interpolated interval gives \((1-s)x_a+sF_i(x)_a\) in each horizontal direction. Flat stage collars finish the construction. The larger-region version uses exactly the same finite clearance argument. ◻

Proof. The compactly supported field satisfies the whole-space velocity class \(C_tH^2\cap C_t^1L^2\) and has bounded velocity and gradient; zero pressure satisfies \(C_tH^1\). Thus Lemma [lem:p2-realization] applies in either domain. Derivatives of (5) are finite sums of products of derivatives of \(U\), proving the stated bounds and support. For mean zero use \((U\cdot\nabla)U=\operatorname{div}(U\otimes U)\) and integrate. The effective cutoff formulas and differentiation give the force program. Periodic evaluation uses a finite superset of potentially active translates, including adjoining intervals at a seam. ◻

Proof. At a main control, erasing records makes \(R\) the head-and-right tape and \(L\) the reversed left tape. The first row writes \(b\) and saves the lost information in \(g\). A stay is complete. For a right move, \(b\) has been put on \(L\) and \(C_+\) transfers the intervening records until the next work symbol is exposed. For a left move, \(C_-\) transfers the intervening records from \(L\) and finally its first work symbol; that symbol becomes the new head immediately before \(b\) after erasure. At finite rule time there are finitely many records and infinitely many work cells in each direction, so every scan finishes. Writes preserve the origin bit.

The complete rule list is \[ \begin{aligned} (M(q,h);\epsilon,a)&\to \begin{cases} (M(q',0);g,b),&d=0,\\ (C_+(q');bg,\epsilon),&d=+,\\ (C_-(q');\epsilon,bg),&d=-, \end{cases}\quad g=g_{q,h,a},\\ (C_+(q);\epsilon,g)&\to(C_+(q);g,\epsilon),&g\in G,\\ (C_+(q);\epsilon,c)&\to(M(q,+);\epsilon,c),&c\in A,\\ (C_-(q);g,\epsilon)&\to(C_-(q);\epsilon,g),&g\in G,\\ (C_-(q);c,\epsilon)&\to(M(q,-);\epsilon,c),&c\in A. \end{aligned} \tag{6}\] No rule leaves a main control with \(q\in H\).

Source separation uses the tested top symbol on \(R\) for main and \(C_+\) controls, and on \(L\) for \(C_-\). Into \(C_+\) the left prefix starts with a work symbol in a main entry and a record in a loop; the record names separate the main entries. Into \(C_-\) the same distinction is on \(R\). Into \(M(q,0)\) the first left record identifies the incoming instruction; into \(M(q,+)\) or \(M(q,-)\) the first right work symbol identifies the exit. Thus every image has a unique inverse on its full cylinder. The simulation invariant proves the halt equivalence, including an initial halt. ◻

Proof. For \(K=|A\sqcup G|\), use digits \(1,3,\ldots,2K-1\) and base \(B=2K+2\). Enumerate all \(m\) controls by \(i=1,\ldots,m\), put \(\ell=1/[16(m+1)]\), and use the code \[(\beta_i+\ell E(L),1/4+\ell E(R),1/4),\qquad \beta_i=2i\ell+\begin{cases}5/8,&\text{halting},\\1/4,&\text{otherwise}. \end{cases}\] Nonhalt intervals lie in \((1/4,3/8)\) and halt intervals in \((5/8,3/4)\). All prefixes in (6) have length at most two; Lemma 6 therefore gives source and target gaps at least \(\ell/B^2\). Let \(N\) be the number of rules. Apply Lemma 8, with collar at most \(\min(\ell/(4B^2),1/[16(N+1)],1/16)\), to their full closed rectangles. Its normal scale compensates the unequal total prefix lengths. The initial code is rational. A localized curl translation of radius \(1/32\) loads it along the segment from the fixed label during \([0,1]\). Repeat the unit rule pulse thereafter. All pulses have zero collars inside the cube and are curls, giving a smooth mean-zero velocity \(U\) with \(U(0)=0\). Lemma 9 supplies the force.

At time \(1+k\) induction gives the code after \(k\) rules until the first halt. A halt is in the observed arc, including at \(t=1\) if initial. For a nonhalting run the loader stays below \(1/2\), and every subsequent horizontal coordinate is constant during vertical motion and between its two nonhalt endpoints during the middle stage. Thus the observer is avoided at every time. At rule time \(k\) the raw stacks are blank beyond \(\max(1,|w|)+2k\) symbols, so this code retains the whole configuration, not merely the event bit. ◻

Proof. Take odd digits and base \(B=2|\Sigma\sqcup\mathcal G|+1\), where \(\mathcal G\) is the record alphabet. Put \(l_0=E(\square^\infty)\) and \(r_0=E(w\square^\infty)\). Give \(C(q_0,*)\) offset zero, other nontrigger controls distinct offsets \(-4,-8,\ldots\), and trigger controls \(C(q,d)\) with \(q\) halting and \(d\in D\) offsets \(4,8,\ldots\). Encode by \[ (o_s-l_0+E(L),-r_0+E(R),0). \tag{9}\] The initial code is exactly zero. For every rule use its two prefix rectangles, with scales \(\lambda_1=B^{|v|-|v'|}\), \(\lambda_2=B^{|w|-|w'|}\) and \(\lambda_3=(\lambda_1\lambda_2)^{-1}\). Lemma 11 acts on the entire box \(R^-\times[-1,1]\), sending it to \(R^+\times[-\lambda_3,\lambda_3]\). The encoded central sheet returns to the same plane \(z=0\) on successive periods; the full box thickness generally changes. One may take margin \(B^{-m_*}/10\), where \(m_*\) is the maximum prefix length, and heights \(4(Z+1)i\) as in that lemma. Periodize the resulting pulse from time zero; the time collars give \(U(0)=0\). Lemma 9 and its pointwise \(H^1\) pressure refinement give the equation and uniqueness.

The code induction now begins at \(t=0\). A reached halt has a trigger code with first coordinate at least \(4-l_0>2\). An initial halt reaches one after its first idle instruction, changing tag \(*\) to \(0\). For a nonhalting run, every used source and target has first-coordinate center at most \(1\) and half-width at most \(1/2\). The exponential box path has convexly interpolated centers and half-width at most the larger endpoint half-width; hence it stays below \(3/2<2\) throughout. Input shifts affect the finite spatial prescription, and no loader is required. ◻

Proof. For \(R=aR_*\) the first rule gives the updated pair \[(L',R')=\begin{cases} (bL,R_*),&d=+,\\ (L,bR_*),&d=0,\\ (L_*,cbR_*),&d=-,\ L=cL_*,\\ (\epsilon,\square bR_*),&d=-,\ L=\epsilon. \end{cases}\] It also places \(\star\) before \(R'\). The \(D_i\) scan transfers \(|L'|\) work symbols until \(\#\) is exposed, inserts \(h_i\) below it, and enters \(U_{q^+(i)}\). Exactly \(|L'|\) reverse transfers restore \(L'\), and the marker-removal rule finishes the step. This proves the count and tape invariant, including the new blank at the left boundary. Record displacements recover the absolute head position.

The complete rules are \[ \begin{aligned} (N_q;\epsilon,a)&\to(D_i;b,\star),&&d=+,\\ (N_q;\epsilon,a)&\to(D_i;\epsilon,\star b),&&d=0,\\ (N_q;c,a)&\to(D_i;\epsilon,\star cb),&&d=-,\ c\in\Gamma,\\ (N_q;\#,a)&\to(D_i;\#,\star\square b),&&d=-,\ c=\#,\\ (D_i;c,\epsilon)&\to(D_i;\epsilon,c),&&c\in\Gamma,\\ (D_i;\#,\epsilon)&\to(U_{q^+(i)};\#h_i,\epsilon),\\ (U_q;\epsilon,c)&\to(U_q;c,\epsilon),&&c\in\Gamma,\\ (U_q;\epsilon,\star)&\to(N_q;\epsilon,\epsilon). \end{aligned} \tag{11}\] No normal rule leaves \(N_{q_h}\).

The tested top symbols separate sources, with an extra left-top test for left moves. Into \(D_i\) a normal entry starts with \(\star\) on the right and a loop with an ordinary letter. Into \(U_q\) a history entry starts with \(\#h_i\) on the left and a loop with an ordinary letter. Distinct records identify distinct entries. Into \(N_q\) there is just its marker-removal rule. These are inverse checks for arbitrary tails, so induction gives all assertions including initial halting. ◻

Proof. The third processor. For a branch \(i\) of (11), replace its normal rule by a rule that performs the same tape update but enters a fresh state \(B_i\) without pushing \(\star\), followed by \((B_i;\epsilon,\epsilon)\to(D_i;\epsilon,\star)\). Use exactly the other rows of that table. Every \(B_i\) has one incoming and one outgoing rule. Into \(D_i\) its new entry has right top \(\star\), whereas loop entries have ordinary right top, so the previous full-cylinder inverse proof remains valid. On every full source cylinder, the composite of the two new rules equals the old normal rule. This proves the exact relationship, and the machine-step count is now \(2|L'|+4\).

Codes and placement. Use odd digits and base \(B=2m+1\), where \(m\) is the relevant full alphabet size. Apply Lemma 6 in the following state rectangles. For the first row take the halt square \([7/10,4/5]^2\). For the \(M\) other controls take centers \((1/8+(2j+1)/(8M),1/4)\), \(0\le j<M\), and half-side \(1/(16M)\). For the second row take the halt rectangle \([3/4,7/8]\times[1/4,1/2]\) and other rectangles \[[1/8+j/(4M),1/8+j/(4M)+1/(8M)]\times[1/4,1/2].\] For the third row give the halt control the square centered at \((7/8,1/2)\) of side \(1/16\), and the other \(M\) controls squares centered at \((i/[2(M+1)],1/2)\), \(1\le i\le M\), of side \(1/[8(M+1)]\). The first two nonhalt families lie in \((0,1/2)^2\), respectively \((0,1/2)\times(0,1)\); the third lies in the latter open rectangle. In each case the full source and target rectangle families are separately separated by the proved cylinder checks and digit gaps.

Routing and loading. Apply Lemma 13 in \((0,1)^2\), using the corresponding nonhalt open rectangle as the safe region. This proves exact maps on full rectangles and all-time confinement whenever both endpoints are nonhalting. Both its exponential-width and linear-width implementations are available. The second row also permits the following explicit linear-width choice: park strictly to the left of all endpoint centers and choose every bend to the left of both endpoints, off the finite forbidden lines. Nonhalt centers then remain below \(3/8\); small squares of half-side below \(1/8\) stay below \(1/2\). This gives the same endpoint maps with a directly checked closed-rectangle plateau. For the third row one may choose rational bends on \((\lambda s,s^2)\), \(\lambda=1/2\) or \(1\). After clearing denominators, forbidden lines give nonzero integer polynomials of degree at most two. A rational \(s=1/D\) with \(D\) larger than all absolute leading coefficients cannot be a root by the rational-root theorem. Avoid the finite endpoint denominators as well and take \(D\) large enough for the prescribed open rectangle. This is an effective form of the parking choice, with no generic-position assumption.

All initial codes are rational. In the first row a planar compact translation, with plateau half-side \(1/100\) and support half-side \(2/100\), loads from \((1/2,1/2)\). In the second row the spatially constant planar velocity \(\dot\theta(t)r_{\rm in}\) loads from the origin. In the third row a small compact translation tube loads from \((1/4,1/4)\). The loader paths avoid the respective observers when the initial state is nonhalting. Follow the loader by the repeated unit pulse and apply Lemma 14 with \(h=\sin(2\pi z)/(2\pi)\). The three velocities are mean zero, smooth at all joins, and zero initially; Lemma 9 supplies their forces.

At time \(1+k\) the particle is the code after \(k\) primitive rules until halting. A halt code lies strictly in the corresponding observed set, including an initial halt at time one. For nonhalting runs, the loader and every subsequent controlled path avoid that set by the established safe-region bounds. This proves the continuous-time equivalences and all three force contracts. ◻

Proof. Every \(F_j\) has a unique primary entry with right top \(\diamond\); its loops have ordinary right tops. Entries into \(G_q\) have distinct left prefixes \(\sharp h_j\), or ordinary left tops for loops. Each main state has its unique exit from \(G_q\). Source separation is by the same tested top symbols as in Lemma 15, with the single additional source state \(S\). These checks prove the full-domain claim. At main states the stacks are \((L\sharp H\square^\infty,R)\). The primary update gives \((L'\sharp H\square^\infty,\diamond R')\); the two scans transfer and restore \(L'\), insert \(h_j\), and delete the marker. Their count and interpretation are those proved for the delimiter table. Initialization is its case \(L'=\epsilon\), \(R'=w\square^\infty\) and takes three rules. The history records include the zero-displacement initialization and recover the absolute head. ◻

Proof. For \(m\) letters use digits \(2,4,\ldots,2m\) and base \(K=2m+2\). Set \(a_S=-E(\sharp\square^\infty)\), give halt main states distinct offsets \(4,8,\ldots\), and other states offsets \(-4,-8,\ldots\). With \(b_0=-E(\square^\infty)\), encode by \((a_s+E(L),b_0+E(R),0)\), so the fixed initial code is zero. Lemma 6 gives separated source and target rectangles. Thicken to \(R_i^-\times[-1,1]\) and apply Lemma 11 with scales \(K^{|v|-|v'|},K^{|w|-|w'|}\) and their reciprocal product. For example take the three switches \(\sigma(8t-(2j-1))\), \(j=1,2,3\), and collar one quarter of the minimum of \(1\) and the rectangle gaps. The field is zero for \(t\le1/8\) and \(t\ge6/8\) within a period. Its periodization is smooth from zero, so Lemma 9 applies.

Induction at integer times follows the initialized rule sequence. A halt code has first coordinate at least \(4\). Every nonhalting used branch has endpoint centers at most \(1\) and widths at most \(1\); the exponential-width bound gives first coordinate at most \(3/2\) throughout. The force therefore has the required all-time event. The complete input-insertion branch is included in every period, and its actual one-time use follows from the symbolic dynamics. ◻

Proof. Let \(K\) be the number of controls, \(\eta=1/(16K)\), and use odd digits with base \(B=2|\Gamma_{\rm full}|+1\). Give nonhalt controls offsets \(a_{s_j}=1/4+2j\eta\) and set \(a_{A_h}=5/8\). The code is \[(a_s+\eta E(L),1/4+\eta E(R),1/4).\] All nonhalt state intervals are in \([1/4,3/8)\), while the halt interval lies in \((1/2,3/4)\). Lemma 6 gives separately separated rectangles \(E_i^0,E_i^1\subset[1/4,3/4]^2\) and scale factors \(\alpha_i=B^{|v_i^0|-|v_i^1|}\), \(\beta_i=B^{|w_i^0|-|w_i^1|}\). Write \(F_i\) for the positive diagonal affine map \(E_i^0\to E_i^1\). Here is an explicit thin-box instance of normal compensation. If there are \(m\) rules, put \[Z_i=\tfrac12+\frac{i}{4(m+1)},\quad M=\max_i\max(1,1/\alpha_i)\max(1,1/\beta_i),\quad \delta_z=\frac1{64(m+1)M},\] \[\mu=\min\{d_*/4,1/[64(m+1)]\},\] where \(d_*\) is the minimum of \(1\) and the within-family planar sup-norm distances. Lift the boxes \(E_i^0\times[1/4-\delta_z,1/4+\delta_z]\) to \(Z_i\), use the horizontal scales \(1-s+s\alpha_i\), \(1-s+s\beta_i\) and reciprocal vertical scale, and lower. Each vertical half-size is at most \(\delta_zM\). During ascent/descent use the endpoint rectangle gaps; in the middle stage use the height gaps \(1/[4(m+1)]\). Enlarging by \(\mu\) preserves separation and stays in the cube. Thus Lemma 7 gives exact affine motion on the full boxes and positive collars. On their central sheet the first coordinate is \((1-s)X_1+sF_i(X)_1\).

The input point is the code of \((A_{q_0},\#\square^\infty,R_{\rm in}\#\square^\infty)\). A curl translation with plateau half-side \(1/32\) and margin \(1/32\) loads it from the fixed label during \([0,1]\). All paths stay inside the cube. Repetition gives a mean-zero velocity and Lemma 9 gives its residual force \(r\) and pressure zero. For the second choice, Proposition 5 solves \(\Delta\psi=\operatorname{div}r\), \(\int\psi=0\), and gives \[f_{\rm sol}=r-\nabla\psi,\qquad p=-\psi.\] It preserves all stated bounds and eventual periodicity, with precisely this change in pressure.

Induction at times \(1+k\) gives the prefix run until halt. A halt is in the slab, including an initial halt. For a nonhalting run the loader stays below \(1/2\) and each subsequent central-sheet coordinate remains between two nonhalt endpoints. No intermediate time enters the slab. The history recovers head displacement; the finite words above the two delimiters recover the full represented tape. ◻

Proof. For the full alphabet of size \(m\) use odd digits and base \(B=2m+1\). If there are \(m_s\) controls, put \(s_0=1/[16(m_s+1)]\). The halt square has corner \((13/16,1/4)\) and side \(s_0\); all other squares have corners \((1/8+2js_0,1/4)\) in their enumeration. Denote each assigned corner by \(p_s\). The nonhalting corners lie below first coordinate \(1/4\). Encode at height \(z_0=1/4\) by \[(p_s+s_0(E(A),E(B)),z_0).\] Lemma 6 supplies all rule rectangles and their exact positive diagonal maps.

Add a pair of equal-size loader squares centered at \((1/2,1/2)\) and \[y_{\rm in}=p_{q_0}+s_0 (E(M_L\square^\infty),E(w\square^\infty)).\] Its common half-side is half the minimum of \(1/16\) and the distances from \(y_{\rm in}\) to the sides of \(R_{\rm sep}=p_{q_0}+s_0(I(M_L)\times[0,1])\). These distances are positive, since infinite odd-digit codes lie strictly inside their prefix intervals. The loader source misses every state square. Its target lies in \(R_{\rm sep}\), whereas all ordinary targets in \(q_0\) have a history letter first on the left. Digit gaps therefore keep this new target separate. This verifies injectivity of the enlarged finite geometric family; it is the reason the loader may repeat.

Apply Lemma 8 to this family, including the loader. More explicitly, if there are \(N\) pairs, choose heights \(h_i=1/2+i/[4(N+1)]\). Write \(F_i\) for the affine map of pair \(i\). For its horizontal scale factors \(\lambda_{ia}\) let \[\Lambda=\max(\{1\}\cup\{\lambda_{ia}:1\le i\le N,\ a=1,2\}),\quad \Lambda_z=\max_i[\min(1,\lambda_{i1})\min(1,\lambda_{i2})]^{-1}.\] If \(g\) is the minimum of \(1\), horizontal boundary clearances, and the positive within-family coordinate-separating gaps, take horizontal source padding \(g/(10\Lambda)\) and vertical half-thickness \(1/[40(N+1)\Lambda_z]\). The linear horizontal scale \(1-s+s\lambda_{ia}\) and reciprocal normal scale keep endpoint padding at most \(g/10\) and middle-stage half-thickness at most one tenth of the height gap. The moving supports are consequently separate inside the cube. Use ascent, transformation, descent switches on \([1/8,2/8]\), \([3/8,5/8]\), \([6/8,7/8]\). The curl formula gives a mean-zero periodic velocity with zero collars at integer times. Its central-sheet horizontal path is \[ (1-s)y+sF_i(y). \tag{13}\] Lemma 9 supplies the force, with pressure zero.

The first period loads the input. Thereafter each period performs the next primitive rule. After \(r\) ordinary steps \(|H|=r\), so the sample time after \(k\) steps is \(1+\sum_{r=0}^{k-1}(2r+3)=(k+1)^2\). A halt code lies in the observed arc, also when \(k=0\). If the machine does not halt, all endpoints after loading have first coordinate below \(1/4\), while the initial one is \(1/2\). Equation (13) excludes the observed arc at every intermediate time. History displacements recover the absolute head index, and removing \(H,M_L\) recovers the tape. All branch and loader data were prepared from finite input, with no run computed. ◻

Proof. Put \(N=(1/8,3/8)^2\), \(J=(5/8,7/8)^2\). Place disjoint rational state squares in \(N\) for nonhalt controls and in \(J\) for halt controls. For \(k\) controls assigned to \((a,a+g)^2\), centers \((a+ig/(k+1),a+g/2)\) and half-side \(g/[4(k+1)]\) suffice. Let \(P_s\) map \([0,1]^2\) to the state square. With base \(B=2|\Sigma|+1\), odd digits and \(h_\sigma(x)=(d(\sigma)+x)/B\), an instruction \((s,\sigma)\mapsto(s',\tau,d)\) has normalized maps \[\begin{array}{ll} d=1:&(x,h_\sigma(y))\mapsto(h_\tau(x),y),\\ d=0:&(x,h_\sigma(y))\mapsto(x,h_\tau(y)),\\ d=-1:&(h_\lambda(x),h_\sigma(y))\mapsto (x,h_\lambda(h_\tau(y))),\quad\lambda\in\Sigma. \end{array}\] All free coordinates range over \([0,1]\). Determinism and read symbols separate sources. At a common target control the incoming move is fixed; distinct written symbols separate targets in the left first digit for \(d=1\), the right first digit for \(d=0\), and the right pair \((\lambda,\tau)\) for \(d=-1\). Hence the full target rectangles are separated as well. Composing with \(P_s,P_{s'}\) preserves positivity of the diagonal maps even when state squares have different sizes.

Apply Lemma 13 in \((0,1)^2\) with safe region \(N\). To retain the linear-width alternative explicitly, shrink to a common small rational half-side \(r\), use sequential parking routes, and linearly interpolate centers and widths with flat switches. If \(0<\beta<1\) makes the rectangles enlarged by \(1+\beta\) pairwise disjoint within each endpoint family, the cutoff \[\prod_{a=1}^2\left[1-\sigma\!\left( \frac{((x_a-c_a)/v_a)^2-1}{(1+\beta)^2-1}\right)\right]\] multiplied by \(\dot c+\operatorname{diag}(\dot v_a/v_a)(x-c)\) gives the exact closed rectangle path \(c(t)+\operatorname{diag}(v_a(t)/v_a(0))(x_0-c(0))\). Taking \(r\) below one sixteenth of every relevant rational squared clearance and endpoint half-side makes the small moving supports miss the stationary ones. Nonhalt paths remain in \(N\) throughout. This formula proves exactness on closed rectangles; the padded version of Lemma 13 separately gives exterior neighborhoods.

Load the rational initial code from \((1/4,1/4)\) by the same planar routing of a small square, confined to \(N\) when the initial state is nonhalting. Follow by the unit step pulse. Lift with \(h(z)=(z-1/2)\chi(z)\), where \(\chi=1\) for \(|z-1/2|\le1/8\) and is supported in \(|z-1/2|<1/4\). Lemmas 14 and 9 give the mean-zero velocity and force with pressure zero. At unit samples after loading the particle is the successive code. Halt codes lie in \(J\); a nonhalting run remains in \(N\) throughout loading and all later motions. This proves the event. The log’s leftmost nonblank cell remains absolute cell one, so the encoded tape also determines absolute head location. ◻

Proof. An output in \(O_r\) came by a right move. Its mark at relative position \(-1\) distinguishes the compute entry (one) from a loop (zero). In the first case \(r\) restores the old state, incoming tag, and work symbol; in the second there were no edits. An output in \(I_{q',d}\) came by a left move. Its history symbol at relative position \(2\) is a pointer precisely for the entry from \(O_r\); the return-loop guard excludes that case. For this entry the record at relative position \(1\) identifies \(r\) and restores the old pair \((\mathsf{top},\bot)\). An output in \(C_{q',d}\) has a unique predecessor type: undo move \(d\) and restore mark one. This proves injectivity on every actual rule output; it does not assert surjectivity or impose initialized-tape restrictions.

Since \(|h_n|\le n\), \(T_n>h_n\). The compute rule marks \(h_n\); the outgoing scan reaches \(T_n\), records the old data, advances the pointer, and returns from \(T_n-1\). Every return-scan cell is unmarked until the marked one, and its right neighbor is never the new pointer. Thus each guard holds. Clearing the mark and moving by \(d\) gives the next machine configuration, with \(h_n+d\le T_n<T_n+1\). The count is \(1+(T_n-h_n-1)+1+(T_n-h_n-1)+1\). It is at most \(4n+5\) for \(a=2\) and at most \(4n+3\) for \(a=1\). This proves the induction and includes initial halting. ◻

Proof. For the torus use \(a=2\), odd digits, base \(B=2|\Gamma|+1\), and \(\lambda=1/(16|\mathcal S|)\). Enumerating each type from zero, assign corners \[b_s=(1/8+2j\lambda,1/4)\quad(s\notin\mathcal H),\qquad b_s=(5/8+2j\lambda,1/4)\quad(s\in\mathcal H).\] Use the code \(b_s+\lambda(E(L),E(R))\). The nonhalt squares lie in \(0<x<1/4\) and the halt squares in \(1/2<x<7/8\). For Euclidean space use \(a=1\), base \(B=2|\Gamma|\) and digits \(0,2,\ldots,B-2\). Give halt controls offsets \(-2,-4,\ldots\) and all others offsets \(2,4,\ldots\), writing \(H(s)\) for the offset. Use \((H(s)+E(L),E(R))\). Zero digits can put codes on rectangle boundaries; our maps are exact on the full closed rectangles. Nonhalt rectangles lie in \(x\ge2\), and halt codes have \(x<0\). In each construction the prefixes in (14) give the separated rectangles required for planar routing.

Here are explicit choices retaining the two all-time avoidance bounds. Let \(N\) be the number of rectangle pairs. In the torus chart park at \[p_i=(x_*,i/(N+1)),\qquad x_*={\tfrac12}\min(\{1/4\}\cup\{c_{i1},d_{i1}\}),\] where \(c_i,d_i\) are endpoint centers. A bend with \(0<x<1/4\) can be chosen off the forbidden lines as follows: choose its abscissa below all vertical forbidden abscissae and \(1/4\), then its positive ordinate below \(1\) and below all positive values of the other lines there. All segments stay in the chart; when both endpoints are nonhalt their centers stay below \(1/4\). Let \(\rho\) be the minimum of \(1\), endpoint half-sides, boundary clearances, and squared distances from each segment to stationary centers. Half-side \(\epsilon=\rho/10\) gives disjoint translation supports because \(3\sqrt2\epsilon<\rho\le\sqrt\rho\). In Euclidean space park on the horizontal axis to the right of every endpoint and of \(2\). For a transfer use a bend \((m,m^2)\), where the integer \(m\ge2\) exceeds the Cauchy root bounds of all polynomials obtained by restricting forbidden lines to that parabola. Each polynomial is nonzero of degree at most two, so this terminates. A rational \(\epsilon<1\), below every endpoint half-side and one tenth of the minimum squared segment clearance, gives disjoint supports. A branch joining nonhalt rectangles has centers at least \(2\) throughout.

In either routing, shrink linearly to the small squares, translate them in sequence, and expand linearly in the target rectangles, using the closed-rectangle cutoff implementation in Lemma 13. Put all slots inside \([1/4,3/4]\). The normalized affine endpoint maps are exact, and the above clearances show that every nonhalt torus path has \(x<1/2\), while every nonhalt Euclidean path has \(x>0\). The empty list uses zero.

Let \(E_0,y_*\) be the rational initial planar codes. On the torus load from \(a=(1/16,1/16)\) by the spatially constant field \(\dot\eta(t)(E_0-a)\), with \(\eta\) flat from zero to one in \([1/4,3/4]\). Follow by the repeated rule pulse and lift with \(h(z)=\sin(2\pi z)/(2\pi)\). In Euclidean space load the origin along \(\theta(t)y_*\) with a compact moving cutoff equal to one on a square of half-side one and supported in its enlargement by one. Follow by the repeated planar pulse and lift with \(h(z)=z\chi(z)\), where \(\chi=1\) on \([-1,1]\) and is supported in \((-2,2)\). Lemma 14 gives the exact planar motions and Lemma 9 gives the forces. Its bounded-velocity comparison refinement is exactly the second row’s uniqueness class.

At time one both particles are their initial codes. Subsequent rule samples encode the run. In the torus case the \(n\)th compute visit is at \(1+\sum_{j<n}(2(T_j-h_j)+1)\) with \(T_j=j+2\); the Euclidean case has \(T_j=j+1\). A halt code satisfies the observer, including an initial halt after loading. In a nonhalting run the torus loader stays below \(1/4\), and the Euclidean loader has nonnegative first coordinate; all later paths obey the strict bounds proved above. The history block’s known absolute starting cell \(a\) recovers absolute head location as well as the head-relative work tape. All support and derivative bounds come from finitely many prescribed pulses. ◻

Proof. The displayed renaming is bijective and changes no write, displacement or top-letter guard in (11); it therefore conjugates the partial maps on all their cylinders. Allowing several halt states only omits their normal rules. The inverse distinctions at transfer, history-insertion and restoration states are unchanged, so the full-domain proof of Lemma 15 applies to this extension. That lemma also gives the initialized simulation and the exact count. The finite left word increases in length by at most one per ordinary transition, hence \(|L_j|\le j\). Displacement records recover the absolute head position. It lies in \([-j,j]\) after \(j\) transitions, and every nonblank work cell lies in \([-j,|w|+j]\): each step writes at the old head and moves by at most one. These bounds recover the finite tape content in addition to the halting event. ◻

Proof. Give each update case of Lemma 27 its own tag \(\lambda\), and add a reserved tag \(\bot\). Use distinct letters \(h_\lambda\), markers \(\#,\diamond\), and states \(B(q,\lambda)\), \(U(q,\lambda)\), \(V(q),D(q)\), with the last three types needed only for nonhalting \(q\).

At a main state the stacks are \(L\#Z,R\). The first rule inserts \(\diamond\), the \(k=|L|\) transfers and \(k\) restores leave the tape unchanged, insert \(h_\lambda\) into \(Z\), and remove \(\diamond\). The final update is exactly the four-case tape update proved above. The instruction count is \(1+k+1+k+1+1=2k+4\). Write \(\lambda_0=\bot\) and let \(\lambda_j\) be the \(j\)th update tag for \(j\ge1\). After \(j\ge0\) transitions the current tag is \(\lambda_j\) and the history is \(Z=h_{\lambda_{j-1}}\cdots h_{\lambda_0}\square^\infty\), with an empty recorded prefix when \(j=0\). Thus the loaded configuration has tag \(\bot\) and blank history, while for \(j\ge1\) the recorded prefix ends at \(h_\bot\). This recovers the displacement history and proves the configuration and halting correspondence, including an initially halted machine after the one loading instruction.

The complete rule list begins \[\begin{align*} (I;\epsilon,\epsilon)&\mapsto(B(q_0,\bot);\#,w),\\ (B(q,\lambda);\epsilon,\epsilon)&\mapsto(U(q,\lambda);\epsilon,\diamond),\quad q\notin H,\\ (U(q,\lambda);c,\epsilon)&\mapsto(U(q,\lambda);\epsilon,c),\quad c\in A,\\ (U(q,\lambda);\#,\epsilon)&\mapsto(V(q);\#h_\lambda,\epsilon),\\ (V(q);\epsilon,c)&\mapsto(V(q);c,\epsilon),\quad c\in A,\\ (V(q);\epsilon,\diamond)&\mapsto(D(q);\epsilon,\epsilon). \end{align*}\] For a transition \(\delta(q,a)=(q',b,d)\) the rules from \(D(q)\) are \[\begin{array}{c|c|c} 1&(D(q);\epsilon,a)&(B(q',\lambda);b,\epsilon)\\ 0&(D(q);\epsilon,a)&(B(q',\lambda);\epsilon,b)\\ -1, c\in A&(D(q);c,a)&(B(q',\lambda);\epsilon,cb)\\ -1, c=\#&(D(q);\#,a)&(B(q',\lambda);\#,\square b). \end{array}\] There are no outgoing rules from halting \(B(q,\lambda)\). The tags make every incoming branch to a \(B\)-state unique, including the loader, whose tag is \(\bot\). Images at \(U\) are separated by right tops \(\diamond\) versus \(c\in A\); images at \(V\) by left prefixes \(\#h_\lambda\) versus \(c\in A\); into \(D(q)\) there is one rule. Source separation is given by the displayed top-letter tests. Consequently both cylinder families are disjoint. ◻

Proof. Index \(e=(q,\ell,a)\) for every nonhalting \(q\) and \(\ell,a\in A\), and write \((q_e,b_e,d_e)=\delta(q,a)\). Add \(\#,\diamond,\tau_e\) and states \(F_e,J_q\). The first rule has source \((q;\ell,a)\) and target \[\begin{cases} (F_e;\diamond b_e\ell,\epsilon),&d_e=1,\\ (F_e;\diamond,\ell b_e),&d_e=-1,\\ (F_e;\diamond\ell,b_e),&d_e=0. \end{cases}\] Add \[\begin{align*} (F_e;\epsilon,c)&\mapsto(F_e;c,\epsilon)&&(c\in A),\\ (F_e;\epsilon,\#)&\mapsto(J_{q_e};\epsilon,\square\#\tau_e),\\ (J_q;c,d)&\mapsto(J_q;\epsilon,cd)&&(c,d\in A),\\ (J_q;\diamond,\epsilon)&\mapsto(q;\epsilon,\epsilon). \end{align*}\] All source tests are disjoint. Into \(F_e\) the entry starts the left stack with \(\diamond\), whereas each loop starts it with a distinct tape letter. Into \(J_q\) the right prefixes \(\square\#\tau_e\) are separated from one another by their tags and from every \(cd\) by the second letter; the \(cd\) themselves distinguish loop images. There is one incoming rule to \(q\).

Writing \(r=ar_1\), the word \(v\) is respectively \(r_1\), \(\ell b_er_1\), or \(b_er_1\). The left stack below the inserted \(\diamond\) is exactly the updated infinite left tape. The \(F_e\) loop moves the finite word \(v\) onto that stack in reverse order. The delimiter rule adds a blank and records \(e\). The \(J_{q_e}\) loop restores \(v\) while its second-stack first letter remains in \(A\), and its exit removes \(\diamond\). There are \(1+|v|+1+|v|+1\) rules. In particular the possibly empty \(v\) after a right move causes no undefined rule: the inserted blank supplies the next scanned cell. Start with \(L=\square^\infty\), \(r=w\square\), and empty history. Induction proves the claimed tape interpretation and exact halting equivalence. History length gives the number of simulated transitions and their displacements. After \(k\) transitions the head lies in \([-k,k]\) and no nonblank tape cell lies outside \([-k,|w|+k]\). Reading the finite right word up to \(\#\) and the first \(2k\) letters of \(L\) therefore recovers all possibly nonblank tape cells: a left offset greater than \(2k\) has absolute index less than \(-k\). The record list supplies the absolute head index. ◻

Proof. Use main labels \(M_q\), branch labels \(D_e\), restore labels \(C_q\), a delimiter \(\#\), distinct records \(k_e\), and a disjoint tagged copy \(\bar A=\{\bar a:a\in A\}\).

At \(M_q\) the stacks are \(L\# Z,R\), starting at \(\#^\infty,w\square^\infty\). Each main rule performs precisely the head-relative tape update; for a right move the lookahead \(c\) is retained and becomes current. The \(m\) updated left letters are transferred with tags, the record is inserted below \(\#\), and the \(m\) tagged letters are restored and untagged. The untagged right top then triggers the exit. This gives \(2m+3\) instructions and the next main configuration. Every scan is finite, and no untagged tape data are confused with the tagged scan segment. The same induction as in Lemma 27 proves the halting equivalence and reconstruction of head displacement.

A right-moving transition is split by its next right letter: \[(M_q;\epsilon,ac)\mapsto(D_e;b,c),\qquad c\in A.\] For a left move use \((M_q;\alpha,a)\mapsto(D_e;\epsilon,\alpha b)\) for \(\alpha\in A\), and \((M_q;\#,a)\mapsto(D_e;\#,\square b)\). For a stay use \((M_q;\epsilon,a)\mapsto(D_e;\epsilon,b)\). Every displayed case has its own \(e\), with destination \(q'(e)\). Complete the table by \[\begin{align*} (D_e;\alpha,\epsilon)&\mapsto(D_e;\epsilon,\bar\alpha),\quad\alpha\in A,\\ (D_e;\#,\epsilon)&\mapsto(C_{q'(e)};\#k_e,\epsilon),\\ (C_q;\epsilon,\bar\alpha)&\mapsto(C_q;\alpha,\epsilon),\quad\alpha\in A,\\ (C_q;\epsilon,a)&\mapsto(M_q;\epsilon,a),\quad a\in A. \end{align*}\] Sources separate by their indicated letters and the right lookahead. Into \(D_e\), the main-rule image has an untagged right top while loop images have distinct tagged tops. Into \(C_q\), the left prefixes \(\#k_e\) separate entries from loops with untagged left tops. The incoming rules to \(M_q\) preserve distinct right tops \(a\). These facts prove full-cylinder injectivity. ◻

Proof. Use fresh markers \(J,E\), a history base \(g_*\), and records \(g_\tau\). A tag \(\tau\) specifies \((q,a,d,c)\) for a moving rule, where \(c\in A\) is the neighboring tape letter or \(c=\perp\) denotes a window edge; a stay has tag \((q,a,0,\perp)\). Use scan states \(S_q\) for nonhalting \(q\) and restore states \(D_\tau\). With \(w_0=w\) for nonempty \(w\) and \(w_0=\square\) otherwise, the boot and scan rules are \[\begin{align*} (s_*;\epsilon,\epsilon)&\mapsto(N_{q_0};Jw_0E,g_*),\\ (N_q;\epsilon,h)&\mapsto(S_q;\epsilon,h),\quad q\notin H,\ h\in\Lambda,\\ (S_q;c,\epsilon)&\mapsto(S_q;\epsilon,c),\quad c\in A, \end{align*}\] where \(\Lambda=\{g_*\}\cup\{g_\tau\}\). For \(\delta(q,a)=(q',b,d)\) the update rules are \[\begin{array}{c|c|c} 0&(S_q;Ja,\epsilon)&(D_{(q,a,0,\perp)};Jb,\epsilon)\\ 1, c\in A&(S_q;Jac,\epsilon)&(D_{(q,a,1,c)};Jc,b)\\ 1,\ \text{edge}&(S_q;JaE,\epsilon)&(D_{(q,a,1,\perp)};J\square E,b)\\ -1, c\in A&(S_q;Ja,c)&(D_{(q,a,-1,c)};Jcb,\epsilon)\\ -1,\ \text{edge}&(S_q;Ja,h)&(D_{(q,a,-1,\perp)};J\square b,h),\quad h\in\Lambda. \end{array}\] Finally include \((D_\tau;\epsilon,c)\mapsto(D_\tau;c,\epsilon)\) for \(c\in A\) and \((D_\tau;\epsilon,h)\mapsto(N_{q'_\tau};\epsilon,g_\tau h)\) for \(h\in\Lambda\).

The domains separate by history tops at \(N\), by tape tops versus \(J\) at \(S\), by the tested current letter and neighbor, and by second-stack tops at \(D\). Into \(S_q\), history tops distinguish entry from tape-letter scan images. Into \(D_\tau\), first tops \(J\) distinguish updates from restore loops; the only multiple update entries sharing one tag are the left-edge variants, whose second tops \(h\) distinguish their images. Into a main state the prefixes \(g_\tau h\) distinguish every restore image; the boot image instead starts with \(g_*\). Hence both full cylinder families are disjoint.

Entering \(S_q\) and transferring \(\ell\) leaves \(Ja rE^\infty\) and puts \(\operatorname{rev}(\ell)\) above the old history. A stay replaces \(a\) by \(b\). A right move pushes \(b\) onto this reversed left segment and takes the next right cell as current, inserting \(\square\) if at the edge. A left move pops the nearest left cell, or uses a new blank if there is none, and puts \(b\) at the front of the right segment. The \(D_\tau\) loops restore the new left segment in its original order, and the exit records the tag. Counting entry, the \(|\ell|\) scan moves, the update, \(|\ell_{\rm new}|\) restore moves, and the exit proves the formula. This also proves the invariant and that every simulated step is finite. The tag list determines absolute head position. An initially halted machine is detected immediately after boot; otherwise halting and nonhalting follow by induction. ◻

Proof. This is the recorder of (OpenAI 2026, Lemma 2.1) with initial frontier \(r_0=2\), under the following bijections of control states and history letters: \[(S_q,A_r,R_r,F_q,L_q)\mapsto(B_q,A_r,R_r,N_q,L_q),\qquad (E,P,[r])\mapsto(\mathtt e,\mathtt F,\lambda_r).\] The work alphabet and marker bit are unchanged. In rows one, two, three, six, and seven the history symbol is required to differ from the frontier; row four reads the frontier, and row five reads an empty history cell. These are exactly the guards in (OpenAI 2026, Lemma 2.1). The writes and displacements also agree row by row. Thus these bijections conjugate the entire partial transition, not only its initialized orbit. Its full-domain inverse, destination-determined incoming directions, and distinguishing written symbols transfer.

The initialization sets every history cell to \(\mathtt e\) except for \(\mathtt F\) at absolute cell \(2\), and sets every marker bit to zero. The checkpoint invariant of (OpenAI 2026, Lemma 2.1) gives records at \(2,\ldots,n+1\), frontier \(2+n\), and original work head \(h_n\). Its count \(2(r_0+n-h_{n+1})+4\) is the asserted count. The same invariant includes an initially halted machine. ◻

Proof. Write a tape cell as \((a_j,g_j,m_j)\) with indices relative to the head. After the indicated edits a displacement \(d\) recenters by \(s'_j=\widetilde s_{j+d}\).

Initially the auxiliary head is at absolute cell \(0\) in \(S_{q_0}\), all marker bits are zero, the history symbol is \(\#\) at absolute cell \(2\) and \(\bot\) everywhere else, and the work track is the input followed by blanks on the rest of the tape. At checkpoint \(n\), the records occupy cells \(2,\ldots,n+1\), the frontier is at \(e=2+n\), and the other history cells are empty. This holds at initialization. After the work update the new head \(h'<e\) is marked, then the right scan finds \(e\). Its two-cell rule records the transition and puts the frontier at \(e+1\), starting the return at \(e-1\). Along that return the cell to the right has index at most \(e\), so it is not the new frontier; the loop guard is satisfied until the marked cell is reached. Clearing the marker gives the next checkpoint. The count is one work update, one marking update, \(e-h'-1\) outward loops, one frontier update, \(e-h'-1\) inward loops, and one exit, totaling \(2(e-h')+2\).

Use the following entire table: \[\begin{array}{c|l|l|c|c} \text{label}&\text{condition}&\text{edits}&d&\text{new label}\\\hline S_q&a_0=a&r=(q,a),\ a_0\gets b_r&d_r&P_r\\ P_r&m_0=0&m_0\gets1&1&R_r\\ R_r&m_0=0,\ g_0\ne\#&\text{none}&1&R_r\\ R_r&m_0=0,\ g_0=\#,\ g_1=\bot&g_0\gets r,\ g_1\gets\#&-1&L_{q_r'}\\ L_q&m_0=0,\ g_1\ne\#&\text{none}&-1&L_q\\ L_q&m_0=1&m_0\gets0&0&S_q. \end{array}\] The first row is present only for nonhalting \(q\).

Injectivity must hold beyond these intended runs. For output \(P_r\), the record in the label determines the old state, overwritten work symbol, and displacement. Into \(R_r\) the output marker at index \(-1\) distinguishes the marking entry from the loop. Into \(L_q\), an incoming frontier update has a delimiter at output index \(2\) and a determining record at index \(1\); a continuation cannot have that delimiter because its old \(g_1\ne\#\). In the first case restore the old delimiter and empty following history cell; in the second simply undo the shift. Into \(S_q\), restore a marker bit at index \(0\). These inverse rules prove injectivity of the entire partial update.

Fix the source symbols at \(-1,0,1\) and the label wherever a row is defined. The edited source window, after shift \(d\), occupies \(-1-d,\ldots,1-d\), and its left and right prefix lengths are \(1+d\) and \(2-d\). Everything outside this window is an unrestricted unchanged tail, with the same order on its respective side. Thus the image is a whole prefix cylinder. Source cylinders partition the domain; injectivity makes their images disjoint. No assertion merely about one initialized orbit is used in passing to rectangles. ◻

Proof. The encodings are injective by the gap argument, so the indicated map and inverse are well defined on the coded sets. Applying one branch replaces exactly its two prefixes, leaving both words’ tails unchanged in either convention; the two possible compositions therefore yield the same encoded output. Equation (15) proves the stronger full-rectangle identity in each encoding. This is a conjugacy of the specified partial symbolic dynamics; the separately given interpolation paths establish their respective all-time fluid events. ◻

Proof. Write \(U(s,x)\) for the chosen construction, including its loading interval. It is periodic only after that interval, but all its derivatives are uniformly bounded on the whole half-line. Put \[s(t)=\log(1+t),\quad a(t)=(1+t)^{-1},\quad \widehat U(t,x)=a(t)U(s(t),x).\] It is smooth and effective and has the same spatial support. Since \(U(0)=0\), its initial velocity is zero. For every spatial multi-index \(\alpha\), \[\partial_x^\alpha\widehat U=a(\partial_x^\alpha U)\circ s, \qquad \partial_t\partial_x^\alpha\widehat U =a'(\partial_x^\alpha U)\circ s +a^2(\partial_s\partial_x^\alpha U)\circ s.\] The uniform derivative bounds for the original finite pulse give the stated spatial and first-time estimates. Repeated chain and product rules express every higher mixed derivative as a finite sum of bounded derivatives of \(U\) multiplied by derivatives of \(a\) and \(s\), so all are bounded as well. The new residual force is exactly \[\mathcal F_\nu[\widehat U] =a'U\circ s+a^2\big(\partial_sU+(U\cdot\nabla)U\big)\circ s -\nu a(\Delta U)\circ s.\] Its pointwise magnitude is at most \(C(1+t)^{-1}\). Fixed compact support gives a finite space-time square integral, since \(\int_0^\infty(1+t)^{-2}\,dt<\infty\). The same realization and uniqueness argument applies. If \(X(s)\) was the original material path, then \(X(s(t))\) solves the new particle ODE by the chain rule. The clock is increasing and maps \([0,\infty)\) onto itself, so the two paths have identical images and exactly the same observation event. A checkpoint at original time \(s_j\) is reached at the finite new time \(e^{s_j}-1\); no finite upper bound on the halting time is required to prescribe this clock. ◻

Proof. Choose a positive rational margin \(\epsilon\) at most one quarter of a positive coordinate-separating gap for each pair in each family; for empty pair lists take \(\epsilon=1\). The enlarged families stay disjoint. Choose rational \(D_0\) larger than \(\epsilon\) plus every source or target half-side. Take an integer \(G\ge1\) so that within each family the scaled centers \(Gc_i\) and \(G\widehat c_i\) are more than \(10D_0\) apart in the sup norm. Choose parking centers \(e_i\) more than \(10D_0\) apart from one another and from all these scaled centers. A sufficiently distant row with spacing \(20D_0\) does this effectively.

Use affine paths \[ X\mapsto C_i(\xi)+\operatorname{diag}(a_i(\xi),a_i(\xi)^{-1})(X-c_i). \tag{23}\] First translate centers simultaneously \(c_i\to Gc_i\), keeping shapes fixed; any coordinate separation can only increase. Next move one rectangle at a time to \(e_i\). At those parking centers change \(a_i\) from \(1\) to \(\lambda_i\). Each half-side stays between its endpoint values and hence below \(D_0-\epsilon\). Move the target-shaped rectangles one at a time to \(G\widehat c_i\), then translate centers simultaneously down to \(\widehat c_i\). In this last phase the target separations stay valid down to scale one. During source evacuation, occupied centers are scaled source centers or parking centers. During target delivery, every source has already been evacuated, and occupied centers are parking centers or scaled target centers. Each such mixed family has separation greater than \(10D_0\) by the choices above. Thus arbitrary intersections between the original source and target families never place two occupied rectangles at the same location. The obstacle family for each transfer consists of every other currently occupied rectangle, wherever it is in that phase.

For a one-at-a-time transfer, put a closed square of sup radius \(4D_0\) around every stationary center. These obstacles are disjoint, and the transfer endpoints are outside them. Follow the straight segment, replacing any portion inside one obstacle by a boundary detour in a fixed orientation. Entry and exit points solve rational linear inequalities, so all waypoints are rational. A tangent contact, a corner contact without entry, or a segment already on the boundary needs no detour: it already has the required clearance. A segment crossing the interior has rational first and last intersection points, found by clipping its rational parameter interval against the four rational side inequalities. A fixed clockwise boundary arc between those points uses only rational corners. The obstacles are separated, so each detour misses every other obstacle. The moving center remains at sup distance at least \(4D_0\) from all stationary centers; both enlarged rectangles have radius less than \(D_0\), proving separation throughout.

Schedule the finitely many submotions in successive equal slots inside \([1/3,2/3]\), using a flat step for each segment and scale change. This smooths time without changing any path or clearance. Let \(\chi_i\) equal one on a positive collar of the moving rectangle and be supported in its \(\epsilon\) enlargement. With \(Y=X-C_i\), set \[ \mathcal H=\sum_i\chi_i\left( \dot C_{i1}Y_2-\dot C_{i2}Y_1 +\frac{\dot a_i}{a_i}Y_1Y_2\right),\qquad V=(\partial_{X_2}\mathcal H,-\partial_{X_1}\mathcal H). \tag{24}\] The supports are disjoint. On rectangle \(i\) the field is \(\dot C_i+\operatorname{diag}(\dot a_i/a_i,-\dot a_i/a_i)(X-C_i)\), so (23) solves its ODE exactly. The same formula holds on a positive initial neighborhood by the plateau and finite affine norm bounds. Smooth ODE uniqueness identifies the motion. A rational support bound follows from the finite endpoint and waypoint list plus \(D_0+1\). Every operation is effective finite geometry and the fixed flat step, proving the lemma. ◻