Or, perhaps more appropriately, “A” Steinhaus conjecture, he/she (I’m guessing Hugo, so he. Perhaps I’ll look into it) seems to have made a couple. This conjecture (theorem) also goes by the name “The Three Gap Theorem”, or “The Three Distance Theorem”. Which is all a little annoying, I think. It makes looking for references 3 times as hard, I reckon. But it’s a pretty cool result, and I’m glad Dave Richeson brought it to my attention via his blog post on Three cool facts about rotations of the circle.
To write down the theorem, I’ll first introduce the notation for the “decimal part” of a real number, defined as , being the largest integer no bigger than . Since I’ll be thinking about positive , it is the value of if you ignore digits to the left of the decimal point. This seems to be fairly common notation. Anyway…
The theorem goes something like this:
Theorem: Suppose that is irrational. Let be a positive integer bigger than 1, and consider the points for . These points partition the interval into subintervals. If the distances of these subintervals are calculated, there will be either 2 or 3 distinct distances.
The circle comes in by thinking of the interval as a circle with circumference 1. To help visualize it, Dr. Richeson made a pretty sweet GeoGebra applet.
I think this is a pretty initially surprising theorem. My initial shock has worn off just slightly, now that I’ve played with pictures and dug through a proof, but it’s still a wonderful result. I mean, irrational values are supposed to do weird things, right? Their multiples should bounce all over the place in the unit interval. And yet, they partition the circle into just 2 or 3 differently-sized gaps? Crazy talk. Also, the theorem as stated above isn’t as strong as it could be… you can say a bit more about the distances. I think I’ll talk more about it in another post.
I started reading about this theorem, after Dr. Richeson’s post, in the paper by Tony van Ravenstein. As I was reading the proof I got hung up on some details, and found that consulting the paper by Micaela Mayero got me over those difficulties. The paper by Mayero is essentially a formal proof written for the Coq formal proof system, so it sort of makes sense that details will be pretty fully explained in it. Either way though, it’s really not a long or particularly difficult proof (you mostly play with some inequalities).
I may return, in a future post, to talking about the proof, and I’ll certainly come back and tell you as I read more about further consequences and generalizations, and whatever else I find in some other papers I’m planning on looking at. But for now, let me mention a result in van Ravenstein’s paper. He proves that in going from the picture with points to the picture of points, the -th point will break up the oldest of the intervals with the largest length. The “age” of an interval is pretty intuitive. If a particular interval, say between multiples and comes in when there are points, and those two points are still neighbors when there are points, then the age of that interval, at stage , is (plus 1, if you want, it doesn’t matter).
To help picture what’s going on, I made an interactive Sage notebook. If you have an account on sagenb.org, or have Sage installed on your own computer and want to just copy my code over, you can look at my code and play with the notebook. I had hoped that publishing my notebook there would let you play with the interactive bits without you needing an account, but no dice. Sorry.
To give some sense of my notebook, and the theorem, I’ve got some pictures for you.
First, let’s take or so (basically 1 minus the golden ratio, nice and irrational). I’ve set up my notebook so that points travel from 0, at the top of the circle, clockwise, because that’s how it was done in the papers I was reading, and I thought it’d be less confusing. So here’s the starting picture, when there’s just the points 0 and :
Along the outside of the circle, at each dot, I list which multiple it is. The “newest” dot is magenta, instead of red (probably not great color choices… mess with my code and make your own ). In the center of the circle I list the lengths of the intervals, in decreasing order. Along each interval, I also write the age of that interval, and color-code the text to the list of distances. I’ve decided to always have the largest length be red-orangeish, the smallest length blue-ish, and the middle length (if there is one) green-ish.
In the picture above, the interval on the left is clearly the oldest of the longest length intervals, so the theorem is that when we add another point, this interval will get broken up by that point. Which is clearly true in this case.
Here’s another picture, using the same , but slightly more points, showing that three gaps occur:
And, finally, 20 points:
Here’s a picture using a starting a little bigger than 0.6, showing 20 points:
I like how the points seem to develop in clusters (also evidenced by Dr. Richeson’s app).
I guess that’s probably enough for now. Like I said, I’m hoping to have plenty more to say about things related to all of this soon…
Postscript: I want to make a few shout-outs. I thought putting them at the end of this post might interrupt any sort of flow of the article (if there is any) a little less.