# October 29 rectangle checkpoint: evidence guide

The current accepted whole-domain ceiling is U-L <= 2 for every rectangle
w <= n and every feasible constant daily budget k, with the established
conventions for degenerate boards. Global gap zero remains open.

Start with research/paired-regional-2026-10-28/RESULTS.md and the current
manuscript. That results file is the mathematical status index; individual
notes, reviews and certificates supply the precise hypotheses. All prior
exact families and stronger bounds are retained. The separate extensions
project remains parked and is not a condition for rectangle completion.

Important accepted additions include the all-budget, all-even-length exact
family w=2b+1 with b>=4096; the additional band b>=512,
3b<=k<=floor(15b/4); general physical middle-transfer and boundary-reachability
lemmas; and the exact examples T_48(64,93)=285 and T_72(102,124)=413.
Those examples disprove universal optimality of the earlier fixed-corner
prefix construction. The new general results are ordinary proofs with
internal independent review and the named exact or literal certificates.
Finite diagnostics never establish surrounding parameter families.

The October 24 continuation independently verified the previously frozen
751-profile comparison candidate and its physical interface. It is no
longer an unverified candidate in the current checkpoint. Its old separately
named candidate archive and older notes remain historical evidence. Their
old status text is intentionally preserved. Exact shape evaluators from
October 25 are potentially enormous and do not supply an O(1) numerical
formula or prove that the inexpensive bounds match everywhere.

Chronological RESULTS and logs are dated historical records. Their former
gap ceilings, private/public status and absence-of-new-Lean statements
refer to their own dates, not this publication pass. Use the current
release.json and formal-artifact.md for the synchronized release and precise
Lean coverage. All 84 canonical Lean sources were freshly compiled on
October 29; PairedCompression is the only new mathematical module. It proves
an abstract paired-history compression interface under stated hypotheses.
It does not formalize the new geometric classification, uniform two-day
bracket, boundary-arrival results, or exact 285/413-day examples.

This package contains the three newly published research directories and
all preceding October source-supplement files, together with discovered
local source dependencies. The larger research-sources.zip also includes
the earlier manuscript, computational and formal dependencies. Programs are
source evidence: some exploratory searches are expensive; do not execute
all programs indiscriminately. Python certificates may require the same
standard scientific libraries or Z3 used by their source programs.

Mathematical source bytes are unchanged. source-manifest.json hashes every
member. Frozen research manifests and review receipts may also mention
private handoffs or omitted compiled executables: those historical hashes
remain intact, while this package's manifest is the authoritative membership
list. Private orchestration plans, handoffs, caches and executable binaries
are excluded. Scientific logs, counterexamples, failed conjectures and
candidate computations are preserved; inclusion never implies acceptance.

The current research objective remains matching bounds and directly
specified optimal inspections throughout the full rectangle domain. A
fixed-size expression using O(1) standard operations is the final numerical
goal, deferred until the bounds match. No arXiv submission is claimed.