Rectangle capture time: remaining gaps
Rectangle overview · Exact coverage · Remaining gaps · Progress against the goal · Manuscript · Parked extensions
This page is generated from the private project’s canonical assessment. Named research files and certificates are preserved in the mathematical sources package; theorem links lead to the current manuscript-derived proofs. Download this assessment.
29 October 2026. The accepted computable bounds differ by at most two throughout and . The union of all prior exact regimes and the new all-budget odd-width-at-least-8,193/even-length regime is retained. Its complement is not a claim that every individual instance is unknown. The coverage assessment gives the ranges.
1. Matching the two-day bracket
The remaining mathematical issue is uniform compatibility of boundary shapes with their actual arrival times, physical checkerboard phase, and shared inspection budget. We have rigorous lower clocks, genuine head and suffix constructions, and sufficient middle-transfer theorems. We do not yet have a theorem ensuring that one pair of admissible boundary shapes attains every unresolved candidate deadline, or that every alternative violates a necessary history constraint.
Odd-by-odd boards retain exact joint evaluation. Even-area boards retain literal finite evaluators, as well as the practical two-day constructive bracket. A generic exact state-space search is not the claimed uniform gap-zero closure or a direct parameter-only optimal inspection rule.
2. What has succeeded
The uniform odd-width comparison removes the remaining three-day exceptions, giving a whole-domain ceiling of two. The new all-budget exact theorem handles every even length at odd widths at least 8,193. No eventual-length qualification is hidden.
Physical raw-boundary reshaping gives the exact 285-day and 413-day examples in the current checkpoint. Shared-layer necessary models suggested the shapes; actual backward arrival, forward suffix words, and independent literal replay validated them. A feasible relaxation alone was never used as an upper-bound proof.
The direct middle theorem and the paired raw-boundary sufficient criterion preserve inherited overlap, phase, and real quota. The pronic reverse cap, unique sensitive creator masses, ordered creator clocks, and shared-defect ancestry constrain any proposed faster history. The earlier front/front and front/corner results remain accepted; their existence is not new progress in this release.
3. Failed shortcuts and the lesson
Universal optimality of the old fixed-corner prefix is false: it is one day slower on both 64-by-93 at budget 48 and 102-by-124 at budget 72. A lower-bound attack aiming to prove that construction always optimal has the wrong target.
Free arrival of a raw boundary profile at its scalar clock is also false. On 12-by-12 at budget 7, a 22-cell proper-root notch would need a 20-cell predecessor in a fixed 27-cell neighborhood with shadow at most 25. Two independent exact checks of all 888,030 predecessors give minimum shadow 26. The target arrives at ten updates rather than the scalar estimate eight. The proof uses the repaired strict-collar envelope on an induced 11-by-12 subrectangle; it does not invoke the older high-budget-only envelope outside its range.
Static packing, separately optimal endpoint shapes, and pairwise overlap constraints do not automatically supply a compatible history. The same missing cells and unused inspection allowance must be shared across all ancestors. Failed cone searches do not prove impossibility, and feasible necessary integer models do not prove reachability.
4. The next decisive obligation
At each unresolved full-board deadline, either derive a contradiction from genuine history constraints, or choose compatible boundary profiles with real head and suffix words at the required clocks that meet a proved middle criterion. This must retain both cohorts, both physical phases, every activation branch and per-day quota sharing.
A quota-preserving paired compression into a sufficiently rich profile class is the most direct unification route. The new abstract Lean theorem verifies what such operators would preserve, but the required geometric operators for unequal even-area rectangles have not been constructed. Two-sided raw intervals may require a richer class than the currently successful one-sided notches.
The complementary lower-bound route is a regional potential retaining true creator clocks and a common defect budget. It should rule out a deadline only when every genuinely reachable profile pair fails, rather than independently optimizing incompatible pieces. These are research directions, not promised theorems.
5. Evaluation, construction, verification and presentation remain distinct
After uniform matching, the final goal still requires an absolute O(1)-operation expression, with no parameter-length recurrence, sum, optimizer or preprocessing hidden inside an operation. Direct optimal inspections remain a separate obligation where present algorithms reconstruct them by search. No expression simplification was pursued ahead of global matching.
The new general rectangle statements have ordinary proofs, internal independent reviews and stated exact certificates. Complete physical-game Lean proofs remain available for paths and two rows; supporting modules do not formalize all wider-board claims. Publication synchronization is separate from mathematical unification. Independent extensions stay parked at /princess/extensions/.