Rectangle capture time: progress against the goal
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 objective remains every rectangle, constant budget, and full initial uncertainty. First match computable bounds and attain them physically everywhere; only then reduce the value to an O(1)-operation expression. No quantifier or completion criterion has been weakened.
The uniform numerical improvement
The last public release proved a four-day ceiling. Subsequent work first reduced it to three, then to two for every width, length and feasible budget. The new odd-width comparison closes the residual width exceptions together. Stronger earlier formulas, exact evaluators and one-day bounds are retained. A two-day worst-case ceiling is not a claim that every instance improved by two days, nor that any specific instance necessarily still has a gap of two.
New exact coverage
Every odd width at least 8,193 and every even length now has an exact answer at every budget, including infeasibility and the one/two-day endpoints. The middle-budget answer is a physical-prefix recurrence with an optimal palindrome strategy, not yet a bounded numerical expression. The additional , band for width and even length gives extra smaller-width coverage. All earlier exact families remain valid.
Odd-by-odd exact joint evaluation predates this checkpoint and is not counted again as newly solved. The 25 October literal cutset/endpoint evaluators make physical compatibility exact within their specified state spaces, sometimes with a smaller exponent than area. They do not establish that the inexpensive scalar bounds coincide everywhere.
What changed about the remaining obstruction
Two new optimal physical strategies, and , disprove universal optimality of the old fixed-corner construction. This is not merely a stronger lower-bound problem. Actual boundary reshaping is needed on some boards.
A paired middle construction now succeeds when supplied actual reachable endpoints and the stated phase, overlap and occupancy guards. The missing all-parameter theorem concerns selecting boundary profiles with genuine compatible arrivals. The proper-root notch counterexample shows why assigning an arbitrary favorable profile its scalar clock is invalid.
What the release adds, separately
The website, manuscript, PDF and source packages now describe this checkpoint. Prior releases and research records remain preserved with their original dates. One new Lean module verifies abstract paired compression and overlap preservation. It does not prove the new global two-day or all-budget capture theorems in Lean.
Scope separation remains unchanged: independent higher-dimensional and varying-budget applications stay in the parked companion. Publishing the new checkpoint is artifact synchronization; proving the new bounds is mathematical progress; retaining the parked work is scope management. These are separate achievements.
Global gap zero, the final fixed-size expression, direct optimal inspections in the remaining cases, and complete wider-board formalization remain unfinished. Coverage and remaining gaps give the precise boundaries.