n = 1 · Case Records · The Squares Project

n = 1 provedO=R

$s (1) = 1$

The best packing known for 1 square, side

1

012

\sqrt{n}

\sqrt{n} + 1

Proven

$s (1) = 1$

optimal
exact
rigid

Bounds

Best known packing

$1$

Construction: —
Source: [Kingbird]
Evidence: E-kingbird-upper-register

Verified upper bound

$1$

The reported value, verified here.

Evidence: E-basic-grid-upper

Reported lower bound

Kind: perfect square
Evidence: E-basic-area-lower

Verified lower bound

$1$

The reported value, verified here.

Evidence: E-basic-area-lower

Gap

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 $n = 1$ ..100; B·UB(n) on 64 grid rows

Verification

upper: replayed here; lower: replayed here

—

Rigidity

locally rigid, verified, exact algebraic

Evidence: E-perfect-square-tiling-rigid

Scope

This record's side is verified above and below at exactly 1, so its 1 unit square of total area 1 sits in a 1 by 1 container of area 1. The packing is a tiling with no slack anywhere, so no square admits any feasible motion. This is global rather than local, and holds for the exact configuration rather than for a materialized approximation of it. It says nothing about s(n) beyond what the tiling itself shows.

Evidence and sources

3 evidence entries

E-kingbird-upper-register, E-basic-area-lower, E-basic-grid-upper

[Kingbird] record catalogue
[Friedman DS7] survey

In the frontier survey On GitHub

$s (1)$ — solved

$s (1) = 1$ . Established by triviality (a perfect square).

The packing

Found by an unrecorded author, via an unrecorded method.

The lower bound

$1$ is a perfect square, so the $1 \times 1$ grid is optimal and the area bound $\sqrt{n}$ is already tight.

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-basic-area-lower`	replayed here	independent	`V-check-basic-bounds` (first-party)
verified upper	`E-basic-grid-upper`	replayed here	independent	`V-check-basic-bounds` (first-party)