Squares tiled by pairwise unequal rectangles: the seven-piece column

Abstract

For integers n,m ≥ 1 let W^(*)(n,m) be the minimum total length of the interior segments of a partition of the square [0,n]² into m axis-aligned rectangles with integer corners and pairwise distinct (unordered) dimension pairs, when such a partition exists. Lago Gómez, who introduced this quantity as the two-dimensional core of a problem about tilings of a cube, proved W^(*)(n,m)=n+2(m-2) throughout the middle regime Tₘ₋₂ ≤ n<Tₘ₋₁ for 4 ≤ m ≤ 6, conjectured it for all m ≥ 4, and asked for the case m=7, where the middle regime is the finite range 15 ≤ n ≤ 20. We settle that range: W^(*)(n,7)=n+10 for 15 ≤ n ≤ 20, the upper bounds by explicit tilings and the matching lower bounds by two independent exhaustive searches. The same two searches determine the whole deep regime of the same column, W^(*)(n,7) for 5 ≤ n ≤ 14, where the value climbs in steps of +1, drops once at n=10, and reaches its middle-regime value three steps early, at n=12. Independently of any search we prove three structural facts about this tiling class: the identity W(T)+2n=Σᵢ(wᵢ+hᵢ) for every tiling; the piece-count ceiling 4m ≤ n²+6, which settles every non-existence entry of the table of W^(*) for 3 ≤ n ≤ 5 and gives the maximum piece counts 3,5,7 at n=3,4,5; and a layer-cake bound on the total semiperimeter, from which W^(*)(4,5)=10 and W^(*)(5,7)=19 follow with both halves proved. The last of these is the first exact value in the open column m=7 that does not rest on a search. Every theorem, proposition, lemma and corollary below is machine-checked in Lean 4, except where a heading marks part of it as resting in addition on exhaustive computation.

Open review

This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.

Archived files

1. Version 1 · current (opens in a new tab)

   Source snapshot 2026-08-30 15:34 UTC

   File fingerprint

   ae7360dcf784961467dc49d37463edecbd9113c3b3ea23d785739bb69b0f417c