Princess searches: parked companion proofs

13 Sep 2026

This companion preserves independent extensions and their existing proofs. It is parked: these open directions are not requirements for completing the rectangle project. Relevant fixed-deadline rectangle consequences remain with the main manuscript.

Rectangle overview · Progress reconciliation · Coverage and remaining gaps · Parked companion · PDF from the same source

Preserved results and parked scope

This companion preserves independent results from the combined September 2026 manuscript. No new mathematical results are asserted by the split. The active project asks for an absolute $O(1)$ numerical expression for $T_k(a,b)$ on every rectangle with constant budget and full initial uncertainty, together with directly specified optimal inspections and proofs of capture and minimality. This companion does not enlarge that completion criterion. Its research directions are parked until an explicit decision to resume them.

The preserved results include whole-strategy normal forms for equal-sided boxes; isoperimetric nesting and exact two-count evaluation on every all-odd box; reductions for boxes with a side of length two; exact profile transfer for either longitudinal parity; the complete $3\times3\times3$ , $4\times4\times4$ and $3\times4\times4$ time tables; and the all-length five-inspection formula $18n-36$ on $3\times3\times n$ , $n\ge3$ . General-cylinder height bounds, feasibility, growth rates and effective eventual affine periods are also preserved. Their algorithms and parameter-dependent finite preprocessing are not presented as uniform fixed-size closed forms.

For reference the complete three-cube values are $\begin{array}{c|rrrrrrrr} m&0\!:\!4&5&6&7\!:\!8&9\!:\!11&12&13\!:\!26&27\text{ or more}\\\hline T_m(P_3^3)&\infty&18&10&6&4&3&2&1. \end{array}$ The box applications depend on the shared game semantics and compression lemmas proved in the main manuscript. References marked “main” point to that paired document and use its theorem numbering. The shared odd-period proof uses its local labels and links its rectangle-profile specialization to the main proof. There is one authoritative Lean source tree; application manifests, not duplicated formal developments, distinguish the two scopes.

The generic survivor-envelope transfer in the main manuscript applies also to non-path cross-sections and varying prescribed daily capacities. Those independent applications are parked here, while the minimum constant budget for a fixed deadline on a rectangle remains a consequence of the active capture-time relation. Likewise, a generic partial-state lemma may remain a main proof dependency without making its universal optimality theory an active objective.

How to resume

Read the scope document and companion handoff before choosing a new question. Identify its graph family, budget convention, initial uncertainty and desired output; do not inherit the rectangle completion criterion or silently extend it. The accompanying restart notes preserve accepted results, ordinary-proof and formal boundaries, finite witnesses, failed approaches, and unfinished investigations. The 13 September 2026 combined release is the immutable comparison point for this separation.

Equal-sided boxes and independent compression applications

The comparison operators are retained with the rectangle tools in the main manuscript. Here we preserve their independent higher-dimensional application.

Theorem 2.1 (Normal form on equal-sided boxes). On $P_n^d$ , $n\geq2$ , an optimal strategy from the full board can be chosen so that its possible-position sets and survivors are lower ideals for the legal moves $v\longmapsto v+e_i-e_j,\qquad v\longmapsto v-e_i-e_j, \qquad i<j.$ (2.1) The conclusion respects arbitrary prescribed daily budgets. The same operators are available within every group of equal-length coordinates in an arbitrary Cartesian box. Odd-coordinate path compressions can be included simultaneously.

Proof. Lift both square operators to every pair $i<j$ of equal coordinates. They compress toward smaller $x_j$ on lines $x_i+x_j=k$ and $x_i-x_j=k$ . Use the potential $\mathcal E(S)=\sum_{v\in S}\sum_{i=1}^d i v_i.$ A nontrivial plus-diagonal transfer by $\delta>0$ decreases it by $(j-i)\delta$ , and a minus-diagonal transfer by $(i+j)\delta$ . An odd-coordinate prefix transfer also strictly decreases it. The potential is uniformly bounded; on $P_n^d$ the bound $n^d(n-1)d(d+1)/2$ suffices. Uniform cycling therefore gives an idempotent strategy compression. Its fixed sets are precisely the ideals for the displayed local moves, with the additional $-2e_i$ conditions when odd-coordinate operators are included. Apply Theorem 3.2 (main). ◻

In dimension two the two-diagonal fixed sets are the downward pyramidal sets of the square isoperimetric argument. They differ from ordinary checkerboard corner ideals. In any dimension they give an exact finite recurrence over their fixed family, since both neighborhoods and intersections remain fixed. The theorem does not bound the number of these ideals by a polynomial in $d$ or in $n$ .

An exact isoperimetric order in every all-odd box

The preceding rectangle theorem extends to every dimension. The extension uses a weighted exchange argument: compression in lower-dimensional faces first makes neighborhood size a sum of local costs, and an order comparison then identifies exchanges that cannot increase that sum. Parity-restricted isoperimetry on hypercubes was studied by Körner and Wei (1984), and local-to-global methods for Cartesian-product vertex boundaries by Bezrukov and Serra (2002). Here the neighborhood is the open neighborhood of a single color class. We give the face compressions and their exchange argument explicitly, rather than infer the result from a theorem about closed vertex boundaries.

Delete any factors of side length one, and write the remaining box as $B=\prod_{i=1}^d\{0,\ldots,L_i\},\qquad 2\le L_1\le\cdots\le L_d,\qquad L_i\text{ even}.$ Thus coordinates are ordered from the shortest side to the longest. Let $B_p$ be its color- $p$ class, where the color of $x$ is the parity of $|x|=\sum_i x_i$ . Within either color, order vertices by increasing $|x|$ and then by decreasing lexicographic coordinates. Write $x\prec y$ for this order and $I_p(k)$ for its first $k$ vertices. The direction of the lexicographic tie is part of the definition.

Theorem 3.1 (Compatible isoperimetric nesting in all-odd boxes). For every $S\subseteq B_p$ , $|N(S)|\ge |N(I_p(|S|))|.$ Moreover, $N(I_p(k))$ is a prefix in the opposite color. Consequently the minimum capture time for every inspection budget on $B$ is given by an exact recurrence on $O(|B|^2)$ states, and optimal inspection sets can be recovered from that recurrence.

For $d=1$ the minimizing order is the spacing-two prefix order of Lemma 3.4 (main). For $d=2$ , putting the shorter coordinate first and ordering it decreasingly within a weight layer is equivalent to the increasing-long-coordinate convention of Theorem 5.1 (main). These provide the induction bases. In particular, the higher-dimensional assertion does not assume a general Cartesian-product isoperimetric principle.

Prefix neighborhoods and a local cost identity

For a nonzero vertex $z$ , let $j(z)$ be its last positive coordinate and put $\ell(z)=z-e_{j(z)}.$ This is its earliest lower neighbor in decreasing lexicographic order.

Lemma 3.2 (Nesting of prefix neighborhoods). For the stated weight and lexicographic order, the neighborhood of a prefix is a prefix of the opposite color. This statement holds even without the assumptions that the side lengths are odd and sorted.

Proof. Within a fixed weight layer, $\ell$ preserves order, allowing ties. Indeed, suppose $z\prec w$ first differ in coordinate $i$ , so $z_i>w_i$ . Equal weights imply that $w$ has a positive coordinate after $i$ . If $z$ does too, neither predecessor operation changes the first difference. Otherwise $j(z)=i$ and $z_i-1\ge w_i$ . A strict inequality preserves the order. In the equality case the tail of $w$ has total weight one; removing its unique unit gives $\ell(z)=\ell(w)$ .

Consider a nonempty prefix whose last, possibly partial, layer has weight $r$ . Every smaller opposite-color layer is completely covered: its nonzero vertices have lower neighbors in complete source layers. When weight zero belongs to the opposite color, it is covered by the first odd layer. No vertex above layer $r+1$ is covered. On layer $r+1$ , a vertex is covered precisely when its earliest lower neighbor belongs to the selected prefix in layer $r$ . The order preservation just proved makes these covered vertices an initial interval of layer $r+1$ . The empty prefix is immediate. ◻

Call a set pair-compressed if, after fixing all but any two coordinates, its selected vertices in either free-coordinate parity form a prefix of the inherited order. Define $a(0)=d,\qquad a(x)=d-j(x)+1-\mathbf{1}_{\{x_{j(x)}=L_{j(x)}\}}\quad(x\ne0).$ (1)

Lemma 3.3 (Neighborhood cost of a pair-compressed set). If $d\ge2$ and $\varnothing\ne S\subseteq B_p$ is pair-compressed, then $|N(S)|=\sum_{x\in S}a(x)+\mathbf{1}_{\{p=1\}}.$ (2)

Proof. For every nonzero $z$ , we claim $z\in N(S)\quad\Longleftrightarrow\quad\ell(z)\in S.$ Only the forward implication needs proof. Choose a neighbor $x\in S$ of $z$ . The vertices $x$ and $\ell(z)$ differ in at most two coordinates. If $x$ is a lower neighbor, then $\ell(z)$ is no later than $x$ in their common weight layer. If $x$ is an upper neighbor, $\ell(z)$ has weight two less than $x$ . Pair compression therefore puts $\ell(z)$ in $S$ . If only one coordinate differs, any second coordinate can be used; one exists because $d\ge2$ .

For $x\ne0$ with last positive coordinate $J$ , the preimages of $x$ under $\ell$ are obtained by adding one in coordinate $J$ , if it is not full, or by adding one in any coordinate after $J$ . Their number is $a(x)$ . The origin has the $d$ unit vectors as preimages. Thus the sum in (2) counts every nonzero neighbor exactly once.

If $p=1$ , a nonempty pair-compressed set contains a unit vector. Starting with any of its vertices of weight greater than one, decrease by two in a coordinate that is at least two, or decrease by one in two positive coordinates. Each move stays in a pair fiber and goes earlier in its order, so it preserves membership. The process ends at weight one. The origin is therefore an additional neighbor when $p=1$ , and it can never be a neighbor when $p=0$ . ◻

Face compression and its partial order

Suppose $d\ge3$ and the isoperimetric theorem has been proved in dimension $d-1$ . On each fixed color define a partial order $\le_P$ as the reflexive transitive closure of $x<_P y\quad\hbox{if }x\prec y \hbox{ and }x_i=y_i\hbox{ for at least one }i.$ (3) All generating relations increase the total order, so this is indeed a partial order. Its ideals are exactly the sets whose restriction to every codimension-one fiber is a prefix.

The inductive isoperimetric theorem and compatible neighborhood nesting make the prefix map on each $(d-1)$ -dimensional box a strategy compression: it is monotone, preserves cardinality, and sends each color’s neighborhood into the corresponding prefix of the original neighborhood’s size. The remaining side lengths are still sorted, and their order is the restriction of the global order to a fixed-coordinate fiber. By Lemma 3.3 (main), compressing all such fibers for one coordinate index is a strategy compression of $B$ .

Cycle through the $d$ indices. Every change strictly decreases the sum of the selected vertices’ positions in the global weight and lexicographic order. This nonnegative integer is bounded by $|B|(|B|-1)/2$ . The simultaneous-compression argument in Section 3 (main) therefore gives a uniform finite composition whose output is fixed by every face compression. In particular, every $S\subseteq B_p$ can be replaced by a $P$ -ideal of the same size without increasing its neighborhood.

Every $P$ -ideal is pair-compressed. A two-coordinate fiber lies inside a codimension-one fiber obtained by fixing a coordinate outside the pair; such a coordinate exists because $d\ge3$ . The restriction of a prefix to a subfiber is a prefix of its inherited order. Thus Lemma 3.3 applies to the resulting ideals.

The exchange comparison

The following elementary comparison is the step that links the local cost identity to the global order.

Lemma 3.4 (Terminal-coordinate comparison). Let $d\ge3$ . If same-parity vertices satisfy $x\prec y$ and $x_d=0<y_d$ , then $x\le_P y$ . Also, if $x\prec y$ and $x_d<y_d=L_d$ , then $x\le_P y$ .

Proof. First, if $u\le v$ coordinatewise and their weights have the same parity, then $u\le_P v$ . Perform all required increments of size two within individual coordinates, and then pair the remaining increments of size one. Each step increases weight by two and changes at most two coordinates. Since $d\ge3$ , it leaves a coordinate unchanged and is a generator of (3).

For the first assertion, a coordinate agreement between $x$ and $y$ already gives a generator. Assume henceforth that all coordinates differ. If $|x|<|y|$ and some $i<d$ has $x_i>y_i$ , transfer $t=x_i-y_i$ units from coordinate $i$ to coordinate $d$ of $x$ , obtaining $z$ . This is legal because $0<t\le L_i\le L_d$ and $x_d=0$ . We have $x\prec z$ within their common weight layer, while $z\prec y$ follows from $|z|=|x|<|y|$ . The vertex $z$ retains $d-2\ge1$ coordinates of $x$ and agrees with $y$ in coordinate $i$ . Hence $x<_P z<_P y$ . If there is no such excess coordinate, then $x\le y$ coordinatewise, and the preceding observation applies.

It remains to consider $|x|=|y|$ . Since all coordinates differ, $x_1>y_1$ . If a middle coordinate $2\le i\le d-1$ has $x_i>y_i$ , use the same transfer to coordinate $d$ . Again $x\prec z$ , and $z\prec y$ because $z_1=x_1>y_1$ . The same coordinate agreements give the two generators. Otherwise all middle coordinates increase: $x_i<y_i$ for $2\le i\le d-1$ . Weight equality gives $x_1-y_1=y_d+\sum_{i=2}^{d-1}(y_i-x_i).$ Transfer $y_d$ units from the first to the last coordinate of $x$ . The resulting vertex $z$ is valid, since $z_1=y_1+\sum_{i=2}^{d-1}(y_i-x_i)>y_1\ge0, \qquad z_d=y_d\le L_d.$ It satisfies $x\prec z\prec y$ , shares the middle coordinates with $x$ , and shares the last coordinate with $y$ . This proves the first assertion.

The coordinate complement $\rho(x)_i=L_i-x_i$ reverses the weight and lexicographic order, and it preserves coordinate agreements. It therefore reverses the generated partial order. Applying the first assertion to $\rho(y)\prec\rho(x)$ proves the second assertion. ◻

Lemma 3.5 (Cost comparison). If $x\prec y$ have the same parity and $a(x)>a(y)$ , then $x\le_P y$ .

Proof. If $x_d=y_d$ , they share a coordinate. If $x_d=0<y_d$ , use the first part of Lemma 3.4. The case $y_d=0<x_d$ cannot give a strict cost decrease, since $a(x)\le1$ and $a(y)\ge1$ . Finally, if both last coordinates are positive, both costs are zero or one. A strict decrease forces $x_d<L_d=y_d$ , so the second part of that lemma applies. ◻

Proof of Theorem 3.1. The path and rectangle bases were noted above. In dimension $d\ge3$ , the inductive face compressions replace an arbitrary $S\subseteq B_p$ by a $P$ -ideal of the same size and with no larger neighborhood. The empty set needs no further argument.

If a nonempty $P$ -ideal is not a global prefix, let $x$ be its earliest missing vertex and $y$ its latest included vertex. Then $x\prec y$ . They are incomparable in $P$ : $x\le_P y$ would contradict ideality, and $y\le_P x$ would contradict the global order. By Lemma 3.5, $a(x)\le a(y)$ .

Replace $y$ by $x$ . Removing $y$ preserves ideality because every proper successor of $y$ is later in the global order and hence absent. Adding $x$ preserves ideality because every proper predecessor of $x$ is earlier and hence present; $y$ is not such a predecessor. The new set has the same positive cardinality and color. The neighborhood cost identity (2) shows that its neighborhood does not increase. The sum of global positions strictly decreases, so iteration ends at the global prefix of that size. This proves the isoperimetric inequality. Lemma 3.2 gives compatible nesting, completing the induction. ◻

Profiles, exact capture times, and optimal inspections

Write $V=|B|$ , $E=(V+1)/2$ , and $M=(V-1)/2$ . The theorem supplies the complete profiles by a direct cumulative-sum construction: $g_p(0)=0,\qquad g_p(k)=\sum_{x\in I_p(k)}a(x)+\mathbf{1}_{\{p=1\}}\quad(k>0).$ (4) For $d=1$ these expressions also agree with the odd-path profiles. Enumerate the vertices, order each color as specified, evaluate (1), and take cumulative sums. Using a mixed-radix lexicographic index, sorting requires $O(V\log V)$ integer comparisons; computing weights, indices and costs directly requires $O(dV)$ additional operations. This is a constructive profile algorithm, without an isoperimetric optimization subroutine.

Corollary 3.6 (Feasibility by one profile maximum). For every nontrivial all-odd box, the minimum feasible daily budget is $h(B)=1+\max_{0\le k\le E}\bigl(g_0(k)-k\bigr) =1+\max_{0\le k\le E} \sum_{x\in I_0(k)}\bigl(a(x)-1\bigr).$ (5) The one-room box has threshold one by direct inspection.

Proof. We verify the hypotheses of the general hunter-number criterion of Bolkema and Groothuis (2019, Theorem 16). That theorem states that a bipartite graph with compatible isoperimetric nesting has hunter number $1+\min(u_0,u_1)$ when the maximum neighborhood surpluses $u_p=\max_k(g_p(k)-k)$ differ by at most one.

For completeness, the exact profile duality gives the required relation between these maxima. Define $J(z)=\max\{x:0\le x\le E,\ g_0(x)\le z\}, \qquad 0\le z\le M.$ Then $g_1(y)=E-J(M-y).$ (6) Indeed, a majority set of size $x$ with at most $M-y$ neighbors leaves a minority $y$ -set with no edges to it, giving $g_1(y)\le E-x$ . Conversely, the majority complement of the neighborhood of a minimizing minority $y$ -set has size $E-g_1(y)$ and at most $M-y$ neighbors. These two choices prove (6). Since $E=M+1$ , it follows that $u_1=1+\max_{0\le z\le M}(z-J(z)).$ This last maximum equals $u_0$ . If $J(z)<E$ , let $x=J(z)+1$ . Then $g_0(x)>z$ , so $z-J(z)\le g_0(x)-x\le u_0$ . If $J(z)=E$ , the absence of isolated vertices implies $g_0(E)=M$ ; thus $z=M$ and $z-J(z)=-1\le u_0$ . For the reverse inequality choose a positive $x$ attaining $u_0$ . Such an $x$ exists even when $u_0=0$ , because $g_0(1)\ge1$ then forces $g_0(1)=1$ . For $z=g_0(x)-1$ we have $0\le z<M$ and $J(z)\le x-1$ , hence $z-J(z)\ge g_0(x)-x=u_0$ . Therefore $u_1=u_0+1$ .

Theorem 3.1 supplies compatible nesting, so the cited criterion yields $h(B)=1+u_0$ . Its general lower-bound theorem is being used here; profile duality alone is not a lower-bound proof. The cumulative-sum formula follows from (4). ◻

The upper bound also admits a direct description. Spend all $m=u_0+1$ inspections on one current prefix cohort. If it is not yet captured, a majority step decreases its size by at least one, while a minority step does not increase it, because $u_1=u_0+1$ . Thus it clears after finitely many steps. Clear the other initial cohort next. This proves feasibility without asserting that serial allocation minimizes the time.

For example, the partial-sum scan gives $\begin{array}{c|rrrrrr} B&3\times3&5\times5&3\times3\times3&3\times5\times5 &5\times5\times5&3\times3\times3\times3\\\hline h(B)&2&3&5&8&12&12 \end{array}$ Feasibility therefore needs only the profile scan. Minimum capture time uses the following two-count recurrence.

Define $C(S)=I_0(|S\cap B_0|)\cup I_1(|S\cap B_1|).$ Isoperimetry and nesting imply that $C$ is an idempotent strategy compression. Theorem 3.2 (main) therefore gives an optimal strategy from the full board in which both current-color parts and both survivor parts are prefixes.

A state is the pair $(u,v)$ of counts in the current colors. Choosing survivor counts $0\le i\le u$ and $0\le j\le v$ costs $u+v-i-j$ inspections and gives the exact next state $(u,v)\longrightarrow (g_1(j),g_0(i)).$ (7) The inspection sets are the suffixes $I_0(u)\setminus I_0(i)$ and $I_1(v)\setminus I_1(j)$ . Thus every transition is physically realized, and every unrestricted successful search is matched by a path in this state graph.

For a fixed daily budget $m$ , the optimum is the shortest-path distance from $(E,M)$ to $(0,0)$ , with value infinity when there is no such path. There are $(E+1)(M+1)=O(V^2)$ states. If $u+v\le m$ , one final day captures every possibility. Otherwise, additional inspections cannot hurt, so it suffices to allocate exactly $m$ useful inspections. For $\max(0,m-v)\le p\le\min(m,u),$ the corresponding transition is $(u,v)\longrightarrow \bigl(g_1(v-m+p),\,g_0(u-p)\bigr).$ (8) There are at most $m+1$ transitions per state. Constructing the graph and performing breadth-first search therefore take $O((m+1)V^2)$ operations after constructing the profiles. Recording a shortest path recovers an explicit optimal inspection sequence. A finite optimum is at most $(E+1)(M+1)-1$ , since a shortest path repeats no state. The bounds are polynomial in the number of rooms, rather than in the logarithms of the side lengths.

Equivalently, all budgets can be considered together. Let $W_t(u,v)$ be the smallest daily budget sufficient in at most $t$ days. Then $\begin{aligned} W_0(0,0)&=0,& W_0(u,v)&=\infty\quad((u,v)\ne(0,0)),\notag\\ W_{t+1}(u,v) &=\min_{\substack{0\le i\le u\\0\le j\le v}} \max\bigl\{u+v-i-j,\ W_t(g_1(j),g_0(i))\bigr\}. \end{aligned}$ (9) This exact recurrence includes arbitrary interleaving of the two initial parity cohorts; it makes no serial-allocation assumption.

Remark 3.7. Every weight and lexicographic prefix is a checkerboard corner ideal: a distinct coordinatewise smaller vertex of the same parity has smaller weight. Hence the theorem also proves a corner-ideal normal form for the full-board game on every all-odd box. It does not assert that a global prefix can replace an arbitrary prescribed partial starting set without altering its optimum, and it does not settle boxes with even side lengths. The all-odd-box result gives exact feasibility, minimum time, and strategies through a polynomial recurrence; a uniform closed arithmetic expression for that time is a further question.

Eventual affine periods in odd cylinders

The interior-crossing argument extends to every fixed all-odd cross-section, in every dimension. The first step is an exact finite description of its two end regions; an affine plateau alone would not justify changing the cylinder’s length.

Let $Q$ be a fixed nontrivial box with odd side lengths. Put $W=|Q|,\qquad S=\sum_i(\text{side}_i-1),\qquad Z=W(S+1), \qquad \beta=(W-1)/2.$ Consider $Q\mathbin{\square}P_n$ with odd longitudinal length $n$ . The one-point cross-section gives paths, already classified separately. For $n\ge S+3$ , the longitudinal coordinate is longest and is placed last in the order of Theorem 3.1. Write $H=(Wn+1)/2$ for its majority class size and $g_p^n$ for its exact color- $p$ profile.

Two finite tables describe both ends

For $v\in Q_p$ , let $r_p(v)$ be the rank of $(v,0)$ in the parity order of the infinite prism $Q\times\{0,1,\ldots\}$ . Every such point has weight at most $S$ , so every preceding point has longitudinal coordinate at most $S$ . Its rank is therefore independent of $n$ for $n\ge S+1$ and can be computed in the single finite slab $Q\mathbin{\square}P_{S+1}$ . At most $Z=W(S+1)$ vertices have weight at most $S$ , so $r_p(v)\le Z$ .

Using the transverse cost $a_Q$ from (1), define $U_p(k)=\sum_{\substack{v\in Q_p\\r_p(v)\le k}}a_Q(v), \qquad B_p(k)=\bigl|\{v\in Q_p:r_p(v)\le k\}\bigr|.$ Both tables are constant for $k\ge Z$ .

Lemma 4.1 (Stable corner decomposition). For $n\ge S+3$ and $k>0$ , $g_p^n(k)=k+\mathbf{1}_{\{p=1\}}+U_p(k)-|Q_p|+B_p(H-p-k), \qquad g_p^n(0)=0.$ (10) In particular, every surplus is at most $\beta+p$ , and $k>Z,\quad H-p-k>Z \quad\Longrightarrow\quad g_p^n(k)=k+\beta+p.$ (11)

Proof. The ambient cost $a(x)-1$ equals $a_Q(v)$ on the bottom slice, zero on an interior slice, and $-1$ on the top slice. This includes the origin: its ambient cost minus one is the transverse origin cost. The prefix-cost identity therefore counts the selected bottom weights through $U_p(k)$ and subtracts the number of selected top vertices.

Coordinate complement preserves parity and reverses both weight and lexicographic order. It carries the top slice to the bottom slice. Thus selected top vertices correspond to bottom vertices outside the prefix of size $H-p-k$ , and their number is $|Q_p|-B_p(H-p-k)$ . This proves (10). The empty prefix is separate because the extra origin-neighbor term requires a nonempty odd prefix.

The transverse full-class cost identity gives $U_p(\infty)=|Q_{1-p}|-\mathbf{1}_{\{p=1\}}$ and $B_p(\infty)=|Q_p|$ . Nonnegativity of $a_Q$ gives the asserted upper bound on surplus. Stabilizing both tables gives (11). ◻

The local contribution $a(x)-1$ in a cylinder with $3\times3$ cross-section: transverse costs on the first slice, zero in interior slices, and $-1$ on the last slice. The surplus of a nonempty odd prefix also has the additional $1$ in (10); that term is outside the local sum.

The decomposition gives the stronger identities needed to change length. For two valid majority sizes $H$ and $H+\delta$ , with both longitudinal lengths at least $S+3$ , we have $\begin{aligned} H-p-k>Z&\quad\Longrightarrow\quad g_p^{H+\delta}(k)=g_p^H(k), \\ k>Z&\quad\Longrightarrow\quad g_p^{H+\delta}(k+\delta)=g_p^H(k)+\delta. \end{aligned}$ (12, 13) In the first identity the tail table is full; in the second the bottom weight table is full and the tail argument is unchanged. The first also holds at $k=0$ , since both profiles are zero there. Superscripts now indicate majority size rather than longitudinal length.

An all-odd box has a spanning path whose two endpoints lie in its majority color: traverse successive slices alternately forward and backward and induct on dimension. On that odd path a proper majority $k$ -set has at least $k$ neighbors, by omitting an unselected majority vertex and matching selected vertices toward it from both sides. A nonempty minority $k$ -set has at least $k+1$ neighbors, by its consecutive blocks in the spacing-two path order. The box contains these path edges, so $g_0(k)\ge k\ (k<H),\qquad g_1(k)\ge k+1\ (k>0),\qquad g_0(H)=H-1.$ (14)

Corollary 4.2 (Eventual feasibility threshold). If $H\ge2Z+3$ , then $h(Q\mathbin{\square}P_n)=(W+1)/2$ .

Proof. The size condition implies $n>S+3$ . The majority surplus is at most $\beta$ and attains $\beta$ at $k=Z+1$ by (11). Apply Corollary 3.6. ◻

This is an eventual threshold; shorter cylinders can need fewer inspections. For example, a $5\times5\times5$ box needs twelve, whereas a sufficiently long cylinder with $5\times5$ cross-section needs thirteen.

The period and an explicit threshold

Fix a feasible eventual budget $m\ge\beta+1$ and set $d=2m-W>0,\qquad g=\gcd(W,d),\qquad \Delta=\operatorname{lcm}(W,d)=Wd/g.$ For the explicit threshold define $\begin{aligned} J&=m+1,& A&=Z+1,& R&=\Delta+2J,\notag\\ B&=8Z+6d+2,& L&=Z+m+1,& \mathcal{E}&=B+4L(B+1),\notag\\ H_*&=R+2A+4J+2+2\mathcal{E}(R+2J+1). \end{aligned}$ (15)

Theorem 4.3 (Eventual affine period under the preceding profile hypotheses). For every odd $n$ with $(Wn+1)/2\ge H_*$ , $T_m(Q\mathbin{\square}P_{n+2d/g}) =T_m(Q\mathbin{\square}P_n)+4W/g.$ (16) At the eventual minimum budget $m=(W+1)/2$ , increasing a sufficiently large odd length by two increases the optimal time by exactly $4W$ .

The threshold is not intended to be sharp. The proof uses the profile bounds, plateau and stable translations just proved, together with connectedness.

A potential with a bounded total deficit

For $n\ge S+3$ , write $H=(Wn+1)/2$ and $M=H-1$ . Define $K=2Z+2m+1,\qquad \Gamma=\left(2H-4Z-2m-5\right)_+,\qquad F_p(k)=\min\{\Gamma,\left(2k+p-K\right)_+\}.$

Lemma 4.4 (Uniform potential and time bounds). For $0\le r\le m$ , $F_p(k)-F_{1-p}\bigl(g_p(\left(k-r\right)_+)\bigr) \le\left(2r-W\right)_+.$ (17) Consequently $\left\lceil 2\Gamma/d\right\rceil\le T_m(Q\mathbin{\square}P_n) \le4\left\lceil\left(M-m\right)_+/d\right\rceil+2.$ (18)

Proof. The potential inequality is trivial if $\Gamma=0$ . Otherwise let $q=\left(k-r\right)_+$ and $j=g_p(q)$ . If $q\le Z$ , then $k\le Z+m$ and $2k+p-K\le0$ , so the current potential is zero. If $q\ge H-Z-1$ , then $j\ge q-1\ge H-Z-2$ , and $2j+(1-p)-K\ge2H-2Z-4-K=\Gamma.$ The successor potential is therefore $\Gamma$ . In the remaining region both profiles are on their plateaus, so $j=k-r+\beta+p$ . The difference of the unclipped affine expressions is $2r-W$ . Common monotone, $1$ -Lipschitz clipping proves (17).

For two quota shares $r,m-r$ , the right sides sum to at most $d=2m-W$ . Both full color classes have potential $\Gamma$ , giving the lower bound by summing daily decreases. For the upper bound, start with the minority cohort of size $M$ . Each pair of full-budget days reduces an uncleared cohort by at least $d$ . Thus $2\left\lceil\left(M-m\right)_+/d\right\rceil+1$ days suffice. Pad early clearing to this fixed odd phase length. The other initial cohort remains its full current color class and, after the odd phase, is also in the minority color with size $M$ . Repeat the phase to obtain the upper bound. ◻

For a rectangle $Q=P_w$ , $w=2b+1$ , the explicit profiles of Theorem 5.1 permit the sharper corner radius $Z=b^2$ in the preceding argument. At minimum budget, strengthen its potential slightly as follows, for every odd $n\ge w$ . Take $K=2b^2+2b+2$ and $\Gamma=\left(2H-4b^2-2b-6\right)_+$ . In the low region the current potential is zero for $r<m$ and at most one for $r=m$ ; the high-region and plateau arguments are unchanged. This gives the useful uniform estimate $\max\{0,\,2wn-2w^2+2w-10\} \le T_{(w+1)/2}(P_w\mathbin{\square}P_n) \le2wn-2w-2.$ (19) Thus its leading term is $2wn$ for every fixed odd width, independently of whether a sharper correction has been determined.

Return to the preceding cylinder family, with $Z=W(S+1)$ and the potential of Lemma 4.4. Assume $H\ge H_*$ , so $\Gamma>0$ and $M>m$ . Fix an optimal prefix strategy, using padded full quotas as in Section 2. Let $\Phi_t$ be the sum of its two current-color potentials and put $\eta_t=d-(\Phi_t-\Phi_{t+1})\ge0.$ These are integers, and the upper bound in (18) gives $\sum_t\eta_t=dT_m-2\Gamma\le8Z+6d+2=B.$ (20) Here $d\left\lceil(M-m)/d\right\rceil\le M-m+d-1$ accounts for the rounding. Call a day efficient if $\eta_t=0$ , and bad otherwise. There are at most $B$ bad days.

An efficient day gives all $m$ inspections to one cohort. Indeed, if both positive-part losses in (17) are positive, their sum is $d-W<d$ . If only one is positive but neither share is $m$ , it is at most $d-2$ . Thus on an efficient day the active cohort loses exactly $d$ potential and the inactive cohort’s potential remains exactly constant.

From flat potentials to empty or full cohorts

Zero inspections strictly increase every intermediate potential: $0<F_p(k)<\Gamma \quad\Longrightarrow\quad F_{1-p}(g_p(k))>F_p(k).$ (21) For a proper majority prefix, $g_0(k)\ge k$ , so its unclipped expression increases by at least one after the color reversal. A full majority prefix has potential $\Gamma$ and is excluded. For a nonempty minority prefix, $g_1(k)\ge k+1$ , giving the same conclusion. Clipping preserves strict growth while the old value is below $\Gamma$ .

After an active cohort loses $d$ on an efficient day, its potential is strictly below $\Gamma$ . If it is still positive, (21) forces it to stay active on the next efficient day. A switch is possible only when its potential reaches zero. It cannot become active again in the same efficient run, since zero cannot lose $d$ and its inactive value must stay constant. Hence each consecutive efficient run has at most two focused blocks, and there are at most $2(B+1)$ such blocks in total.

Call a day clean when all $m$ inspections target one cohort and the other cohort is actually empty or actually its full current color class. Flat potential alone is insufficient for this conclusion. We now bound the transient days needed to reach actual emptiness or fullness.

If a nonempty proper support $X$ lies in one color of a connected bipartite graph without isolated vertices, then $X\subsetneq N^2(X)$ . Inclusion follows by backtracking along an edge. Equality would make $X$ closed under two-step paths; connectivity makes the two-step graph connected within each color and would force $X$ to be full. Therefore an uninspected nonempty proper prefix grows by at least one every two days until it is full.

During an efficient focused block the inactive potential is constantly zero or $\Gamma$ . At zero, its count is at most $Z+m=L-1$ ; if nonempty, it cannot remain in that range for more than $2L$ days. At $\Gamma$ , its count is at least $H-Z-2$ , hence within $L$ of its full class; it becomes full within $2L$ days. Empty and full cohorts remain so under further uninspected moves. Each efficient block therefore contributes at most $2L$ nonclean days. Counting all bad days as well, the entire optimal search has at most $\mathcal{E}=B+4L(B+1)$ (22) nonclean days.

A protected band and its two individual cuts

Every one-day count change has absolute value at most $J=m+1$ : profile surplus is between $-1$ and $\beta+1$ , and each quota is at most $m$ . Record both source counts from each nonclean day. A count $k$ forbids integer cuts $c$ with $k\in[c-J,c+R+J]$ , at most $R+2J+1$ cuts. There are at most $2\mathcal{E}$ records. Restrict candidate cuts to $A+2J\le c\le H-R-A-2J-2.$ (23) There are $H-R-2A-4J-1$ candidates. By (15), this exceeds $2\mathcal{E}(R+2J+1)$ . Choose a cut forbidden by no record.

No nonclean transition can touch the protected interval $[c,c+R]$ . A cohort in that interval is therefore active on every day, receiving all $m$ inspections; an inactive clean cohort is empty or full, both outside the interval. Its count never increases. Nor can it cross the interval upwards: a nonclean transition cannot touch it, and a clean active transition does not increase. Both cohorts begin above and finish below the interval.

For each initial cohort $i$ , choose its first count $x_i$ at most $c+\Delta+J$ . The previous count is larger, so the displacement bound gives $c+\Delta<x_i\le c+\Delta+J.$ (24) The entire protected interval is inside the profile plateaus, including all relevant survivors. A full-budget step there sends $k$ to $k-m+\beta+p$ , so every pair of days reduces its count by exactly $d$ and restores its color. The next $\tau=2\Delta/d$ days therefore take $x_i$ to $x_i-\Delta\in(c,c+J]$ . This duration is even, and the trajectory stays in the protected band. Throughout the block its inactive companion remains empty or full. The two crossing blocks cannot overlap.

Define the individual endpoints $\ell_i=x_i-\Delta,\qquad u_i=x_i.$ They need not agree for the two cohorts. This avoids an otherwise real residue problem: when $d>1$ , a trajectory may skip a prescribed count, and the two cohorts need not have matching residues. One common protected band supplies two legitimate individual cuts. Every visit to $(\ell_i,u_i)$ belongs to the chosen crossing block, because active clean trajectories are nonincreasing and nonclean transitions cannot touch the larger band. Boundary stalls at the minimum budget are harmless; the even block duration preserves the needed phase.

Removing and enlarging the crossing blocks

Proof of Theorem 4.3. First contract the majority size from $H$ to $H-\Delta$ and delete both crossing blocks of length $\tau$ . At each remaining state transform initial cohort $i$ by $f_i(k)= \begin{cases} k,&k\le\ell_i,\\ k-\Delta,&k\ge u_i. \end{cases}$ No retained state lies strictly between these cases. At the ends of a deleted block, $u_i$ and $\ell_i$ both map to $\ell_i$ . Its inactive companion is empty or full at both ends; a full class maps to the contracted full class. Since $\tau$ is even, the color labels also match. The two state paths therefore glue.

For a low retained source, its survivor is at most $\ell_i$ . The contracted far-distance satisfies $(H-\Delta)-\ell_i=H-u_i \ge H-(c+R)\ge A+2J+2,$ so the low profile identity (12) applies. Its successor cannot enter the removed interval, by the protected-band argument. For a high retained source, the contracted survivor is at least $\ell_i-m>c-m>Z.$ The stable upper profile identity (13) therefore gives $g_p^H(q+\Delta)=g_p^{H-\Delta}(q)+\Delta.$ These identities verify every retained transition. Quotas remain within the same budget, and unused quota may be wasted. The result is a physical prefix search on length $n-2\Delta/W$ . Its majority size is at least $H_*-\Delta\ge2Z+6J+4$ , so its length exceeds $4(S+1)$ and the longitudinal coordinate remains longest. Thus all stable profile identities still apply. The resulting search is completed in $T_m(Q\mathbin{\square}P_n)-4\Delta/d$ days. Hence $T_m(Q\mathbin{\square}P_{n-2\Delta/W}) \le T_m(Q\mathbin{\square}P_n)-4\Delta/d.$ (25)

Conversely, start with an optimal search on any $H\ge H_*$ and its protected blocks. Enlarge $H$ to $H+\Delta$ . Keep lower counts at or below $\ell_i$ unchanged and increase upper counts at or above $u_i$ by $\Delta$ . Replace each block from $u_i$ to $\ell_i$ by a clean block from $u_i+\Delta$ to $\ell_i$ , lasting $4\Delta/d$ days. The affine profiles realize this trajectory explicitly, with the inactive companion empty or the enlarged full class. The extra $\tau$ days per block are even. The same low and high identities verify every other transition. Thus $T_m(Q\mathbin{\square}P_{n+2\Delta/W}) \le T_m(Q\mathbin{\square}P_n)+4\Delta/d.$ Apply (25) at $H+\Delta$ for the reverse inequality. Since $\Delta/W=d/g$ and $\Delta/d=W/g$ , this proves (16). ◻

Let $n_0$ be the least odd length at or beyond the threshold. For each of the $d/g$ odd residue classes modulo $2d/g$ , the exact two-count recurrence determines the optimum and an optimal strategy at one of $n_0,n_0+2,\ldots,n_0+2d/g-2.$ The theorem then determines every later time in that class and constructs its optimal strategy by insertion. In particular, $T_m(Q\mathbin{\square}P_n)=\frac{2W}{2m-W}\,n+O_{Q,m}(1).$ At the eventual minimum budget there is one offset $C(Q)$ , with $T_{(W+1)/2}(Q\mathbin{\square}P_n)=2Wn-C(Q)$ for every sufficiently large odd $n$ . The offset can depend on the transverse shape, not only on its number of rooms. For rectangular cross-sections $Q=P_w$ , the stronger bounds in (19) give $2w+2\le C(w)\le2w^2-2w+10$ . The offset recurrence and its parameter-dependent finite initialization are not a fixed-size numerical expression. Their reduction remains part of the rectangle objective when $Q=P_w$ .

An exact three-dimensional family

For one cross-section the finite corner calculation gives the optimum from the shortest nontrivial cylinder, without the conservative threshold in Theorem 4.3.

Theorem 4.5. For every odd $n\ge3$ , five inspections per day are necessary and sufficient on $P_3\mathbin{\square}P_3\mathbin{\square}P_n$ , and $T_5(P_3\mathbin{\square}P_3\mathbin{\square}P_n)=18n-36.$

Proof. Put $H=(9n+1)/2$ . For $Q=P_3\mathbin{\square}P_3$ , the ranks of bottom-slice vertices in their respective parity orders, and their transverse costs, are $\begin{array}{c|l|l} p&\text{ranks}&\text{costs}\\\hline 0&(1,2,3,5,8)&(2,1,1,0,0)\\ 1&(1,2,4,6)&(2,1,1,0). \end{array}$ These ranks already stabilize at $n=3$ . The last even bottom point $(2,2,0)$ is first in weight layer four, and its earlier even layers have longitudinal coordinate at most two. The last odd bottom point $(1,2,0)$ is sixth in its parity order: its predecessors are the three unit vectors and $(2,1,0),(2,0,1)$ . Enlarging the longitudinal path therefore introduces no earlier point in either list.

Let $U_p(k)$ be the cumulative listed cost through rank $k$ , and let $B_p(k)$ count the listed ranks at most $k$ . The cost and complement argument of Lemma 4.1 gives, for $k>0$ , $g_0(k)=k+U_0(k)-5+B_0(H-k),\qquad g_1(k)=k+1+U_1(k)-4+B_1(H-1-k),$ with $g_0(0)=g_1(0)=0$ . Thus the corner radius is eight, and the central profiles are $k+4$ and $k+5$ . The majority surplus is at most four and equals four at $k=3$ : $U_0(3)=4$ and $B_0(H-3)=5$ for every $H\ge14$ . Corollary 3.6 gives the minimum budget five.

For the exact time use the identical charge sequences $c_0=c_1=(0,0,\tfrac13,\tfrac23,1,1).$ They satisfy the daily charge bound (113) (main). The rational shortest-charge potentials described in the preceding section are checked against every transition $F_p(k)-F_{1-p}\bigl(g_p(\max\{k-r,0\})\bigr)\le c_p(r), \qquad 0\le r\le5.$ Together with a minority-first serial strategy, the five finite certificates give $\begin{array}{c|rrrrr} n&3&5&7&9&11\\\hline F_0(H)+F_1(H-1)&18&54&90&126&162\\ \text{strategy length}&18&54&90&126&162. \end{array}$ Here the strategy spends all available inspections on the first cohort until it is captured, uses any remaining inspections on its finishing day on the second cohort, and then finishes that cohort. The finite verifier checks the physical room neighborhoods and replays these inspection sets, as well as checking all 1,950 rational inequalities.

At the base $n=11$ , take $H=50$ , $c=25$ , and $D=6$ . The exact arrays satisfy $F_p(k)=2k-14+p\qquad(13\le k\le37).$ This is the full collar $[c-2D,c+2D]$ , and $c\ge8+2D$ , $H-c\ge8+2D+2$ . Both active cohorts visit count 25. At the first visit the other cohort is full, since $25>5$ places the visit before the first cohort’s finishing day. At the second visit the first cohort is empty.

Consequently Lemmas 22.1 (main) and 22.2 (main), in their compatible-profile formulation, apply with corner radius eight. Increasing $H$ by $\Delta$ inserts an affine interval in each potential and raises their initial sum by $4\Delta$ . Inserting $2\Delta$ full-budget days at each serial cut realizes the same increase in time. Each pair of inserted days reduces the active count by one and restores its color, while the other cohort stays full or empty. All remaining transitions follow the stable low and translated high profiles above.

For every odd $n\ge11$ , choose $\Delta=9(n-11)/2$ . The matching bounds are then $162+4\Delta=18n-36$ . The finite certificates cover the smaller odd lengths, completing the proof. ◻

The exact verifier and receipt are included in the companion artifact:

src/three_by_three_cylinder_time.py
research/three-by-three-cylinder-time.json

The receipt stores the corner tables, charges, finite values, and complete base potential arrays. An independent verifier also checked actual room neighborhoods and schedules at seven lengths, including 13 and 31. These checks establish the finite premises of the insertion proof. The variable-length theorem is an ordinary proof with exact rational certificates; it is not claimed here as a complete physical Lean theorem.

Higher-dimensional boxes

The preceding compression theorems work in arbitrary dimension, but do not by themselves provide a closed time formula for every box. We give two unbounded applications and a fully certified three-dimensional example.

A side of length two

Let $H$ be bipartite, with color function $\chi$ , and put $G=H\mathbin{\square}P_2$ . In either color class of $G$ , there is exactly one vertex above each vertex $v$ of $H$ : its second coordinate is $s-\chi(v)$ modulo two. Under this identification, $\pi(N_G(R))=\pi(R)\cup N_H(\pi(R)).$ The vertical move preserves the projection, and an $H$ -move changes it to an $H$ -neighbor. This proves the equality for arbitrary sets, including boundary and empty sets.

Suppose $H$ has an order with prefixes $I_k$ such that every $k$ -set has at least $c(k)$ vertices in its closed neighborhood and $I_k\cup N_H(I_k)=I_{c(k)}$ . Put $A=|H|$ . The two initial-color cohorts then have the exact state transition $(a,b)\longmapsto \bigl(c(\max\{a-p,0\}),c(\max\{b-m+p,0\})\bigr), \qquad 0\le p\le m,$ (26) starting at $(A,A)$ . A state is capturable on the current day exactly when $a+b\le m$ . Tail inspections of the prefixes attain each step. Conversely the cardinalities in every unrestricted search dominate these counters when the same allocations are used. Thus shortest-path search on $(A+1)^2$ states returns both the exact time and an actual optimal strategy, using $O((m+1)(A+1)^2)$ transitions after the profile is known.

Theorem 5.1. Under the preceding closed-neighborhood nesting hypothesis, $h(H\mathbin{\square}P_2)=1+\max_{0\le k\le A}(c(k)-k).$ Both this feasibility formula and recurrence (26) apply to every Cartesian box having a side of length two.

Proof. Write $B=\max_k(c(k)-k)$ . If $m\le B$ , select $k$ with $c(k)\ge k+m$ . A cohort of size at least $k+m$ retains at least $k$ possible positions after inspection and has at least $k+m$ after movement. Initially $A\ge k+m$ . Since $k>0$ , the invariant prevents capture forever. If $m>B$ , a canonical cohort of size $b>m$ has next size at most $b-m+B<b$ . Clear it, then clear the other cohort in the same way; the untouched projected cohort stays full.

For Cartesian $H$ , omit length-one factors, list the other side lengths in increasing order, and order vertices by increasing coordinate sum, breaking a tie by putting the larger first differing coordinate first. The classical simplicial isoperimetric theorem gives exactly the closed- neighborhood nesting hypothesis. We use the statement and definitions in Otachi–Suda (Otachi and Suda 2011, Theorem 2.5), where the result is attributed to Moghadam and Bollobás–Leader. For the one-vertex empty product take $c(0)=0,c(1)=1$ . ◻

For $a,b\ge2$ , the vertex boundary width of $P_a\mathbin{\square}P_b$ is $\min(a,b)$ , so $h(P_a\mathbin{\square}P_b\mathbin{\square}P_2)=\min(a,b)+1$ . If exactly one of $a,b$ is one, the remaining nontrivial ladder has threshold two; if both are one, it is a single edge with threshold one. The theorem also covers all hypercubes. Its input is a classical closed-neighborhood theorem; it does not assert open-neighborhood nesting on arbitrary even rectangles.

Exact profile transfer for either longitudinal parity

There is a useful further recurrence even when global minimizing prefixes are unavailable. Let a bipartite transverse graph $Q$ have compatible minimizing parity orders with profiles $g_0,g_1$ . For a one-color support in $Q\mathbin{\square}P_n$ , let $k_j$ be its size in column $j=0,\ldots,n-1$ , and let $p$ be its global color.

Proposition 5.2. For each prescribed column-count vector, the exact minimum neighborhood size is $\sum_{j=0}^{n-1} \max\{g_{(p+j)\bmod2}(k_j),k_{j-1},k_{j+1}\}, \qquad k_{-1}=k_n=0.$ This holds for every positive $n$ , including even $n$ .

Proof. In column $j$ , the neighborhood is the union of the transverse neighborhood of that column and the supports in the two adjacent columns. Its size is at least the displayed maximum. Replace every column support by the corresponding transverse prefix. All three sets are now prefixes of the same opposite color order, and their union has size exactly the maximum. These replacements attain all column minima simultaneously. ◻

Minimize the sum over vectors with $\sum k_j=k$ to obtain the exact global cardinality profile. A transfer state remembers the previous count $a$ , current count $b$ , and cumulative count. Appending $c$ charges $\max\{g(b),a,c\}$ and replaces the pair by $(b,c)$ . Zero counts at the two outside columns give the boundary conditions. Writing $W=|Q|$ , this direct recurrence uses $O(n^2W^4)$ arithmetic operations and $O(nW^3)$ memory once the transverse profiles are known. It applies in particular to every all-odd cross-section.

This computes exact neighborhood minima, not compatible global orders. The minimizing vector can depend on $k$ without being nested. A search using only these cardinality profiles therefore supplies a lower time bound; it is not asserted to attain that bound on arbitrary even cylinders. The accompanying code checks the recurrence against all $524\,288$ one-color supports of the $3\times3\times4$ box.

The finite $3\times3\times4$ check as a corollary

Proposition 5.3. On $P_3\mathbin{\square}P_3\mathbin{\square}P_4$ , the optimal capture time with five inspections per day is $36$ .

Proof. This is $n=4$ in the all-length theorem 5.5: $18n-36=36$ . ◻

An independent finite verification remains available. Slice compression reduces the physical game to eight counts; exhaustive breadth-first search first leaves at most five rooms after 35 movements. It checks 1,109,364 transitions and discovers 2,017 states. A separately implemented physical-neighborhood search obtains the same layers and optimum, and its saved 36-day schedule replays on the actual room graph. The complete recurrence and verifier are in src/three_by_three_by_four_exact.py, with receipt and witness in research/three-by-three-by-four-exact.json. This supplies an independent finite check of the general theorem; repeating its full finite proof is unnecessary. It is not a complete physical Lean theorem.

Two complete examples with even sides

The distinction between a minimum neighborhood size and a sequence of compatible minimizing shapes is visible even on small cubes. The following two tables are exact ordinary computer-assisted theorems. Their lower certificates and physical schedules have been checked by a second implementation, independently of the search that found them.

Theorem 5.4. The minimum capture times on $P_4^3$ and $P_3\mathbin{\square}P_4^2$ are as follows.

$4\times4\times4$		$3\times4\times4$
Daily budget	Minimum days	Daily budget	Minimum days
$0$ – $7$	$\infty$	$0$ – $6$	$\infty$
$8$	$40$	$7$	$20$
$9$	$20$	$8$	$14$
$10$	$16$	$9$	$11$
$11$	$12$	$10$	$8$
$12$	$10$	$11$	$7$
$13$ – $14$	$8$	$12$ – $13$	$6$
$15$	$7$	$14$	$5$
$16$ – $17$	$6$	$15$ – $19$	$4$
$18$	$5$	$20$ – $23$	$3$
$19$ – $25$	$4$	$24$ – $47$	$2$
$26$ – $31$	$3$	$48$ or more	$1$
$32$ – $63$	$2$
$64$ or more	$1$

Proof. Apply Theorem 2.1 to every equal-length pair, and also compress the length-three coordinate in the second box. The one-color fixed families contain respectively $292$ and $1936$ sets per color. These families are enumerated without a geometric guess: order vertices by increasing $\sum_i i x_i$ , and either omit each vertex or include it when all its legal predecessors are already present. The predecessor moves are (2.1), together with $x\mapsto x-2e_i$ on an odd axis. This recursively enumerates every ideal exactly once. Direct physical neighborhoods preserve the fixed families.

Minimizing $|N(R)|$ at each cardinality in these families gives the exact unrestricted one-color neighborhood profiles, by compression. They give an impossibility trap below budgets eight and seven, respectively. On the four-cube the profile is the same in both colors and is $\begin{split} g={}&(0,3,6,7,9,11,12,13,15,16,17,18,19,19,21,22,23,\\ &24,25,25,26,27,28,28,29,29,30,31,31,31,32,32,32). \end{split}$ For example, a cohort of size at least $21$ retains at least $14$ rooms after seven inspections, and then has at least $g(14)=21$ positions again.

The two-count lower relaxation formed from the exact profiles gives every listed finite lower bound except at budget eight in either box. To verify this statement, enumerate all count pairs, all quota splits, and successive sets of pairs that can reach capture. This calculation is the same monotone finite recurrence used for the three-cube above. Actual room-coordinate schedules attain every listed bound; the verifier updates the complete physical belief set after each inspection and movement. Budget monotonicity extends endpoint schedules across each displayed range.

The two exceptional lower bounds have short certificate descriptions. For each fixed one-color set $A$ let $F(A)$ be the nonnegative integer in the accompanying table. For every fixed survivor $R\subseteq A$ , put $p=|A|-|R|$ . At budget eight the tables satisfy $F(A)\le c(p)+F(N(R)),\qquad 0\le p\le8, \qquad F(\varnothing)=0.$ (27) On $P_4^3$ , the charges at $p=0,\ldots,8$ are $(0,0,0,0,1,2,2,2,2)$ ; both full-color potentials are $40$ . Two allocations totaling at most eight have total charge at most two. Telescoping (27) therefore gives $T_8\ge(40+40)/2=40$ . There are $29\,686$ inequalities to check. An attaining prefix sweep for each cohort has sizes $\begin{split} &32,29,27,25,24,23,22,22,21,21,19,19,\\ &18,18,17,16,15,13,11,8,0. \end{split}$ Each sweep takes twenty days; reflection in an even axis gives the favorable starting phase for the second cohort.

On $P_3\mathbin{\square}P_4^2$ , take $c(p)=p$ and full-color potential $54$ . The $654\,570$ inequalities give $T_8\ge\left\lceil 108/8\right\rceil=14$ , attained by the stored physical schedule. These certificate checks require only integer inequalities and direct finite neighborhoods. They do not trust the shortest-path procedure that generated the potential tables.

Finally, both boxes have a perfect matching. Its disjoint alternating trajectories require at least half the volume in two days; two successive inspections of one full color attain that threshold. One-day capture requires the entire volume. This proves the remaining endpoint ranges. ◻

The independent verifier is src/even_cube_resumed_independent_review.py; complete certificates, room schedules, and review receipts are in the corresponding research/even-resume-* files in the research archive. At eight probes the four-cube’s cardinality relaxation predicts only $32$ days, compared with the true $40$ ; on $3\times4\times4$ it predicts $12$ instead of $14$ . Thus exact neighborhood profiles alone need not determine exact capture times. The shape information retained by the compression is mathematically necessary for these lower arguments.

The complete $3\times3\times3$ example

Encode a room $(x,y,z)\in\{0,1,2\}^3$ by $9x+3y+z$ . Its color is $x+y+z$ modulo two. The two classes have sizes $14,13$ . Their minimum open-neighborhood sizes are the following; a dash indicates a source cardinality larger than the class.

The three-cube drawn as three layers. Adjacent rooms in a layer are connected; rooms at the same position in consecutive layers are also connected. Shading marks the first five inspections of the schedule.

$k$	0	1	2	3	4	5	6	7	8	9	10	11	12	13	14
$g_E(k)$	0	3	5	7	8	9	10	10	11	12	12	13	13	13	13
$g_O(k)$	0	4	6	7	9	10	11	12	12	13	13	14	14	14	–

Here is a finite certificate procedure for the table. For each color, list its vertices; recursively either include or exclude the next vertex, maintaining the selected count $k$ and the union $U$ of its physical neighbor sets. At every leaf check $|U|\ge g(k)$ . This has $2^{14}+2^{13}=24\,576$ leaves. The generic recursion is proved sound in Lean before the concrete finite check is kernel evaluated. Prefixes in increasing coordinate sum with decreasing lexicographic tie breaking attain the values. Neither the lower bound nor the formal classification assumes that an arbitrary search uses these prefixes.

For a fixed budget define the relaxed count successor $f_p(a,b)=\bigl(g_O(\max\{b-m+p,0\}), g_E(\max\{a-p,0\})\bigr).$ All arbitrary physical successors dominate one of these. The finite calculation below independently specifies the time lower bounds. It uses just $15\cdot14=210$ count pairs; $W_t$ denotes relaxed states that can reach zero in at most $t$ inspection rounds.

W = {(0, 0)}
for t = 1, 2, ...:
    Wnext = W union {(a,b): 0<=a<=14, 0<=b<=13,
                   f_p(a,b) belongs to W for some 0<=p<=m}
    if (14,13) belongs to Wnext: return t
    if Wnext == W: return infinity
    W = Wnext

The required lower endpoint checks are $18,10,6,4,3$ at budgets $5,6,8,11,12$ , respectively. In Lean the corresponding distance potentials are stored as finite integers and checked to be nondecreasing in both counts, zero at zero, and to drop by at most one under every relaxed transition. This proves the lower bound without trusting the search routine that found the potentials. For budgets at most four, there is a shorter proof: every same-color triple has at least seven neighbors, so a cohort of at least seven positions can never fall below seven after four inspections and movement.

For clarity, explicit upper schedules are given next. Each row is a sequence of daily inspection sets; a superscript $\times2$ means repeat the entire listed sequence twice. The physical update $B\leftarrow N(B\setminus S)$ , starting from all $27$ rooms, verifies every schedule directly.

$m$	Inspection sets in order
5	$\bigl(\{1,3,5,9,11\},\{4,6,10,12,18\},\{5,7,11,13,15\},$ $\{8,10,12,14,16\},\{9,11,13,15,17\},\{10,12,14,16,18\},$ $\{11,13,15,19,21\},\{8,14,16,20,22\},\{15,17,21,23,25\}\bigr)^{\times2}$
6	$\bigl(\{8,14,16,20,22,26\},\{5,7,11,13,19,25\},$ $\{2,4,10,16,22,24\},\{1,7,13,15,19,21\},$ $\{0,4,6,10,12,18\}\bigr)^{\times2}$
7	$\bigl(\{8,14,16,20,22,24,26\},\{5,7,11,13,15,19,21\},$ $\{0,2,4,6,10,12,18\}\bigr)^{\times2}$
9	$\{2,4,8,14,16,20,22,24,26\},\{1,3,7,9,11,13,15,19,21\},$ $\{5,7,11,13,15,17,19,23,25\},\{0,2,4,6,10,12,18,22,24\}$
12	$\{2,4,6,8,10,12,14,16,20,22,24,26\},$ $\{1,3,8,9,14,16,19,20,21,22,24,26\},$ $\{1,3,5,7,9,11,13,15,19,21\}$
13	All odd-numbered rooms, on each of two consecutive days.

Larger budgets inherit these schedules. Fewer than $27$ probes cannot capture every possible initial room in one day, and $27$ can. We have therefore proved the complete table recorded in the companion introduction. Its geometry, finite inequalities, physical schedules, and interpretation as capture of every actual target walk are all checked in Lean.

The exact five-inspection time on every $3\times3\times n$ cylinder

Theorem 5.5. For every $n\ge3$ , $T_5(P_3\mathbin{\square}P_3\mathbin{\square}P_n)=18n-36.$ The proof combines an explicit physical sweep with an ordinary lower certificate for arbitrary supports. The new even-length argument is not presently a complete physical Lean theorem.

The odd case is Theorem 4.5. Assume $n=2L\ge4$ and put $h=9L$ . Both checkerboard classes have $h$ rooms. The compatible transverse $3\times3$ profiles are $G_0=(0,2,3,4,4,4),\qquad G_1=(0,3,4,5,5).$ Compress every transverse slice to its parity prefix. This operator $C$ is monotone and cardinality preserving, and satisfies $N(CS)\subseteq C(NS)$ by the fiber-compression theorem. For a compressed phase- $p$ set with slice counts $k_j$ , its exact neighborhood count in slice $j$ is $\max\{G_{(p+j)\bmod2}(k_j),k_{j-1},k_{j+1}\}, \qquad k_{-1}=k_n=0.$ We first establish a sharp obstruction to consecutive small boundaries.

A finite word certificate for every even length

For phase zero, pair consecutive counts into letters $(a,b)$ with $0\le a\le5$ , $0\le b\le4$ . Give a letter the cost $v(a,b)=\max\{G_0(a),b\}-a+\max\{G_1(b),a\}-b,$ and consecutive letters $s=(a,b)$ , $t=(c,d)$ the edge cost $\begin{aligned} e(s,t)={}&\max\{G_1(b),a,c\}-\max\{G_1(b),a\}\\ &+\max\{G_0(c),d,b\}-\max\{G_0(c),d\}. \end{aligned}$ The neighborhood surplus is exactly $\sum_i v(s_i)+\sum_{i<L-1}e(s_i,s_{i+1})$ ; no outside edge is added. Every edge cost is nonnegative. The vertex costs are the following nonnegative matrix, with rows $a=0,\ldots,5$ and columns $b=0,\ldots,4$ : $\begin{pmatrix} 0&3&4&5&5\\2&3&3&4&4\\3&3&3&3&3\\ 4&3&3&3&2\\4&3&2&2&1\\4&3&2&1&0 \end{pmatrix}.$ Thus a word of surplus at most four has no prefix of larger cost.

Here is the entire finite certificate specification. A state records its last letter, cost at most four, occupied count capped at four, omitted count capped at eight, whether its first $a\ge3$ , and length capped at two. Initialize with every one-letter word of cost at most four. Appending $t=(c,d)$ adds $v(t)+e(s,t)$ to the cost, $c+d$ to the occupied count, and $9-c-d$ to the omitted count; saturate the two counts, preserve the first-letter flag, and cap length at two. Discard costs above four. Finite closure gives exactly 113 states and 346 edges. Every terminal state of capped length two satisfies:

Its cost is at least zero if either capped count is zero, and otherwise at least $\min\{4,K+1,\left\lfloor(D+2)/2\right\rfloor\}$ , where $K,D$ are its two capped counts.
If its cost is four, $K=4$ , and $D=8$ , its first $a\ge3$ and its last letter is $(a,0)$ with $a\le2$ .

These are finite integer checks of the stated initialization and transition rule, supplied in the accompanying certificate. Induction on word length makes them valid for every $L\ge2$ ; costs above four trivially satisfy the first bound. Reflection in the even longitudinal side exchanges the colors, giving phase one too.

Consequently every monochromatic set of size $k$ has at least $g_h(k)$ neighbors, where $g_h(0)=0,\quad g_h(h)=h,\quad g_h(k)=k+\min\{4,k+1,\left\lfloor(h-k+2)/2\right\rfloor\}\quad(0<k<h).$ (28) Compression transports this bound to arbitrary supports. Call a survivor critical if its surplus is four and $4\le k\le h-8$ . A compressed phase-zero critical set has at most two neighbors in the last slice, whereas every compressed phase-one critical set contains at least three rooms in that slice. Hence consecutive compressed critical survivors are impossible. For arbitrary critical $R$ , (28) forces $|N(CR)|=|N(R)|=|R|+4$ . The compression inclusion therefore becomes $N(CR)=C(NR)$ . If a second critical $S$ lay in $N(R)$ , monotonicity would give $CS\subseteq C(NR)=N(CR)$ , the same contradiction. This proves the obstruction for arbitrary consecutive survivors.

A two-component integer potential

Let $e\in\{0,1\}$ record whether the previous survivor was critical, starting with $e=0$ . A marked count satisfies $8\le k\le h-4$ , and the obstruction forbids $e=e'=1$ . Use charges $c(0),\ldots,c(5)=(0,0,1,2,3,3), \qquad c(p)+c(q)\le3\quad\text{if }p+q\le5.$ Define $\begin{aligned} P_0(k)&=(0,0,1,2,3,3,5,6,9)[k],&&0\le k\le8,\\ P_0(k)&=\min\{6k-42,3k+3h-51,6h-54\},&&k\ge9,\\ P_1(k)&=6k-39,&&8\le k\le h-4. \end{aligned}$ Both functions are nondecreasing in their valid count domains. For every one-cohort step with useful allocation $p\le5$ , $P_e(k)\le c(p)+P_{e'}(k').$ (29) To specify its complete check, put $s=k-p$ . At $s=0$ the only output is $(0,0)$ . If $4\le s\le h-8$ , the minimum marked output is $(s+4,1)$ and the minimum unmarked output is $(s+5,0)$ ; the former is forbidden when $e=1$ . Outside this interval the output is unmarked with count at least $g_h(s)$ . Monotonicity handles every larger actual neighborhood. These cases include all geometric outputs.

For $h=18,27,36,45$ , substitution checks respectively 183, 345, 507, and 669 inequalities, using integers only. The following three cases prove every larger parameter, so this finite verification is not an extrapolation. Write $h=45+\Delta$ , $\Delta\ge0$ . If $k\le17$ , every minimum output is at most 22 and the base inequality is unchanged. If $k\ge27+\Delta$ , subtract $\Delta$ from source and output counts: the residual is at least $22+\Delta$ , and all profiles, history endpoints, and potentials translate exactly, the latter by $6\Delta$ . Finally, if $18\le k\le26+\Delta$ , the residual lies in $[13,26+\Delta]\subseteq[4,h-8]$ , and source and minimum output are in the affine region $P_e(k)=6k-42+3e$ . The possible drops are $6p-27$ for $0\to1$ or $1\to0$ , and $6p-30$ for $0\to0$ ; each is at most $c(p)$ . This proves (29) for every $h\ge45$ . The four bases cover all remaining physical half-sizes $h=9n/2$ .

Both initial potentials are $P_0(h)=6h-54$ , and both terminal potentials vanish. The combined potential decreases by at most three per day. Therefore $T_5\ge\frac{2(6h-54)}3=4h-36=18n-36.$

An explicit sweep attaining the bound

By Lemma 3.2, weight-then-reverse-lexicographic prefixes have prefix neighborhoods even when a box has an even side. We use this nesting only for construction. Let $U_p(k)$ be the cumulative cost through the bottom-slice ranks at most $k$ , and $B_p(k)$ the number of such ranks. The stable bottom data are $\begin{array}{c|c|c} p&\text{ranks}&\text{costs}\\\hline 0&(1,2,3,5,8)&(2,1,1,0,0)\\ 1&(1,2,4,6)&(2,1,1,0). \end{array}$ They stabilize already at $n=3$ , as in the odd-cylinder proof. Reflection now exchanges the colors. Counting the top slice gives the exact physical prefix profiles, zero at zero, $f_p(k)=k+U_p(k)-4+B_{1-p}(h-k),\qquad k>0.$ Indeed the top slice has $4+p$ vertices of source color $p$ , its omitted vertices have the bottom ranks of color $1-p$ , and the origin correction is $p$ ; the resulting constant is $p-(4+p)=-4$ .

Start one cohort in phase zero of this order and inspect its last five rooms each day. The full count follows $h\longrightarrow h-2\longrightarrow h-3,$ returning to phase zero. For every phase-zero count $10\le k\le h-3$ , the next two days are $k\to k-1\to k-1$ . After $h-12$ such pairs, the count is nine in phase zero. The final four days are $9\longrightarrow8\longrightarrow7\longrightarrow5\longrightarrow0.$ All these transitions follow by direct substitution in $f_p$ : $U_0$ is saturated by rank three and $U_1$ by rank four, while the opposite tails supply the displayed upper range. Thus the solo duration is $2+2(h-12)+4=2h-18=9n-18$ for every $h\ge18$ .

This duration is even. The untouched cohort is then in physical phase one. Reflect the order in the longitudinal coordinate for its sweep; reflection exchanges colors, so it starts in virtual phase zero and has the same duration. The first cohort is empty and remains empty. The two physical sweeps take $18n-36$ days, proving the theorem. The independently reflected second order matters: the same orientation would take one additional day.

The accompanying integer certificate and an independent implementation check the finite boundary assertions and all base inequalities. Separate coordinate-neighborhood replays check the two complete sweeps at $n=4,6,8,10,12,30$ . The displayed word induction, three-interval potential argument, and explicit sweep establish the unbounded theorem.

Six inspections on even $3\times3\times n$ cylinders

Theorem 5.6. For every even $n\ge4$ , $T_6(P_3\mathbin{\square}P_3\mathbin{\square}P_n)=6n-8.$

Proof. Put $n=2L$ and $h=9L$ . We reuse the arbitrary-support geometry proved in Section 5.6; those geometric statements do not depend on the inspection budget. For a cohort of size $k$ , let $e$ record whether the preceding survivor had surplus four and size in $[4,h-8]$ . Initially $(k,e)=(h,0)$ . The valid domains are $0\le k\le h$ for $e=0$ , and $8\le k\le h-4$ for $e=1$ . After $p$ useful inspections, put $s=k-p$ . An empty survivor gives $(0,0)$ . Otherwise the next size $y$ satisfies $y\ge g_h(s)$ , where $g_h$ is (28). The next bit is one exactly when $4\le s\le h-8$ and $y=s+4$ . Consecutive bits equal to one are impossible. This relaxes every physical search, including searches whose supports are not global prefixes.

Assign charges $(c(0),\ldots,c(6))=(0,0,0,1,1,2,2)$ . They satisfy $c(p)+c(q)\le2$ whenever $p+q\le6$ . Define $\begin{aligned} (F_0(0),\ldots,F_0(8))&=(0,0,0,1,1,2,2,3,4),\\ F_0(k)&=\min\left\{\left\lfloor 4k/3\right\rfloor-7,\,4h/3-8\right\} &&(k\ge9),\\ F_1(k)&=\left\lfloor(4k+2)/3\right\rfloor-7 &&(8\le k\le h-4). \end{aligned}$ Both functions are nondecreasing. Every allowed transition satisfies $F_e(k)\le c(p)+F_{e'}(y).$ (30) Here is a finite verification with an explicit extension to all lengths. For $h=18,27$ , enumerate valid $(k,e)$ , $0\le p\le\min(k,6)$ , and every $g_h(k-p)\le y\le h$ . Set $e'=1$ precisely in the critical case above, reject $e=e'=1$ , and check (30); when $p=k$ , check just $(y,e')=(0,0)$ . These are respectively 1,095 and 3,174 integer inequalities, all satisfied. This specification and the formulas fully determine the finite certificate; the companion artifact includes an exact enumerator.

For $h=27+\Delta$ , where $\Delta\in9\mathbb{N}$ , it suffices by monotonicity to check the least output in each next-bit class. Split the source range:

If $k\le14$ , the profile and critical status are unchanged from $h=27$ , and every minimum output is at most 19. The potentials are also unchanged, so the base inequalities apply.
If $k\ge20+\Delta$ , subtract $\Delta$ from source, survivor, and output. Since $s-\Delta\ge14$ , the lower profile and critical upper endpoint depend only on $h-s$ ; the full case $s=h$ remains full. The transformed transition is therefore an allowed $h=27$ transition. Both potentials decrease by $4\Delta/3$ , including the full-state cap.
If $15\le k\le19+\Delta$ , then $9\le s\le h-8$ . The minimum branches are $0\to1$ with $y=s+4$ , and $0\to0$ or $1\to0$ with $y=s+5$ . The uncapped formula $\left\lfloor(4k+2e)/3\right\rfloor-7$ applies throughout. The maximum drops over $k\bmod3$ , for $p=0,\ldots,6$ , are $\begin{array}{c|rrrrrrr} &0&1&2&3&4&5&6\\\hline 0\to1,\ 1\to0&-6&-4&-3&-2&0&1&2\\ 0\to0&-6&-5&-4&-2&-1&0&2 \end{array}$ Every entry is at most $c(p)$ .

This proves (30) for every even length. The two initial potentials sum to $2(4h/3-8)$ and both vanish at capture. Their combined daily drop is at most two, giving $T_6\ge4h/3-8=6n-8$ .

For the upper bound, the first two moves depart slightly from a global prefix sweep. Start with the phase-one cohort, whose full slice counts are $(4,5)^L$ . Retain the transverse slice prefixes with counts $R_1=((4,5)^{L-1},2,1),\qquad R_2=((5,4)^{L-1},1,0)$ on the first two days. Their successive neighborhoods, calculated from the transverse profiles, are $((5,4)^{L-1},5,2),\qquad A=((4,5)^{L-1},4,1).$ Each move inspects six rooms, and $|A|=h-4$ . The global weightlex prefix of size $h-10$ is contained in $A$ . Indeed, its only missing rooms are four final-slice cells of coordinate weight at least $n+1$ . Reflection in all three coordinates maps rooms of weight at least $n+1$ to the seven phase-zero rooms of weight at most two. Thus all four missing cells lie among the seven largest-weight rooms and are omitted by this prefix.

Now repeatedly retain the global prefix of size $\max(k-6,0)$ . The compatibility and exact prefix profiles established in the preceding subsection justify every later move. Starting in phase one, each pair with $k\in\{17,20,\ldots,h-4\}$ gives $k\to k-1\to k-3$ . After $(h-18)/3$ pairs the count is 14, and the final six days are $14\longrightarrow13\longrightarrow11\longrightarrow10 \longrightarrow8\longrightarrow6\longrightarrow0.$ One cohort therefore takes $2+2(h-18)/3+6=3n-4$ days, an even number. The other cohort stays full during these moves. Reflecting the long coordinate converts its phase zero into the virtual starting phase one, so the same construction clears it in a further $3n-4$ days. ◻

The finite arithmetic certificate and its all-length extension are ordinary proofs. This additional even-cylinder result is not presently a complete physical Lean theorem.

Applications of the shared height construction

The height construction is Theorem 24.1 (main) in the main manuscript. We use it here without duplicating its proof.

Theorem 5.7 (Exact feasibility on sufficiently long boxes). Let $H$ be a finite bipartite graph with $A\ge2$ vertices and a Hamiltonian path. If $n\ge2\left\lfloor A/2\right\rfloor$ , then $h(H\mathbin{\square}P_n)=\left\lfloor A/2\right\rfloor+1.$ In particular, this applies to every Cartesian box used as the transverse graph, with arbitrary even or odd side lengths.

Proof. The Hamiltonian path supplies a spanning subgraph $P_A$ of $H$ , so $P_A\mathbin{\square}P_n$ is a subgraph of $H\mathbin{\square}P_n$ . An evader can restrict its moves to this subgraph; the subgraph need not be induced. The classical rectangle theorem (Abramovskaya et al. 2016, Theorem 2) therefore gives $h(H\mathbin{\square}P_n)\ge\left\lfloor\min(A,n)/2\right\rfloor+1 =\left\lfloor A/2\right\rfloor+1.$ Theorem 24.1 (main) gives the matching upper bound. A Cartesian box has a Hamiltonian path by the usual snake construction: traverse successive slices alternately forwards and backwards along a Hamiltonian path in the lower-dimensional box. The joining endpoints differ only in the new coordinate. ◻

Thus, for example, $4\times4\times n$ requires exactly nine probes for every $n\ge16$ , and $3\times4\times n$ requires exactly seven for every $n\ge12$ . The length threshold is sufficient; no claim is made that it is the first length attaining the eventual budget. This theorem settles feasibility in an unbounded family containing all side parities, without asserting an optimal-time formula.

Corollary 5.8. For every $n\ge3$ , $h(P_3\mathbin{\square}P_3\mathbin{\square}P_n)=5$ . The remaining values are two at $n=1$ and four at $n=2$ .

Proof. For $n\ge3$ the board contains the three-cube. An evader may choose to stay in that subgraph, so its hunting number is at least five. Theorem 24.1 (main) gives the upper bound with $A=9$ . At $n=1$ use the rectangle theorem; at $n=2$ use Theorem 5.1 with the $3\times3$ base. ◻

For a general box this construction can be applied along a longest axis, giving $\left\lfloor(\prod_{i\ne j}n_i)/2\right\rfloor+1$ as a sufficient budget. It can be loose. The five-inspection time of every $3\times3\times n$ cylinder is determined above; the full classification at larger budgets remains open here.

General-cylinder growth rates

Theorem 25.1 (main) in the main manuscript, retained there as a rectangle proof tool, also gives the following independent applications.

For example, at budgets nine and ten respectively, $T_9(P_4^2\mathbin{\square}P_n)=16n+O(1)$ and $T_{10}(P_4^2\mathbin{\square}P_n)=8n+O(1)$ . At seven probes, $T_7(P_3\mathbin{\square}P_4\mathbin{\square}P_n)=12n+O(1)$ . Here the cross-section and budget are fixed while the longitudinal side grows. The next theorem strengthens this leading-term result to an exact eventual affine period for every fixed transverse box. Exact constant terms for all short boxes remain a separate question.

Eventual affine periods for every fixed transverse box

Theorem 6.1 (Every fixed transverse box). Let $Q$ be a fixed Cartesian product of finite paths, with $A=|Q|\ge1$ . For each fixed integer $m>A/2$ , put $D=2m-A,\qquad g=\gcd(A,D),\qquad \Delta=2D/g.$ There is an effectively specified positive integer $N$ , bounded by a polynomial in $A$ and $m$ , such that $T_m(Q\mathbin{\square}P_{n+\Delta}) =T_m(Q\mathbin{\square}P_n)+4A/g,\qquad n\ge N.$ (31) Both longitudinal parities are covered, and $\Delta$ is an even integer. For each integer $0\le m\le A/2$ , all sufficiently long cylinders are impossible to search with that budget.

Combining the parity classes

Proof of Theorem 6.1. Every transverse box has a Hamiltonian path by the snake construction used in Theorem 5.7. If $A\ge2$ is even, Theorem 26.1 (main) already supplies the asserted recurrence for both longitudinal parities. If $A\ge3$ is odd, every nontrivial transverse side is odd. Theorem 4.3 applies to odd longitudinal lengths, while Theorem 26.4 (main) applies to even lengths. Both give exactly the same even period $\Delta=2(2m-A)/\gcd(A,2m-A)$ and the same increment $4A/\gcd(A,2m-A)$ . Taking the larger threshold proves the common recurrence on both parity classes.

If $A=1$ , the cylinder is a path. For $m=1$ the formula $T_1(P_n)=2n-4$ , $n\ge3$ , gives period two and increment four. For $m\ge2$ , take $\Delta=2(2m-1)$ and $N=m+1$ in (1) (main). This changes its ceiling by four and preserves both the exceptional congruence and the parity correction, giving the required increment $2\Delta/(2m-1)=4$ .

For $A\ge2$ and integer $m\le A/2$ , Theorem 5.7 gives impossibility whenever $n\ge2\left\lfloor A/2\right\rfloor$ . If $A=1$ , the only such budget is zero; no target on a nonempty path can be captured without an inspection.

For completeness the displayed sufficient time thresholds are polynomial. With $X=A+m+1$ , their definitions give $K,B,L_1=O(X^2)$ , $E=O(X^4)$ , $F=O(X^5)$ , and $\rho=O(X^4)$ . Because $m>A/2$ , we have $K_0\le2(A-1)$ and $\ell_0\le2A$ , so $U=O(A)$ and $W=O(X)$ . The dominating threshold term $F\rho$ is $O(X^9)$ . For the earlier odd-length box theorem, $S=\sum_i(n_i-1)\le A-1$ , hence its corner bound satisfies $Z=A(S+1)\le A^2$ . Substitution into (15) also gives a polynomial bound, dominated by $O(X^9)$ . The path threshold is smaller. Taking the larger parity threshold thus preserves a uniform polynomial sufficient bound. ◻

At the eventual minimum budget $m=\left\lfloor A/2\right\rfloor+1$ , the period is two. The time increase on adding two columns is $2A$ when $A$ is even and $4A$ when $A$ is odd. The polynomial onset bound is sufficient, not a claim of the earliest length at which this recurrence holds.

The theorem fixes the entire cross-section and the budget while the last side grows. It does not supply the smallest period, the finite exception values, or a simple formula for every arbitrary finite box. The proof covers every transverse box; for a general odd-order Hamiltonian graph the new paired-column theorem only asserts the even-length case. These eventual-period results have ordinary proofs and independent review, rather than complete Lean formalizations.

Formalization, evidence and provenance

The canonical development has 83 Lean 4.33.1/Std source modules shared with the main project. There are no admitted proofs, project-specific mathematical axioms or trusted external solver results in the checked receipt. Scope manifests assign application roles while keeping one source for each module. Module counts must not be read as numbers of complete geometric classifications. This companion package contains 51 modules, including 11 shared with the 43-module rectangle package. The split preserves the existing compilation receipt and checks unchanged source hashes and import closure; it does not claim a new Lean compilation.

Two complete physical-game classifications belong to this companion.

ThreeCubeTimeClassification covers every budget on $3\times3\times3$ , including the five-inspection eighteen-day lower bound and attaining schedules. FourCubeClassification covers every budget on $4\times4\times4$ , including the shape-sensitive forty-day lower bound at budget eight. Both quantify over actual target walks and room-valued inspection sequences. The paths and two-row classifications belong to the main rectangle scope.

The all-odd-box isoperimetric nesting theorem, the closed-neighborhood side-two reduction, exact cylinder profile transfer, $3\times4\times4$ ordinary classification, unbounded $3\times3\times n$ formulas, general height constructions and eventual periods have ordinary proofs rather than complete physical-game Lean proofs. Concrete cube profiles, compression operators, semantic reductions and finite checks support some of them without verifying every geometric hypothesis. The generic survivor-envelope equivalence is formalized, while its spatial matrix and semilinearity applications remain ordinary proofs. Each theorem’s source and the detailed module map retain these distinctions.

The original path research is credited to the author’s October 2019–March 2020 work. The subsequent grid and box investigation, experiments, proof development and writing used substantial assistance from Astra 6 through the Codex harness. Reorganizing these results does not change attribution, proof status or priority claims. The human author retains responsibility for the work and any eventual submission.

This companion is parked, not an arXiv submission. Its remaining questions are independent future work. The canonical records and downloads are at https://angelraychev.com/princess/extensions/.

Acknowledgments

The author thanks Dimitar Rusev for writing the preliminary section on monotonicity (Section 3) in the 2020 student-conference version of this work. By agreement, his contribution to that version is acknowledged here; both authors remain credited in its bibliographic entry. The author also thanks his mathematics teacher and mentor Dimitar Dimitrov, who encouraged him to pursue mathematical research and guided his early work.

Abramovskaya, Tatjana V., Fedor V. Fomin, Petr A. Golovach, and Michał Pilipczuk. 2016. “How to Hunt an Invisible Rabbit on a Graph.” European Journal of Combinatorics 52: 12–26. https://doi.org/10.1016/j.ejc.2015.08.002.

Bezrukov, Sergei L., and Oriol Serra. 2002. “A Local–Global Principle for Vertex-Isoperimetric Problems.” Discrete Mathematics 257 (2–3): 285–309. https://doi.org/10.1016/S0012-365X(02)00431-4.

Bolkema, Jessalyn, and Corbin Groothuis. 2019. “Hunting Rabbits on the Hypercube.” Discrete Mathematics 342 (2): 360–72. https://doi.org/10.1016/j.disc.2018.10.011.

Körner, János, and Victor K. Wei. 1984. “Odd and Even Hamming Spheres Also Have Minimum Boundary.” Discrete Mathematics 51 (2): 147–65. https://doi.org/10.1016/0012-365X(84)90068-2.

Otachi, Yota, and Ryohei Suda. 2011. “Bandwidth and Pathwidth of Three-Dimensional Grids.” Discrete Mathematics 311 (10–11): 881–87. https://doi.org/10.1016/j.disc.2011.02.019.