Finding a princess on a rectangle

13 Sep 2026

Active scope: two-dimensional rectangles, a constant daily budget and full initial uncertainty. The latest work adds uniform exact families, explicit constructions and one-day bounds across a linear-budget region. The full fixed-size closed-form classification remains open. The new results have reviewed ordinary proofs and checked computational certificates, with no additional Lean formalization. The progress reconciliation separates these advances from the original completion 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(a,b) for the answer on an a × b rectangle with k simultaneous inspections per day. Rotation gives T_k(a,b) = T_k(b,a). The objective includes when capture is impossible and a directly specified optimal sequence of inspections whenever the answer is finite.

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 · Lean coverage · Paper and sources · Parked extensions

The corridor theorem comes from Angel Raychev's October 2019–March 2020 research. Rectangle extensions and proof development date to September 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.

What is now proved for general rectangles

Width, length, and daily budget now vary together. For a rectangle with shorter side w ≥ 2, the known feasibility threshold is ⌊w/2⌋ + 1. We have exact neighborhood formulas for every width and exact geometric characterizations of minimum time at every feasible budget. A fixed-size numerical formula using an absolute O(1) number of standard operations, independent of width, length and budget, remains open.

Every odd width at the smallest feasible budget: for w = 2b + 1, odd n ≥ w, and m = b + 1, the exact time is 2wn − C_w. One width-only corner calculation determines the constant for every width; it takes only O(w) arithmetic stages. This replaces the previous list of seven verified widths mathematically. The recurrence remains an intermediate result under the fixed-size numerical goal. Formula and proof.

Odd-by-odd rectangles at any feasible budget: the optimum is either 2τ − 1 or 2τ, where τ is the faster search when the initial checkerboard parity is known. For every sufficiently long rectangle, the two pure solo residuals alone decide which. The onset is explicit. Outside the newly settled budget ranges below, shorter cases retain an exact bounded joint-state calculation whose size depends on width and budget, not length. The general solo calculation has O(w) stages, so an exact decision can still leave a numerical evaluation gap under the current goal. Scalar theorem · Exact remaining evaluator.

Every rectangle with an even number of rooms: an optimal search has closely spaced physical boundary checkpoints. Interior connections now have explicit weights computed from their endpoint heights. A finite graph of boundary choices gives the exact optimum and a compressed optimal strategy, using a bounded number of integer arithmetic stages in the length after preprocessing. That preprocessing depends on width and budget and can be very large; the general compiler is not implemented in the explorer. Its parameter-dependent preprocessing and operation bound do not satisfy the absolute O(1) numerical goal. Expanding every daily inspection takes time proportional to that output. Theorem and proof.

Explicit large-budget formulas cover all side parities. The threshold for shorter width 2b is max(b + 1, b(b − 1) + 1). It is b² + 1 for width 2b + 1 at odd length, and b(b + 1) + 1 at even length. The even-width theorem includes every feasible four-row budget. These general classifications have independently reviewed ordinary proofs; complete geometric formalization in Lean remains pending.

Explicit constructions now cover every feasible budget on every even-area rectangle. The same quotient-and-remainder expressions used by the large-budget theorems give upper bounds at smaller budgets too. They come with specified inspections on the actual board. The general high-budget theorems supply matching lower bounds at the thresholds above; at smaller budgets, optimality requires a separate result such as one of the new families below. Even shorter sides · Odd shorter sides and even lengths.

New uniform bounds and exact families

New exact odd-area ranges cover every length. For w = 2r + 1 and every odd n ≥ w, the two solo residuals give the exact full-board decision at every feasible budget satisfying r + 1 ≤ k ≤ 2r or 27k³ ≤ r⁴. Direct optimal prefix and central-day strategies accompany the result. The clocks in these entire ranges are not yet uniformly evaluable in O(1) operations. Separately, all seven-row odd-length budgets now have exact fixed-size formulas, as does the even-width family w = 2r, k = r(r − 1), r ≥ 3, at every length. Exact ranges and remaining numerical obligations.

A uniform one-day bracket now holds on every even-area rectangle with w ≥ 4 and ⌈4w/3⌉ ≤ k < wn/2. A lower bound for arbitrary searches and a directly specified prefix-and-reflection strategy differ by at most one day. On even widths, the sharper threshold is k ≥ ⌈13w/10⌉. These are proved inequalities for all lengths and widths in the stated ranges; they do not determine which endpoint is optimal or turn the underlying clocks into a fixed-size formula. Uniform bracket · Sharper budget range.

Twenty-five rows with thirteen inspections per day: every even n ≥ 26 takes exactly 50n − 925 days. The physical construction shares a final inspection day; the lower proof retains geometric information about possible corners across successive days. This is an all-length equality, rather than extrapolation from a list of boards. The reconciliation records this family alongside the other new formulas, their direct strategies and the remaining gaps.

Further exact cases, and a one-day gap

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 × 8 board with five inspections per day takes 40 days; a 12 × 12 board with seven takes 72 days.
• A 7 × 8 board with four inspections per day takes 68 days; a 9 × 10 board with five takes 96 days.
• An 11 × 12 board with six inspections per day takes 128 days; an 11 × 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 × 24 board with thirteen daily inspections, the proved full-board interval is 206 ≤ T₁₃(24,24) ≤ 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 ≥ 2 rooms,

The extra day ε is one exactly when n ≡ m + 1 (mod 2m − 1) and at least one of n and m is odd. Otherwise ε is zero.

If you can inspect every room, one day suffices. With one inspection per day and n ≥ 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 ≥ 2 columns and 2 ≤ m < 2n, put N = n − 1 and M = m − 1. Then

Here ε is one exactly when M is even and N ≡ M/2 (mod 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 ≥ 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 ⌊3n/2⌋.

For the remaining budgets 2 ≤ m < ⌊3n/2⌋, 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 ≥ r + 4. When n is even and q is odd, the condition improves to m ≥ 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 ≥ 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 ≤ m < 2n, write 2n − 2 = q(m − 2) + r, with 0 ≤ r < m − 2. The answer is 2q when r = 0. Otherwise it is 2q + 1 when r = 1 or m ≥ 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 ≥ 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⌈(5n − 8)/3⌉ days when n is even. When n is odd, the answer is 2⌈(5n − 9)/3⌉ 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 ≥ w, the explicit optimal-time formula holds for every budget m ≥ b² + 1. At every feasible budget, let τ be the fastest search when the initial checkerboard parity is known. The full optimum is either 2τ − 1 or 2τ; 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 ≥ 2b² + 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 ≥ 2b, put h = bn. At every budget b + 1 ≤ m < h, divide h − b = q(m − b) + r, with 0 ≤ r < m − b, and set J(r) = r + min(⌈√r⌉, b). There is a search taking 2q days if r = 0; otherwise it takes 2q + 1 when 2J(r) ≤ m, and 2q + 2 when that test fails. These values are proved optimal when m ≥ 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 ≥ w, and every feasible budget b + 1 ≤ 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 ≥ 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(⌈√k⌉, ⌊w/2⌋, ρ(h − k)), where w is the shorter side and ρ(d) is the smallest nonnegative integer s with d ≤ 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 ≥ 7, the minimum is 2⌈(7n − 16)/3⌉ 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 ≥ 3, every odd length n ≥ w takes exactly 2wn − C_w days at the minimum budget b + 1. Here C_w = 8b² − 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 ≥ 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 general exact minimum-budget classification 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 new lower bounds do not close the general value gaps on even-area rectangles, including the uniform minimum-budget lower bound just described. The other main obligations remain: reduce width-dependent scalar clocks to bounded expressions; determine the full-board shared-budget decision on the remaining short odd rectangles; and evaluate sufficient boundary choices uniformly for even-area rectangles. Direct strategy specifications and complete physical-game formalization are tracked separately. The coverage assessment gives exact parameter ranges, source statements and evidence status. The gap assessment records failed approaches and what each proposed next step would establish.

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(a,b) ≤ 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(a,b).

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 43 checked modules from the historical 83-module combined development. The rectangle and extension packages have separate import-closed coverage; unchanged source hashes are checked against that compiler receipt. Neither the package separation nor the new corner, localization, merger and finite-case results add a Lean theorem in this checkpoint.

The exact transfer through the middle of an odd rectangle now 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 are September 2026 work 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.