The crystallographic restriction in every dimension: GL(N, ℤ) has an element of order m if and only if ψ(m) ≤ N
A Lean 4 development of the crystallographic restriction in every dimension. For a positive integer m let psi(m) be the sum of phi(p^k) over the prime powers p^k exactly dividing m, except that the prime power 2 contributes 0 (phi is Euler's totient; psi(1) = psi(2) = 0, psi(3) = psi(4) = psi(6) = 2, psi(ab) = psi(a) + psi(b) for coprime a, b; OEIS A080737). Theorem (Vaidyanathaswamy 1928; Hiller 1985; a proof in Kuzmanovich-Pavlichenkov 2002; Theorem 1 of Bamberg-Cairns-Kilminster 2003): for N >= 1, the group GL(N, Z) of invertible integer N x N matrices has an element of order m >= 1 if…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-15-000017
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-15-000017/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-15-000017/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'