29 May 2021

Found and written by Jonathan F. Waldmann. I was not able to find evidence of anyone discussing the topics of this sequence (especially not circle packing in the discrete plane) before, aside from note B10, however there is a chance that I overlooked previous work.

This spreadheet is a continuation of

my first elaboration on this problem,

and looking to provide more proofs and clarifications, as well as proving more terms.

Definition

Inverse of the supremum on the density of marked points ("dots") in ℤ² with pairwise minimum distance sqrt(n).

a(n) := 1 / sup( lim_k->inf : |A cut B(k)| / |B(k) cut ℤ²|, with the requirement that dist(y,z)>=sqrt(n) for all y,z in A; A subset of ℤ².)

By using a limit going out to infinity equally in all directions, we define the notion of a density despite the infinite measure of the discrete plane.

If this limit doesn't exist for a set of points, that set simply won't contribute to the set of possible limits for our supremum. Either way, I conjecture that defining the density via liminf or even limsup would lead to the same results.

Statements from my first sheet

How to read my illustrations

The discrete plane ℤ² is a grid of points arranged in a square pattern. In my illustrations, the coloured/framed squares are to be seen as centered at those points, with the visible gridlines marking the shifted grid (ℤ+0.5)² separating the points.

A green square marks a dot, a red square marks a point which can not be a dot, and a black frame highlights a shape of interest. Any squares not worth highlighting are white.

A yellow square marks an "aura" (as used for the proofs of a(8)=8 and a(10)=10), and an orange square marks one of a limited number of squares, at least one of which must lie outside of all auras.

Proofs by tiling the plane

In my first sheet, I often showed that a formation of squares tiles the plane, and immediately concluded upper or lower bounds about the density defined above. Here, I shall go into more detail about these proof methods.

If a formation tiles the plane, it also imperfectly tiles all increasingly large k-balls B(k) around the origin. As the area of a k-ball grows in proportion to k², the size of the rim with width c (c constant per tile) only grows in proportion to k.

This means that the percentage of untiled squares in B(k) is proportional to k/k², which tends to zero as k tends to infinity. Thus, showing the dot density in any repeating tiling of the plane indeed gives the limit for the densities in [B(k)].

In practice, this means that if a formation of size x tiles the plane and can hold at most y dots, the limit for the densities can at most be y/x,

and if a tiling of the plane with tiles of size x contains y dots in each tile, the limit for the densities in that particular dot pattern is exactly y/x, proving the supremum to be >= y/x.

Proofs using "auras"

"Auras" are a way to visualize and prove inherent facts about all dot patterns for a given index. As they are only used for highlighting, they can be defined at will, and only their properties need to be shown.

In the case of a(8)=8 and a(10)=10, I define auras to always be oriented in the same direction. I then show that the auras of two separate dots can not overlap, reserving the full area of an aura for just one dot.

From there, I illustrate the existence of additional squares that are not part of any aura, within a finite set of candidates. I then associate each dot with at least one such square, and each such square with at most one dot.

This lets me conclude a density of at most 1 dot per b+1 squares, where b is the size of the previously defined aura and 1 comes from the additional square.

Since those b+1 squares are shown to be within a limited range, this proves a density of at most 1/(b+1) (Verifying this step for the limit-based definition of density is left as an exercise for the reader).

Statements from the OEIS entry

Interpreting the problem as circle packing

To interpret the problem of finding the highest possible density as circle packing in ℤ², each dot can be defined as the center of a circle with diameter sqrt(n), i.e. radius sqrt(n)/2.

Since two circles of diameter sqrt(n) overlap if and only if their distance is smaller than 2*sqrt(n)/2, a circle packing with centers in ℤ² is valid if and only if the corresponding dot pattern is valid.

Thus, solving one problem solves the other. The sequence, however, can only be interpreted as the inverse frequency of circles, i.e. the inverse density of circle centers. Respecting the circles' area requires a different, fractional sequence.

Triangle area as an upper bound

I claim that the minimum area of an acute- or right-angled triangle with integer coordinates of pairwise minimum distance sqrt(n) is an upper bound for a(n).

Let ABC be such a triangle, achieving this lowest possible area. Let ABCD be the parallelogram formed by mirroring ABC along BC. We can tile the plane with ABCD by connecting AB with CD, and BC with AD, resulting in a square pattern.

By the choice of ABC, any two dots in the same triangle are at least sqrt(n) apart. Since ABC is acute- or right-angled, any two dots that don't share a triangle (e.g. A and D) are further apart.

We can therefore construct a valid set of dots by placing dots at the vertices of every triangle in our tiling of the plane. Counting out the triangles and vertices in a repeating portion of the plane, there is 1 dot for every 2 triangles.

Thus, any valid triangle for the area problem infers a valid dot pattern for the circle packing problem, with the inverse density equalling twice the triangle's area.

Conjectured equality with double the triangle area

It seems reasonable that for any given pattern of dots, it should be possible to divide the plane along those dots into right or acute triangles, or triangles of an angle range where the area can be proved to not be smaller (<120°?).

From there, an argument in line with the plane tiling proofs could be used to show the double triangle area to be a lower bound for the inverse dot density.

Generating terms for the triangle area sequence

A triangle is valid if and only if its pairwise point distances AB and BC satisfy:

|AB|>=sqrt(n)

|BC|>=sqrt(n)

|AB+BC|>=sqrt(n)

AB*BC<=0 (angle ABC is acute or right)

BC*(AB+BC)>=0 (angle BCA is acute or right)

(AB+BC)*AB>=0 (angle CAB is acute or right)

The doubled area of ABC can then be calculated via base*height.

Proof that a(n+1)>=a(n)

Any dot pattern that is valid at index n+1 remains valid at n. Thus, the supremum in the definition for a(n) is greater or equal that for a(n+1). Thus, the inverse is smaller or equal.

Proof that a(n+1)=a(n) if n is not the sum of 2 squares

Let A and B be two points on ℤ² with distance vector (x,y). By Pythagoras, their distance is sqrt(x²+y²). Thus, it is not sqrt(n) or between sqrt(n) and sqrt(n+1), and any dot pattern made invalid by their proximity at index n+1 remains invalid at n.

Proof that a(n)<=n if n is the sum of 2 squares

Let n be the sum of 2 squares x²+y². We tile the plane with squares, one square's vertices placed at (0,0), (x,y), (x+y,y+x), and (y,x). As explained above, this gives us a dot pattern of density 1/n.

Conjecturing a(n)>sqrt(3/4)*n

The height of an equilateral triangle is cos(60°)=sqrt(3/4) times the base. Since this ratio is an irrational number, no acute or right triangle can match or beat a base of sqrt(n) and a height of sqrt(3n/4) at the same time.

So if the conjecture about equality with the triangle sequence is true, this lower bound is true as well.

Proof of a(14)=a(15)=a(16)=a(17)=15

Lower bound:

We define the following non-rotatable "aura" around each dot (1).

By exhaustion, we see that the auras of any two dots can not overlap.

When attempting to tile the plane with this non-rotatable configuration,

at least one of the following two squares must be left open (2,3,4).

These two squares cannot overlap between different dots.

Thus, each dot must claim 15 squares for itself and only itself, forcing a density of 1/15 or lower.

Upper bound:

The following configuration of 15 squares tiles the plane while containing exactly 1 dot (5).

Note that a(16)=a(17), even though 16 is a sum of 2 squares (4²+0²).