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.
13 September 2026. Research is paused for reconciliation. The goal is unchanged: every rectangular full-start constant-budget capture time in fixed-size standard numerical operations, with directly specified optimal inspections and proofs. See CLASSIFICATION_SCOPE.md, RECTANGLE_COVERAGE.md, and the baseline comparison BOX_RECONCILIATION.md.
An exact optimizer does not close the numerical goal. A direct optimal strategy with an iterative clock closes construction and optimality, but still leaves evaluation. A finite diagnostic may identify a missing lemma without proving that lemma at every width. Those distinctions control the assessment below; old, superseded containing ranges are not current claims.
1. Remaining even-area full-board values and direct optimal strategies
Write w=min(a,b), n=max(a,b). After removing the original narrow/high-budget formulas and the new exact families, the containing ranges are:
- w=2r>=6, n>=w, r+1<=k<=r(r-1)-1, excluding fixed-block inputs where the proved lower and upper agree.
- w=2r+1>=7, n>=w even, r+1<=k<=r(r+1), excluding (w,k)=(25,13).
Isolated certified points inside these ranges keep their exact values. The known exact boundary-port representation is still an optimizer with parameter-dependent preprocessing. It does not settle the final requested form of the answer throughout either range.
The largest new uniform bound statement is a one-day interval between a named corner-model lower and a physical upper whenever k>=ceil(4w/3). For even w, k>=ceil(13w/10) already suffices; for odd w=2r+1 the additional condition k>=ceil(13r/5)+3 and a sharper integer test are available. These thresholds are sufficient, not necessary. The budget interval from feasibility to these thresholds still has no universal one-day theorem. Even above them, the remaining day is not uniformly decided.
Two current examples separate progress from completion. The whole family T13(25,n)=50n-925 is exact for even n>=26. For24 rows, T13(24,n)>=24n-370 holds at every n>=24, but the matching upper on even lengths is24n-369. For odd n>=25 the current upper is24n-368, a two-day bracket. In particular T13(24,24) remains206 versus207. A103-day necessary solo history has not been turned into a physical103-day schedule or excluded in the unrestricted game.
What has been tried and what it taught us
The original scalar neighborhood minima do not compose into a legal strategy. The recorded6x6,k5 size relaxation predicts13 where the exact finite calculation gives14. Corner availability and erosion counts improve that relaxation, but they still permit histories whose distant corners cannot be reached quickly enough.
Whole near-square and near-pronic intervals now force localization, not only their exact equality endpoints. These restrictions extend through stated critical cases, and their guarded mergers are proved. Two persistent radius coordinates record how the localization propagates; a fixed-operation lens counts the maximum overlap of the corresponding corner balls. These tools remove false terminal shortcuts at widths25,23 and47. The25-row application is a uniform full-board theorem; the23/47 checks remain finite terminal-model evidence.
The new clipped radius clock has a proved Bellman inequality through updates, resets and the stated mergers, including excursions above its terminal size cap. Its initial value with unknown radii can be too weak. Therefore merely writing this potential does not prove the target boundary clock or the full-board lower.
The current lower-bound conjecture isolates consecutive sharp square events. Between them the nonsensitive steps obey one pronic recurrence. An opposite- anchor event must also satisfy the corner-ball lens. The proposed charge compares its elapsed time plus the new anchored clock with the previous anchored clock. It has passed19,263 exhaustive small-parameter checks and 24,766 targeted larger-parameter checks; these are not an unbounded proof. Discrete clock credits matter: a continuous extra-delay estimate can be less than one day. Entry from unrestricted boundary states and critical excursions also need their own justified treatment.
On the upper side, the exact descending-word scheduling theorem showed that changing visibility times gives no new credit for that fixed word at feasible even-width budgets. A larger search over that same word cannot close the gap. The uniform corner-change construction removes a splice-index search at the minimum budget, but is not proved optimal. The new16-row/budget56 shape change demonstrates an actual strict improvement over both anchored-prefix uppers on an infinite residue class. So the remaining discrepancy must not be assigned exclusively to the lower bound without evidence.
Two simpler proposed potentials failed: the minimum of the two phase clocks can switch its preferred orientation illegally, and selecting the phase from current corner counts loses the old anchor when its corner is inspected away. A proposed smaller multiple of the low root-credit loss also fails under physical two-step updates. These failures motivate persistent geometry and phase alignment, rather than additional unproved scalar identifications.
What would close this part
A full-board lower matching a directly specified physical family would settle value and construction, even if a numerical clock remained. One possible route is an event-charge theorem with a valid entrance argument; another is a different manageable optimal family proved by a global replacement. Neither requires optimality from every arbitrary partial state. Any stronger partial-state statement should be pursued only when it helps this obligation.
2. Remaining odd-board central decisions
Every odd rectangle already has the exact interval2tau-1<=T<=2tau and an exact retained joint evaluator. The new scalar decision is proved on every odd length whenever r+1<=k<=2r or27k³<=r⁴, where w=2r+1. Minimum budget, high budgets, widths through five and odd-length width seven are also covered. An improved explicit onset and a recent-reset test cover further inputs.
Thus an exact containing range for the still-unproved direct scalar decision is w=2r+1>=9, n>=w odd, 2r+1<=k<=r², 27k³>r⁴, below the improved onset, and outside the accepted reset or other special-case conditions. This is still an infinite family, despite the finite number of possible shorter lengths at each fixed width and budget. It must not be described as a fixed finite set of exceptions.
The new short-window collar bounds the numerical smaller coordinate of every exceptional history. An orientation cleanup then gives the improved onset. The all-low-linear theorem uses an unbounded ordinary argument and one fully checked19,852-case finite complement. The cubic-budget extension is an ordinary inequality proof. These replace substantial parts of the former joint optimization requirement with direct optimal strategies.
The remaining direct attack asks whether relevant actual exceptional frontiers always have a correctly oriented dominating representative, or whether a weaker full-board central obstruction suffices. A plateau-aware elimination now states exactly when a proposed crossed target can have an oriented exceptional predecessor. That is a local necessary/exact feasibility tool, not a proof that true solo orbits avoid all such crossings.
Stronger convenient assertions have failed. Separate ammunition costs do not ensure a simultaneous schedule. An actual21x21,k12 history has one unit of rounded-root credit beyond primary lag. Synthetic capacity traces violate stronger orientation envelopes even after several full-budget updates. The suggested claim that all bottom solo gaps stay in{0,1} is false on the actual11x11,k7 sequence(0,0),(4,4),(8,7),(10,11),(14,12). No accepted theorem uses that claim. Actual ancestry and the true scalar orbit must enter the proof, or an appropriate dominating exchange must replace them.
3. Numerical evaluation after optimality is proved
The original minimum-budget gap is unchanged: w=2r+1>=17, n>=w odd, k=r+1 has exact value2wn-(8r²-4r-4L_r+4), but L_r still uses a width-only recurrence. Its optimal strategy and matching bounds predate the fixed-scope baseline. A general fixed-size expression for L_r has not been obtained.
Arbitrary-budget solo clocks likewise retain width-dependent changing root bands outside the fixed-block region16(2k-w)>=r². The new49-block evaluator removes this dependence in that stated region, and its composition with the accepted scalar-decision conditions gives exact bounded subfamilies. It does not eliminate every root band at every surplus budget.
On even widths,16(k-r-1)>=r² gives a fixed168-block lower/upper evaluator. Equality closes that input’s value and direct construction under the numerical goal. A strict gap leaves the mathematical choice unresolved. Even a future uniform matching theorem may still require evaluation of the remaining low-budget entrance and terminal clocks.
Possible next approaches should target the whole accumulated root-band passage, not only the affine middle, which already has bulk division jumps. A bounded number of decisive bands or a genuine closed summation would help. Replacing a clock by a named hitting time, a variable matrix product, a parameter-sized sum, or a shortest path is not numerical completion. No proof that the desired closed expression exists or is impossible has been found; neither conclusion should be inferred from the present progress.
4. Formalization and exposition
Complete physical-game Lean classifications in the main scope remain paths and two rows. The83 canonical formal modules and their source-specific coverage are unchanged. New geometry, wide-rectangle classification regions, and finite certificate interpretations have ordinary proofs and independent reviews, not new complete Lean classifications. The target remains a faithful physical-game theorem for the eventual rectangle result and its dependencies.
Current overview, detailed proofs, PDF, source packages and reconciliation must distinguish fixed-size expressions, exact recurrences, optimized characterizations, direct inspections, and merely feasible constructions. The baseline comparison is in BOX_RECONCILIATION.md. Historical attempts and old coverage statements remain preserved in the source record; they are not competing current assessments.
5. Scope and restart priorities
Independent higher-dimensional boxes/cylinders, varying-budget classifications, and unrelated partial-start objectives remain parked at/princess/extensions/. Their results and formal coverage are preserved. Relevant compression, isoperimetry, inverse profiles, corner geometry, height transitions and constant-budget inverse-deadline consequences remain available in the main project. Parking applications is scope selection, not a new theorem.
On resumption, prioritize matching the remaining even-area bounds while allowing the independent odd central-decision route to proceed. Then address the fixed-size numerical clocks where exactness is already known. A major proof that settles a parameter family is more valuable than another isolated width or a minor sharpening of a sufficient threshold. Research is currently paused; these restart directions are not automatic authorization to continue.