n = 3 provedO=

s(3)=2

The best packing known for 3 squares, side 2,
2
123
1.7322.732
nn+1

Proven

s(3)=2

  • optimal
  • exact

Bounds

Best known packing

2

Construction
grid
Tilt angles
0∘
Source
[Kingbird]
Evidence
E-kingbird-upper-register
Verified upper bound

2

The reported value, verified here.

Evidence
E-basic-grid-upper
Reported lower bound

2

Kind
counting
Source
[Friedman DS7]
Evidence
E-side2-center-lower
Verified lower bound

2

The reported value, verified here.

Evidence
E-side2-center-lower
Gap

0

Solved: the verified bounds meet.

Results in the register

Verification

upper: replayed here; lower: replayed here

—

Rigidity

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.

s(3) — solved

s(3)=2. Established by an elementary counting argument.

The exact quotient map of optimal configurations for three unit squares.

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 n=3: no arrangement has ever been found that beats the trivial ⌈3⌉=2 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 D4×S3 quotient the interval [0,1/2]. 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)