Four Short of a Square

The grid gives s(k² − 4) ≤ k; the work is the other direction. For k ≥ 8 it is done for all k at once.

How much each case rests on:

For k ≥ 8: our exact checker, the reviewed k² − 3 code, certifies the 9 × 9 box, and wand125's separately written one re-checks its tilted squares (§04); Lean carries that to every k (§05). Nothing here is peer reviewed.

Friedman's survey conjectured that s(n² − c) = n implies s((n+1)² − c) = n + 1 (Conjecture 1). For c = 4 the conclusion now holds for every n that matters: at n = 3 the hypothesis fails (s(5) = 2 + 1/√2 < 3), at n = 4 the conclusion s(21) = 5 holds, and from there s(k² − 4) = k for every k ≥ 5. So the deficit-4 case of Conjecture 1 holds whatever the still open s(12) turns out to be.

As far as we know, no exact value of s(k² − 4) for any k ≥ 4 was known before September 2026. This project proved s(32) = 6 (26 September), s(21) = 5 and s(45) = 7 (27 September) and s(60) = 8 (28 September), one box at a time. wand125 proved s(77) = 9 first, on 1 October, by inserting a band into our s(60) cover and checking it with our checkers. The cases k ≥ 10, and k = 9 by a second route, are new here. Since s never decreases, this also re-derives s(k² − 3) = k for k ≥ 5.

The measure has the three parts of the k² − 3 family, on the 1/5-grid with no weighted points, now with corner size and band width 3:

• Corner modules on the 3 × 3 square at each corner: 176 segment pieces plus area density on [14/5, 3]², the same module reflected at all four corners.
• A periodic wall band of width 3: 110 segment pieces per unit period plus area density on the strip from 14/5 to 3, repeating with period 1.
• Lebesgue interior: mass equal to area on [14/5, k − 14/5]².

Why one box is enough. As for k² − 3: the band carries exactly its own area per period, so all the saving sits at the corners, and a unit square, less than 2 wide at any angle, can be shifted by whole units along each axis into [0,9] without changing what it captures. With corner size R = 3 this works for every k ≥ 2R + 2 = 8 (the k² − 3 family, with R = 2, used the 7 × 7 box).

Zero margin. The wall squares, and many limits as the tilt goes to zero with the square's edges on grid lines, capture exactly 1. Away from those, the linear program that chose the masses demanded growth in proportion to the tilt (factor 0.08 up to 3°). The float optimum without that demand is about 1.13 per corner; the exact family keeps 1.0739, so 0.074 per corner above the 1 needed.

The claim, Valid9: every closed unit square in [0,9]² captures mass at least 1 under μ₉. By the square's symmetries it is enough to take centres in [0, 9/2]² and tilts up to 45°.

At zero tilt all 1,600 one-sided corner limits were computed exactly: minimum exactly 1, reached at 208. This step is also kernel-checked in Lean over the whole box (§05).

At positive tilt the program of the k² − 3 certificate, byte for byte the same files apart from an assert and a dump flag, subdivides the placements until every piece is proved with exact rational arithmetic, using the same exact lemma at the tight placements.

Reviews. The checker code was reviewed by six agents for k² − 3, and wand125's separately written checker corroborated that certificate. This run was given to three more adversarial review agents (2026-10-03), each with its own code: an attack on the cover (all 111,392 tiny-tilt limits exactly, millions of poses near the tight sets and at random, local minimisation: nothing below 1; the smallest local minimum away from the exactly-tight sets is about 1 + 4.5·10⁻⁵); the run record (coverage reconstructed independently, all area-density leaves re-proved, about 0.9 million exact masses, none below 1); and the statement chain and literature. None found an error in the mathematics. The Rust checker zmx2 certifies all but 4,844 boxes, all at tilts below 0.05°.

A second checker. On 6 October 2026 wand125 published an exact re-check of ValidTilt9, the tilted part of Valid9 (§05), with the separately written checker that had corroborated Valid7 (valid7-independent-check, commit c561dbb3, records in release records-tilt9-v1): centres in [0, 9/2]², no symmetry used, 28,350 root boxes, none uncertified. jlevy/squares reviewed it: its region contains ValidTilt9's, the source's record check reports every root certified, and it found no defect. The register records it as reported evidence; the case itself (T-081) is not yet register-verified, and we have not re-run it here.

theorem SquarePacking.Bentz4.bentz4_of_validTilt9 (ht : ValidTilt9) :
    ∀ k : ℕ, 8 ≤ k → minSide (k ^ 2 - 4) = k

The hypothesis ValidTilt9 says that every closed unit square in [0,9]² with centre in [0, 9/2]² and tilt in (0°, 45°] captures mass at least 1 under the 9 × 9 box file, taken verbatim: exactly the region the positive-tilt run of §04 covers.

Everything else is checked by Lean's kernel: the measure for every k and that for k = 9 it is the box file; the total k² − 4D < k² − 4; the move of any unit square into the 9 × 9 box; the reduction by the square's symmetries (the box file's symmetry checked by the kernel); the zero-tilt case, by exact corner limits over the whole box; the scaling argument; and the grid. Standard axioms only, no sorry, no native_decide. The tilted run itself is not in Lean: its lemmas are proved on paper.

• For k ≥ 10 everything rests on the 9 × 9 box: our run of search/qx2_zm.py, and Lean for the rest. Its code was reviewed and corroborated for k² − 3, but this cover is new (larger box, wider band, corner pieces on the band's end lines). wand125's separately written exact checker has re-checked its tilted squares (§04); that check is reviewed but not yet replayed or register-verified.
• The reviews were done by AI agents, not by outside mathematicians. Nothing here is peer reviewed.
• The Lean proof is conditional on ValidTilt9 (§05).
• k = 5, 6, 7 rest on their own bundles, with the trust stated in §01; only s(32) = 6 is hypothesis-free in Lean.
• The fast check in the bundle does not recompute any positive-tilt leaf; verify.sh --full does (§07).

The bundle is s12/certificates/k2m4: its README says what checks what. verify.sh takes about 20 seconds: hashes, the cover's total and symmetry, that the family rebuilds the box file, the Lean data, the zero-tilt check, and the run record's structure and coverage, but no positive-tilt mass bound. verify.sh --full re-runs qx2_zm.py (about 226 CPU-hours) and compares root for root. The 9 × 9 box file is K4_k008_box9.txt.