n = 3 provedO=
Proven
- optimal
- exact
Bounds
0
Solved: the verified bounds meet.
Results in the register
T-058 V3 C3 wand125 after Tokoharu, Daniel · 2026-09-29 · 100 cases
Rectangle-certificate ceiling
α·UB(n)proved for ..100;B·UB(n)on 64 grid rows
upper: replayed here; lower: replayed here
—
not rigid, numerically checked, numerical multiprecision
Evidence: E-translation-escape-not-rigid
Scope
Square 1 of the retained witness (witness id 2) translates 1 along (0, 1) with the packing still valid, so the configuration admits a non-trivial feasible motion; 2 of its 3 squares do. Every constraint is exactly affine in the slide parameter, so the arithmetic carries no linearization error, but the coordinates are the witness's own finite-precision transcription: this settles the retained configuration, not the true optimum. Rigidity and optimality are independent, and this bears only on the former.
4 evidence entries
E-kingbird-upper-register, E-basic-grid-upper, E-basic-area-lower, E-side2-center-lower
- [Kingbird] record catalogue
- [Friedman DS7] lower bound proof
- [Alpert et al. 2023] context
- [Alvarado-Garduño–González 2025] context
— solved
. Established by an elementary counting argument.
The full proved optimum is a configuration space rather than one privileged pose: two labelled cycles reduce to one quotient interval.
The packing
The record catalogue does not picture : no arrangement has ever been found that beats the trivial grid, so the grid is still the best known packing. That is a statement about what has been searched, not a proof.
The lower bound
Established by an elementary counting argument.
The complete optimal configuration space
Exp-014 excludes genuinely rotated side-2 packings and enumerates the full axis-aligned space. The labelled space is two circles, the unlabelled space one circle, and the quotient the interval . Its exact quotient and stratum map is a permanent known-answer control for later landscape visualizations.
Verification Code
The programs behind this case’s verified bounds, by their evidence.
The code column says how the code that ran stands to the code its producer used.
VERIFIERS.md says what each program is and whose it is.
| bound | evidence | run | code | programs |
|---|---|---|---|---|
| verified lower | E-side2-center-lower |
replayed here | producer’s code | V-optimal-moduli (first-party) |
| verified upper | E-basic-grid-upper |
replayed here | independent | V-check-basic-bounds (first-party) |