Princess searches: parked extensions

13 Sep 2026

Rectangle overview · Rectangle coverage · Companion proofs · Companion Lean coverage

Parked. This companion preserves existing achievements and unfinished extensions. No new research was performed for this separation. None of its independent open questions is required to finish the main rectangle project.

The active objective is a fixed-size O(1) numerical expression for rectangle capture time, including feasibility, together with directly specified optimal inspections and their proofs. The same compulsory-movement game is studied here on higher-dimensional boxes and broader cylinders. Necessary general proof tools remain with the rectangle argument; independent applications have their home here.

Companion PDF · LaTeX sources · Research sources and certificates · Lean sources · Parked restart notes

The statements below retain their original proof boundaries. An exact algorithm is not relabeled a closed form, and a verified component is not a complete formal proof of its geometric application.

The three-dimensional example

On the three-by-three-by-three building, all budgets are now classified. Five inspections suffice, and the eighteen-day strategy is optimal.

The entire table has a complete Lean proof. It checks neighborhood bounds for all possible sets in each parity class, uses finite potentials to prove the lower times, and verifies actual inspection schedules attaining them. The final theorem quantifies over every legal target walk and every competing inspection sequence.

The eighteen-day example extends to an entire family: a three-by-three-by-n building with n ≥ 3 takes exactly 18n − 36 days with five daily inspections. That formula has an independently reviewed ordinary proof. The even-length proof uses a small finite boundary certificate and one bit of history. It proves the same formula for every even length, with no exceptional cases. Read the all-length theorem.

The four-by-four-by-four building

This even-sided box is completely resolved. Eight inspections per day are necessary and sufficient, and the optimal search at that budget takes forty days. One additional daily inspection halves the time.

Every entry has a complete physical Lean proof. At eight inspections, counts alone would suggest thirty-two days. The proof has to retain the shape of the possible-position set to establish the true forty-day minimum. Lean checks that geometric reduction as well as the lower bounds and attaining schedules.

For every even n ≥ 4, six daily inspections on the three-by-three-by-n building take exactly 6n − 8 days. Two special opening moves improve on a fixed global-prefix strategy by one day. A history-dependent potential proves optimality. This six-inspection theorem is an ordinary proof.

Odd-sided boxes in any dimension

A uniform theorem now covers every box whose side lengths are all odd: 3 × 5, 3 × 5 × 7, 5 × 5 × 5 × 5, and arbitrary higher-dimensional examples. It gives an exact algorithm for feasibility, minimum days, and an optimal strategy for every daily budget.

The key is to order each checkerboard color by distance from a corner, with a specific rule for ties. We proved that the first k rooms always have the smallest possible neighborhood, and that their neighbors form another initial segment. Any search can therefore be compared with a search described by just two counts. An exchange argument proves this in every dimension.

For V rooms, the algorithm uses at most (V + 1)² count pairs and m + 1 choices per pair. This is a proved reduction from arbitrary strategies, not a search over every subset of rooms. It is polynomial in the room count; the room count itself can grow exponentially with dimension. The theorem has two independent ordinary proof reviews and is not yet fully formalized in Lean.

General-cylinder behavior

A broader theorem applies to any fixed odd-sided cross-section in any dimension. For each fixed sufficient budget, the minimum time eventually obeys a periodic rule: adding a fixed block of floors adds a fixed number of search days. The proof gives an explicit threshold and a finite procedure to determine the constants. At the minimum budget, each added room eventually contributes exactly two days.

The two ends determine a finite correction; a sufficiently long middle section can be inserted into or removed from an optimal search. Proving this required controlling arbitrary competing searches, including those that split their daily inspections between the two parity groups. The current explicit threshold is large; it proves eventual behavior without claiming that the pattern begins at small sizes.

The parity bridge now covers every fixed rectangular cross-section and both even and odd building lengths. Fix a cross-section with A rooms and a budget m > A/2. For all sufficiently long buildings, the exact minimum time is a linear function plus a periodic correction. The proof forces efficient portions of any optimal search to have one of finitely many boundary shapes, then inserts or removes a protected block of floors. When the cross-section is odd and the length is even, one bit of history accounts for the alternating expansion costs. Arbitrary search behavior is allowed outside the efficient portions.

The period is explicit. Write D = 2m − A and g = gcd(A, D). For every sufficiently large n,

At the minimum sufficient budget, the length period is just two. We also give a polynomial bound in A and m on where the formula begins. This bound is deliberately generous. A direct argument with the heights of the advancing boundary avoids enumerating all possible boundary shapes. Read the exact theorem and proof.

Consequently, the leading term is

The error stays bounded as the building grows. For example, a four-by-four cross-section gives 16n + O(1) days at nine inspections per day, or 8n + O(1) at ten. The explicit height strategy stays within a bounded number of days of optimal. This does not specify the exact constant for each short building.

If the deadline is fixed instead

There is also a general answer to the reverse question: if capture must happen within a fixed number t of days, how many rooms must we inspect each day? For any fixed finite cross-section with A rooms, the least budget on a sufficiently long building is An/t plus a periodic correction. A finite column-by-column description proves this, using the same inspection and compulsory-movement rules.

Here the deadline stays fixed while the building grows. This is a separate theorem from fixing the budget and minimizing time. Its certificate is connected to actual target walks in Lean; the eventual-period argument currently has an ordinary proof.

Further results and open scope

These extensions have ordinary mathematical proofs and independent checks. The all-odd-box and length-two-side algorithms are polynomial in the number of rooms. The more general compression recurrences can have many states, and are not closed formulas for arbitrary dimensions. A complete classification for all rectangular boxes remains unresolved in this investigation.

Preservation and credit

The original path research is Angel Raychev's October 2019–March 2020 work. The later investigations were developed in September 2026 with substantial assistance from Astra 6 through the Codex harness. Original authorship and Dimitar Rusev's acknowledged contribution remain recorded in the manuscripts and research history.

The frozen combined release preserves the former manuscript and packages. Shared mathematical and formal sources have one authoritative copy. The formal coverage guide separates complete cube classifications from supporting lemmas and ordinary proofs. No complete arbitrary-dimensional classification or full formalization of all companion results is claimed.