Finding a princess on a rectangle

Updated 29 Oct 2026

29 October 2026 checkpoint: proved lower and constructive upper bounds differ by at most two days for every rectangle and every feasible daily budget. All budgets are now exact for odd widths at least 8,193 and every even length. The general zero-gap problem remains open. The new paired-compression lemma is checked in Lean; the wider capture-time results have ordinary proofs and independent internal reviews. Checkpoint and evidence · Progress against the goal.

You can inspect several rooms each morning. After every unsuccessful search, the princess must move to an adjacent room. How many days guarantee finding her, whatever choices she makes?

Write $T_k(w,n)$ for the answer on a rectangle with shorter side $w$, longer side $n\ge w$, and $k$ simultaneous inspections per day. The objective includes when capture is impossible and optimal inspections whenever capture is possible.

The immediate priority is matching computable lower and constructive upper bounds for every $w,n,k$. Recurrences, finite-state calculations and parameter-dependent preprocessing are acceptable now. General numerical simplification is deferred until those bounds match throughout the domain.

The numerical completion criterion is a fixed-size expression using $O(1)$ standard numerical operations, with a bound independent of all three parameters. A fixed finite case distinction, arithmetic, powers, roots, floors and ceilings are allowed. Recurrences, parameter-length sums, array updates, shortest paths and parameter-dependent preprocessing remain intermediate results. Naming an algorithm as a new operation does not meet this criterion. Printing the inspection sequence is a separate task and need not take constant time.

Progress against the goal · Exact coverage and remaining gaps · Detailed proofs · Resources

The corridor theorem comes from Angel Raychev's October 2019–March 2020 research. Rectangle extensions and proof development date to September–October 2026. The explorer covers one through four rows; each displayed schedule is checked on the actual room graph. Higher-dimensional demonstrations are preserved in the companion.

The proof excerpts below retain their local notation: $m$ denotes the daily budget $k$, $w$ and $n$ are the shorter and longer sides, and $b$ within $w = 2b$ or $2b + 1$ is a local half-width parameter.

The rooms and the rules

A path is one row of rooms. A ladder graph is simply a two-row grid: you can move left or right along a row, or between the two rooms in a column. There are no diagonal moves. A grid with $n$ columns has $2n$ rooms.

Each day you inspect at most $m$ rooms simultaneously. If every inspection misses, the princess must make exactly one legal move; she cannot stay in place. You learn only whether you found her. The aim is a guarantee against every starting room and every sequence of moves.

The explorer tracks all positions still possible after earlier misses. A dot means she could be there; it does not choose a convenient route for her. The two dot styles distinguish checkerboard parity. An × marks an inspected room.

A two-day bracket at every width, length and budget

Capture is possible exactly when $k\ge\lfloor w/2\rfloor+1$, with the path and single-room conventions included. For every feasible input, the accepted combined bounds satisfy

The lower bound applies to arbitrary legal inspection histories. The upper bound supplies actual inspections. Both are computable by the stated recurrences and finite endpoint choices. Every width, length and feasible budget is covered; all earlier exact and one-day ranges remain stronger where applicable. The last public checkpoint had a four-day ceiling, and the intervening private checkpoint had three.

Odd-by-odd boards retain their exact joint evaluator at every feasible budget. Even-area boards now have a uniform two-day constructive bracket, plus the exact ranges below. An exact finite-state evaluator is available separately, but may be expensive; it is not the final bounded-operation expression.

Every budget at odd widths at least 8,193

Let $w=2b+1$, $b\ge4096$, and let $n\ge w$ be any even length. Put $h=wn/2$ and $B=b(b+1)$. In the remaining low- and middle-budget range $b+1\le k\le B$, the exact answer is

Here $P(c)$ is the physical-prefix gate recurrence, with a prescribed optimal prefix/palindrome inspection strategy. Together with the retained high-budget formula for $B+1\le k<h$, the two-day range $h\le k<2h$, and one day at $k\ge2h$, this covers every budget and every even length at the stated widths. Budgets at most $b$ are infeasible. The recurrence is not yet an O(1)-operation expression.

A separate smaller-width band is also exact: $b\ge512$ and $3b\le k\le\lfloor15b/4\rfloor$, again at every even length. Earlier even-width transport families, odd-width natural-range families and minimum-budget results remain in the complete coverage assessment.

Why reshaping the boundary is necessary

Two new exact results are $T_{48}(64,93)=285$ and $T_{72}(102,124)=413$. The older fixed-corner construction takes 286 and 414 respectively. We now have matching lower bounds and actual inspection words, independently replayed on the room graph. Thus that older construction cannot be universally optimal; some remaining gaps require improving the strategy itself.

A common construction joins a genuinely reached head to a genuine suffix through a directly specified middle passage. It retains the physical checkerboard phase and charges inherited overlap to the real daily budget. The theorem is conditional on the stated endpoint and occupancy guards. It does not make a favorable boundary shape reachable at an arbitrarily chosen clock.

That distinction is essential: a specified 22-cell notch on a 12-by-12 board with budget seven reaches its scalar size estimate after eight updates, but the actual target needs ten. Two independent exhaustive predecessor checks establish the obstruction. This is a partial-state arrival result, not the full board's capture time.

What remains open

The missing uniform theorem must choose boundary shapes together with real, compatible head and suffix histories, or rule out the candidate deadline using their shared history constraints. Static packing and independently optimal endpoints do not suffice. The new abstract paired-compression theorem checks what a suitable compression would preserve; constructing the required geometric operators remains open.

The previously unverified 751-profile comparison was independently verified in the later 24 October continuation, including 4,507 universal arithmetic obligations and its physical interface. Its earlier discovery archive remains historical. Acceptance of that comparison does not prove global gap zero. The current checkpoint separates accepted results, diagnostic models and remaining obligations.

Earlier exact cases and bounds, retained

The shared geometric bounds, combined with finite integer certificates, now give the following exact answers. Each has a matching inspection sequence replayed on the actual room graph.

• An $8 \times 8$ board with five inspections per day takes 40 days; a $12 \times 12$ board with seven takes 72 days.
• A $7 \times 8$ board with four inspections per day takes 68 days; a $9 \times 10$ board with five takes 96 days.
• An $11 \times 12$ board with six inspections per day takes 128 days; an $11 \times 14$ board with six takes 172 days.

The finite-cases theorem gives the proof and certificate for each equality. The geometric ingredients hold uniformly across their stated parameter ranges; these numerical evaluations establish the displayed boards, rather than a classification of every width.

For a $24 \times 24$ board with thirteen daily inspections, the proved full-board interval is $206 \le T_{13}(24,24) \le 207$. The upper bound is a checked 207-day inspection sequence. A geometric obstruction, a separately verified calculation of the equality cases, and the shared-budget argument prove the lower bound of 206. Which of the two values is optimal remains open. Proof of the interval.

Why a corner can matter for several days

The number of possible rooms does not always say enough. On a half-strip of width $2b$, let a survivor in one checkerboard color have $k$ rooms and $k + s$ neighbors, with $s < b$. If $k > s(s - 1)$, every survivor room is forced into the triangle of radius $2s - 2$ at the favorable corner. The opposite corner cannot become possible before $2(b - s) + 1$ more moves, whatever inspections follow.

A single formula unifies the underlying quadrant bounds: after forbidding the chosen color’s diagonals strictly below the first allowed diagonal $h$, the largest support with surplus at most $s$ has size $\max(s(s - 1)/2, s(s - h))$. The quadrant theorem and conditional half-strip profiles have complete ordinary proofs. These restrictions are necessary geometric information; they do not prove that every sequence of separate minimizing shapes can occur in a search.

The new finite-board bounds record more than how many rooms remain possible. For each checkerboard group they also count its possible board corners, and the opposite-color corners whose two neighbors remain possible. The latter is called an erosion-corner count. This distinguishes merely reaching a corner from keeping both routes into it. The critical corner bound and erosion refinement apply to arbitrary room arrangements within their stated ranges.

Localization now holds throughout an interval of sizes, not only at one exact triangular size. On an odd-width, even-length board, sufficiently efficient cleared rooms in that interval must all lie close to one corner. This forces a restriction on the next inspection step that the existing erosion count already records. It replaces the need for another history bit in the eleven-row argument. Localization theorem · Resulting transition rule.

A further merger theorem combines the two checkerboard groups into one necessary lower-bound calculation while preserving the relevant budget and corner restrictions. This simplifies the proof of impossibility; it does not turn a numerical model path into a physical search. Matching constructions are checked separately. Together these arguments replace several isolated corner and history calculations with common theorems. Their ordinary proofs and computational consequences are new; their complete Lean formalization remains to be done.

One row: every budget

Write $T_m(G)$ for the fewest days that guarantee capture on a graph $G$ with at most $m$ inspections per day. On a path with $n > m \ge 2$ rooms,

The extra day $\varepsilon$ is one exactly when $n \equiv m + 1 \pmod{2m - 1}$ and at least one of $n$ and $m$ is odd. Otherwise $\varepsilon$ is zero.

If you can inspect every room, one day suffices. With one inspection per day and $n \ge 3$, the answer is $2n - 4$. A two-room path takes two days with one daily inspection.

The reconstructed proof gives a single indexed sweep in place of twelve construction cases. A matching lower bound counts how possible positions can disappear and identifies when equality is impossible.

Two rows: every budget

For $n \ge 2$ columns and $2 \le m < 2n$, put $N = n - 1$ and $M = m - 1$. Then

Here $\varepsilon$ is one exactly when $M$ is even and $N \equiv M/2 \pmod{M}$. One inspection per day cannot guarantee capture. Inspecting all $2n$ rooms takes one day. For a single column, the building is just the two-room path.

For example, a two-by-four grid with three daily inspections needs four days. The ceiling alone would give three; the residue condition accounts for the extra day.

The proof separates the two possible initial checkerboard parities. Projecting onto columns turns each into a path walk where a vertical move keeps the column fixed. A comparison argument reduces arbitrary search strategies to two lengths, and a short weight argument proves optimality.

Three rows: every budget

For a three-row grid with $n \ge 2$ columns, one inspection per day is insufficient. Inspecting all $3n$ rooms gives capture in one day; otherwise, two days are optimal as soon as the daily budget reaches $\lfloor 3n/2\rfloor$.

For the remaining budgets $2 \le m < \lfloor 3n/2\rfloor$, divide $3n - 4$ by $2m - 3$, writing

• If the remainder $r$ is zero, exactly $2q$ days are needed.
• If $r > 0$, exactly $2q + 1$ days are needed when $m \ge r + 4$. When $n$ is even and $q$ is odd, the condition improves to $m \ge r + 3$.
• In the other cases, exactly $2q + 2$ days are needed.

For example, a three-by-six grid with five daily inspections needs four days. With two daily inspections, the formula becomes $6n - 8$. A single column is the three-room path: it takes two days with one or two inspections, and one day with three.

The proof retains a count and one bit of information about the previous expansion. The two initial parity groups can sweep from different directions. A change of variable makes the recurrence affine; counting inspections over each group's final sweep proves that arbitrary interleavings cannot do better. The complete ordinary proof has passed an independent mathematical review.

Four rows: every budget

For four rows and $n \ge 4$ columns, two daily inspections are insufficient; three suffice. At least $4n$ inspections give one day, and budgets from $2n$ through $4n - 1$ give two days.

For $3 \le m < 2n$, write $2n - 2 = q(m - 2) + r$, with $0 \le r < m - 2$. The answer is $2q$ when $r = 0$. Otherwise it is $2q + 1$ when $r = 1$ or $m \ge 2r + 4$, and $2q + 2$ in the remaining cases. A board with fewer than four columns reduces, by rotation, to one of the earlier families.

With three daily inspections this simplifies to $4n - 4$ days. This is now a specialization of the general even-width theorem, whose improved budget threshold covers all four-row cases. The ordinary proof has passed an independent review; its full Lean formalization is still pending.

Five rows: every budget

For five rows and $n \ge 5$ columns, three daily inspections are necessary and sufficient. The exact minimum time at that budget is $10n - 20$ days. The proof covers every length: odd lengths use the neighborhood profiles below, and even lengths use a finite symbolic classification valid for every number of columns. Both proofs have passed independent review. Their counting potentials are checked in Lean; the complete geometric bridge is still an ordinary proof.

Every larger budget now has a closed formula for both even and odd lengths. Four inspections per day take $2\lceil (5n - 8)/3\rceil$ days when $n$ is even. When $n$ is odd, the answer is $2\lceil (5n - 9)/3\rceil$ days, plus two more when $3$ divides $n$. For example, five-by-nine with four daily inspections takes 26 days. The even-length theorem and odd-length theorem give the remaining quotient-and-remainder formulas and explicit strategies.

Wider rectangles: width and budget both vary

For an odd width $w = 2b + 1$ and odd length $n \ge w$, the explicit optimal-time formula holds for every budget $m \ge b^{2} + 1$. At every feasible budget, let $\tau$ be the fastest search when the initial checkerboard parity is known. The full optimum is either $2\tau - 1$ or $2\tau$; the bounded joint-state theorem above decides which. The underlying lower bound concentrates uncertainty before the first possible capture and then reverses time about the middle day.

The formula divides $wn - w - 1$ by $2m - w$. The quotient counts the full sweeps; a short rule for the remainder decides whether the two parity groups can share their transition day. At budgets $m \ge 2b^{2} + 1$, the final rule uses only integer division and a single residue cutoff. For example, seven-by-fifteen with twelve inspections per day takes exactly twelve days. The complete theorem supplies the formula and proves optimality against arbitrary interleavings.

For an even shorter side $2b$ and any longer side $n \ge 2b$, put $h = bn$. At every budget $b + 1 \le m < h$, divide $h - b = q(m - b) + r$, with $0 \le r < m - b$, and set $J(r) = r + \min(\lceil \sqrt{r}\rceil, b)$. There is a search taking $2q$ days if $r = 0$; otherwise it takes $2q + 1$ when $2J(r) \le m$, and $2q + 2$ when that test fails. These values are proved optimal when $m \ge \max(b + 1, b(b - 1) + 1)$. Below that threshold they remain upper bounds. Larger budgets give the usual two-day and one-day cases. Construction and exact range.

For example, a six-by-nine building with ten daily inspections takes exactly seven days. The construction works backwards from a small final survivor set, enlarging it into legal earlier search envelopes.

A common backwards-construction lemma now supplies the two even-area cases. It applies more generally to every connected bipartite cross-section, with at least two rooms, and allows terminal survivors of arbitrary shape when their required predecessor closure fits the daily allowance.

For $w = 2b + 1$, even $n \ge w$, and every feasible budget $b + 1 \le m < wn/2$, divide $wn - w - 1 = q(2m - w) + r$. The explicit construction takes $2q$ days when $r = 0$; otherwise it takes $2q + 1$ or $2q + 2$ according to a rounded-root test on $r$. These values are proved optimal for $m \ge b(b + 1) + 1$; below that threshold they are upper bounds. The complete theorem gives the test and separates the all-budget construction from the large-budget lower bound.

For every even-area rectangle, the exact minimum neighborhood of a single-color set with $k$ rooms is $k + \min(\lceil \sqrt{k}\rceil, \lfloor w/2\rfloor, \rho (h - k))$, where $w$ is the shorter side and $\rho (d)$ is the smallest nonnegative integer $s$ with $d \le s(s + 1)$. The proof handles all widths and both side parities. This static fact does not mean that the best shapes can always follow each other during a search.

Additional bounded-width formulas

A further closed formula covers seven rows with five daily inspections: for every odd $n \ge 7$, the minimum is $2\lceil (7n - 16)/3\rceil$ days. The proof uses a periodic potential and a two-day obstruction to rule out the last possible saving.

The all-odd minimum-budget clock

For every odd width $w = 2b + 1 \ge 3$, every odd length $n \ge w$ takes exactly $2wn - C_{w}$ days at the minimum budget $b + 1$. Here $C_{w} = 8b^{2} - 4b - 4L_{b} + 4$, where $L_{b}$ is the first arrival time in the explicit width-only corner recurrence. Its equivalent solo calculation uses $O(b)$ arithmetic stages. For widths 3 through 15, the constants begin 8, 20, 44, 84, 136, 208, 288.

For even $n \ge w$, the same expression gives a proved physical upper bound at budget $b + 1$. It can be strict: at width25, sharing the final inspection day improves $50n - 924$ to the exact $50n - 925$. Thus equality of the older expression throughout the family is false. The October natural-range theorem now gives exact recurrence-based values for every odd width at least 25 and every even length. A fixed-size numerical evaluation throughout that family remains open.

What still needs a bounded expression

For widths 3, 5, 7, 9, 11, 13 and 15 the displayed constants form a fixed finite lookup, giving bounded numerical formulas at minimum budget on odd lengths. For the general odd width the clock still needs evaluation. Proving its exactness does not settle that new numerical requirement.

The first priority remains matching the computable bounds everywhere. After that, width-dependent clocks and endpoint minima still need fixed-size numerical evaluation. Direct optimal rules are separate from reconstruction by an optimizer, and ordinary proofs are separate from complete physical-game formalization. The coverage assessment distinguishes those layers; the gap assessment records the remaining physical compatibility issues.

The inverse deadline question

On a rectangle, the minimum constant daily budget for a fixed deadline is an inverse view of the same relation $T_{k}(w,n) \le t$. Its relevant transfer results remain available in the main proof tools. Eventual periodicity or an optimizer in that formulation does not automatically yield a fixed-size expression for $T_{k}(w,n)$.

The previous 128-page combined release remains available as a dated archive. The parked companion preserves independent higher-dimensional applications. Moving those results was a choice of scope; the new shared corner arguments are mathematical consolidation within that scope. The companion's open questions are not conditions for finishing this rectangle project.

Proofs and verification

The path and two-row classifications have complete ordinary proofs and independent mathematical reviews. The explorer contains 3,000 cases across one to four rows. Every displayed strategy has been replayed on the actual room graph.

The path and two-row classifications have complete Lean proofs for every positive size and budget. They cover physical rooms, legal moves, construction of attaining strategies, and minimality against arbitrary probe sequences. Independent semantic reviews checked that the formal definitions match the game, including the single-room exception and the path formula's parity correction.

The abstract theorem for compressing whole strategies is also proved in Lean, including arbitrary daily budgets and its interpretation as capture of actual walks. Its geometric applications, and the three-row and four-row minimum-time formulas, are not yet fully formalized. The rectangle package contains 44 checked modules, including the new PairedCompression.lean. It verifies complement-dual compression, real prefix histories, daily-budget preservation and contraction of the joining overlap under explicit hypotheses. The uniform two-day bound, new all-budget exact range and wider rectangle applications have not been added as complete physical-game Lean theorems. The formal guide records the exact compiler evidence and scope.

The bounded two-counter middle-transfer theorem has a constructive Lean proof in MiddleIntervalTransfer.lean. It verifies that the endpoint conditions suffice and constructs legal daily allocations. Applying it to the rectangle’s geometric profiles remains an ordinary proof.

Two further modules verify supporting lemmas: RootConvolution.lean reduces a rounded-root optimization to two explicit candidates; ProbeLocalization.lean proves that inspections outside a final difference set’s backward reachability region can be removed without changing the final possible-position set. The finite band bounds and complete new rectangle algorithms remain ordinary proofs.

Three further formal components support this checkpoint. FastestAncestry verifies the shared-budget ancestry argument under explicit inverse-profile hypotheses and bounded-secondary trace assumptions. ClippedPyramidErosion verifies a physical cell construction and its exact loss. ConvexCapacityConvolution proves the two-candidate minimum for all unbounded nondecreasing convex integer capacities, including the concrete punctured-quadrant capacities. The quadrant geometry itself remains an ordinary proof.

Research history and credit

The path theorem comes from Angel's October 2019–March 2020 work. Its two- and three-inspection cases prove and generalize formulas conjectured by Dmitry Kamenetsky in March 2018: A301337 and A301426.

The two-row derivation, extensions, proof reconstruction, and formalization began in September 2026; the rectangle investigation continued in October 2026 using Astra 6 in the Codex harness. The higher-dimensional applications and their literature discussion are preserved in the parked companion. Literature novelty of the extensions remains under review.

Dimitar Rusev contributed Section 3 to the original joint student manuscript. With his agreement, that contribution is acknowledged in the revised manuscripts.

Read the complete proofs, download the formal artifact, or open the manuscript and sources. This is a research manuscript in preparation; no Princess paper has been submitted to arXiv.