# Rectangle completion gaps and restart 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](CLASSIFICATION_SCOPE.md),
[RECTANGLE_COVERAGE.md](RECTANGLE_COVERAGE.md), and the baseline comparison
[BOX_RECONCILIATION.md](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](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.