The Dimension That Buys Nothing
A crystal cannot have five-fold symmetry. Everyone who has met the fact has also met its companion, that the permitted rotation orders are the same list in the plane and in space, 1, 2, 3, 4 and 6, and almost nobody says why the second thing is true. It is not a coincidence about three dimensions. Written in a lattice basis a symmetry is an integer matrix, so the question is which orders occur among integer matrices of finite order, and order n first fits in psi(n) dimensions, where psi(n) is the least total degree of a set of cyclotomic polynomials whose indices have least common multiple n. That number is even for every n above 2. So every odd dimension carries exactly what the even dimension below it carried, and not one thing more. Space obeys a plane's law because three is odd.
Slide the dimension below and watch the orders arrive in pairs of dimensions, never singly. Four is where the pentagon comes back.
Every rotation a lattice of dimension d can carry
Lit cells are permitted orders; gold cells are the ones this dimension adds. Click any cell to build the matrix that has that order. The grid stops at 120 only because a screen does; the arithmetic does not.
Drag from 2 to 3 and nothing happens. Drag from 3 to 4 and four new orders appear at once, the pentagon among them. Drag from 4 to 5 and nothing happens again. This continues forever, and it is the reason the crystallographic restriction reads the same in a wallpaper and in a mineral.
The whole pattern, to dimension 32
Odd rows are dim, and their last column always says nothing. That column is the finding. It is not an observation about small cases: psi(n) is even for every n from 3 up, so the column reads nothing at every odd dimension there will ever be.
Why the cost is not what you would guess
A rotation of order n in a single plane, extended to the rest of space, has the primitive n-th root of unity as an eigenvalue, and the smallest monic integer polynomial with that root is the n-th cyclotomic polynomial, of degree phi(n). So the natural guess for the least dimension is phi(n), and the guess is right for a while. It first fails at n = 15, where phi(15) is 8 but 6 dimensions are enough.
The reason is that a matrix of order 15 need not turn by a fifteenth of a turn anywhere. It can turn by a third in one plane and by a fifth in another, at the same time, and then it returns to where it started only after 15 steps, because 15 is the least common multiple of 3 and 5. A third of a turn costs 2 dimensions and a fifth costs 4, so the pair costs 6. A single fifteenth of a turn costs 8. Splitting is cheaper, and the arithmetic of how much cheaper is the whole subject.
The matrix itself
Its planes, turning together
step 0
Each block is a plane the matrix rotates, drawn in the lattice metric it preserves rather than in the screen's, which is why the polygons come out regular. The dot goes gold when that plane is back where it began. The matrix is the identity only when every dot is gold at once.
M and the lattice it preserves
M
G, the invariant metric
Every power, until it comes home
Two things in that panel are worth dwelling on. The first is that every entry of every one of these matrices is 0, 1 or minus 1. That is not a convenience of presentation. The blocks are companion matrices of Phi(p^a) and Phi(2p^a), and neither has a coefficient outside that set: Phi(p^a)(x) is 1 + x^q + x^2q + and so on up to x^((p-1)q) with q = p^(a-1), all coefficients 1, and Phi(2m)(x) = Phi(m)(minus x) for odd m above 1, which only flips signs. It matters below, when we go looking for these matrices by brute force.
The second is G. An integer matrix of finite order is not obviously a rotation of anything; it is just a shuffle of coordinates that happens to repeat. G is the proof that it is a rotation: sum the transpose-times-itself over all n powers and you get a positive definite integer matrix satisfying Mᵀ G M = G exactly, in whole numbers. G is the lattice, and M turns it. This is the bridge from an arithmetic question to a crystallographic one, and it is one line of algebra.
Both directions, in full
The statement is that GL(d, Z) contains an element of order exactly n if and only if psi(n) is at most d, where psi(n) is the minimum, over all sets S of divisors of n whose least common multiple is n, of the sum of phi(m) for m in S.
Enough. Take a minimising S. Stack the companion matrices of Phi(m) for m in S into one block-diagonal matrix. Each block has order exactly m, so the stack has order the least common multiple of S, which is n, and its size is the sum of the degrees, which is psi(n). Its determinant is plus or minus one because Phi(m) has constant term 1 for every m above 1. Pad with an identity block to reach any larger d.
Necessary. Let A be an integer matrix with A to the n the identity and n least. Over the rationals x^n minus 1 is squarefree, so the minimal polynomial of A is a product of distinct cyclotomics Phi(m) with m dividing n. A to the k is the identity exactly when every one of those m divides k, so the least common multiple of their indices is n. The minimal polynomial has degree at most d, and its degree is the sum of those phi(m), which is at least psi(n) by definition. So d is at least psi(n).
And the closed form. Write n as a product of prime powers. Any S with least common multiple n must, for each prime power p^a exactly dividing n, contain some element divisible by p^a. Group S by which prime powers each element covers: an element covering a set of prime powers has phi at least the product of their phi values, and a product of numbers each at least 2 is at least their sum. So the total is at least the sum of phi(p^a) over the prime powers of n, and taking S to be the prime powers themselves attains it.
The one place the argument leaks is the step where a product of numbers each at least 2 beats their sum, because phi(p^a) = 1 happens, for exactly one prime power: phi(2) = 1. So when 2 divides n but 4 does not, the factor 2 can be folded into another block for free, since phi(2m) = phi(m) for odd m, and psi(n) = psi(n/2). That single exception is the entire difference between psi and the naive sum, and it is why order 6 lives in the plane while order 5 does not.
Now the parity. For n at least 3, every prime power p^a exactly dividing n has phi(p^a) even, because phi(2^a) = 2^(a-1) with a at least 2 in the non-exceptional case, and phi(p^a) = p^(a-1)(p-1) with p odd. A sum of even numbers is even, and the exceptional case only ever reduces to a smaller odd multiple, so psi(n) is even for every n above 2. An odd dimension d therefore permits exactly the n with psi(n) at most d, and since psi(n) is never the odd number d, that is exactly the n with psi(n) at most d minus 1. The odd dimension buys nothing.
Found by brute force, not by formula
A proof is a claim about all cases and a search is a claim about a window, and the two are worth having side by side. So the window: take every integer matrix in a box and ask, in exact arithmetic, what orders actually turn up.
In dimension 3, every matrix with entries from minus 2 to 2 is 1,953,125 matrices, of which 135,408 have determinant plus or minus one. The orders that occur are 1, 2, 3, 4 and 6. Not one has order 5, and an order-5 matrix would have announced itself at its fifth power, long before any cutoff. The same sweep in dimension 2, over entries from minus 8 to 8, gives the same five orders.
In dimension 4, with entries only from minus 1 to 1, the box is 43,046,721 matrices, of which 10,340,736 are unimodular. Nine orders occur: 1, 2, 3, 4, 5, 6, 8, 10 and 12. Those are exactly the nine the theorem permits. Order 5 turns up 17,088 times.
That window was not chosen to flatter the result. It was chosen because of the fact noted above, that every minimal witness has entries in minus 1, 0 and 1, which means this smallest possible box was guaranteed in advance to contain a representative of every permitted order. It could not have missed one. What it could have done, and did not, is turn up a tenth.
The sweep's own numbers audit each other, which is a nicer check than it looks. Negating a matrix of odd order n gives one of order 2n, and the box is closed under negation, so the count of order-5 matrices and the count of order-10 matrices must be equal. They are: 17,088 each. For an even order, negation preserves the order, so those counts must be even, and they are. Order 2 is the one odd count, 5,435, because negation pairs its matrices up except for minus the identity, which has nowhere to go.
What the sweep settles, exactly: every matrix in these boxes was carried 400 powers, or else proved to have infinite order before then by a trace that grew too large for a root of unity. So no matrix in any box has an order anywhere between 1 and 400 other than the ones listed. What the sweep does not settle, and cannot: matrices outside the boxes. A finite-order integer matrix can have entries of any size, being conjugate to a small one. That is what the proof above is for.
What the kernel will sign
The easy half of the theorem is decidable one case at a time, so it has been decided. DimensionParity.lean exhibits, for every order permitted in dimensions 1 through 8, an explicit integer matrix of exactly that order, and closes 214 theorems by decide alone: for each order n, that M to the n is the identity, and that M to the n over p is not, for each prime p dividing n. Order then divides n and divides no maximal proper divisor of n, so it is exactly n.
The file has no imports, no Mathlib and no Batteries, so the only trusted component is Lean's type checker. Its axiom audit prints [propext] for every theorem and nothing wider: no sorry, no Classical.choice, and no native_decide, which would move the trust out of the kernel and into a compiled binary. The matrices in it are byte-for-byte the matrices this page draws, and the verifier parses the Lean source and checks that, so the kernel and the browser are looking at the same objects.
The hard half, that no other order occurs, is a real theorem and is not machine-checked here. It is proved on paper above and nowhere else in this repository. Saying so is the point of saying it.
None of this arithmetic is new, and here is exactly where it lives
The generalised crystallographic restriction is classical. Hiller gave it in The Crystallographic Restriction in Higher Dimensions (Acta Crystallographica A41, 1985); Bamberg, Cairns and Kilminster worked it into an elementary form in the American Mathematical Monthly (110, 2003), where it is connected to Goldbach's conjecture by way of which dimensions realise which orders; Kuzmanovich and Pavlichenkov cover the surrounding theory in the same journal (109, 2002). Every sequence on this page is already in the On-Line Encyclopedia of Integer Sequences. psi itself is A152455, and also A080737 with a different convention at n = 2. The orders new at each even dimension are the rows of A080738, their counts A080739, the running totals A080740, and the largest order in each dimension is A005417, whose own comment states the parity fact in as many words: maximal order of an element of finite order in GL(2n, Z) or GL(2n+1, Z).
What this page adds is not a fact but a way of standing next to one. The arithmetic is checked against 10,000 terms of A152455 rather than against its first line. The matrices are exhibited rather than asserted, with their orders recomputed in exact integer arithmetic in front of you and their invariant lattices printed. The multiplicities the 45 million matrices give are computed here, and this page found nothing to check them against, so they are made to check each other instead. And the easy direction is now something a kernel has signed.
Reproducing this
public/strata/the-dimension-that-buys-nothing/math.js is the module this page runs in your browser, and it is the module the verifier imports, so nothing you see here was computed anywhere else and copied in. research/the-dimension-that-buys-nothing/lib.mjs is a second, deliberately different implementation, which finds psi by minimising over the whole divisor lattice and uses no closed form at all. research/the-dimension-that-buys-nothing/sweep.mjs runs the exhaustive searches.
Run node verify-the-dimension-that-buys-nothing.mjs to check the lot: the two implementations against each other, both against seven OEIS b-files, the witnesses against exact integer arithmetic, the sweeps from scratch, and the Lean source against the matrices this page draws. It reports 75/75 and takes about two minutes, most of it the dimension-4 sweep; pass --fast to skip that one, which drops the count to 62/62. It ends by mutating this page and the module it runs on, checking that the checks go red, and restoring both to the same bytes.
You do not need this repository to do that, and you should not have to take our word for the OEIS comparison either. In an empty directory, fetch four files:
curl -sS --create-dirs -O https://artwaste.land/checks/verify-the-dimension-that-buys-nothing.mjs
curl -sS --create-dirs -o research/the-dimension-that-buys-nothing/lib.mjs \
https://artwaste.land/checks/research/the-dimension-that-buys-nothing/lib.mjs
curl -sS --create-dirs -o research/the-dimension-that-buys-nothing/sweep.mjs \
https://artwaste.land/checks/research/the-dimension-that-buys-nothing/sweep.mjs
curl -sS --create-dirs -o public/strata/the-dimension-that-buys-nothing/math.js \
https://artwaste.land/strata/the-dimension-that-buys-nothing/math.js
node verify-the-dimension-that-buys-nothing.mjs
It will fetch the seven b-files from oeis.org and this page from this address, because sequence data is data and goes to the Data Room rather than to the check publisher, and because a page's figures are worth checking against the page as published rather than against a copy we handed you. It prints every file it fetches and where from. Run from outside, the OEIS comparison is against OEIS, not against us, which is the comparison worth having.
Run bash research/the-dimension-that-buys-nothing/lean/verify.sh to have Lean typecheck the 214 theorems and print the axiom footprint of each. It needs Lean 4, which bash research/sorting-networks/lean/install-lean.sh installs in about a minute. The proof itself is DimensionParity.lean, served here rather than through /checks/ because it is written by research/the-dimension-that-buys-nothing/lean/generate.mjs and the check publisher holds generated files back on purpose. Download it next to the script and the script will run; without it the script says so and prints this same address.