Shubnikov symmetry, neutron diffraction, and the helimagnet as the dm³ helical attractor
Chapter 16 arranged atoms in space. This chapter arranges something the atoms carry but space alone cannot see: their spin. A crystal can be perfectly ordered chemically and still hide a second, independent order — the pattern of atomic magnetic moments woven through the same lattice. Mapping that hidden order is magnetic crystallography, and it forces one new symmetry the ordinary 230 space groups never needed: time reversal. Reverse the direction of time and an electron's spin flips. That single extra generator, written $1'$, is the operator $K$ of the dm³ chain acting on the magnetic degree of freedom.
The chapter runs in the now-familiar two halves. First a compact primer on how magnetic order is classified (Shubnikov groups) and measured (neutrons, not X-rays). Then the dm³ bridge — and this time the bridge is unusually tight: a helimagnet is literally the dm³ helical attractor, its spins riding the limit cycle $\Gamma = \{r=1\}$, its commensurability set by the canonical period $T^\ast = 2\pi$. Those statements are formalized in a new file, MagneticLattice.lean, and the honest inventory is given at the end. Along the way there is an experiment you can run at any age with a handful of magnetic spheres.
sorry in MagneticLattice.lean; three hard ones are named and left open.
Ordinary crystallography positions atoms with one of the 230 space groups. Magnetic crystallography keeps all of that spatial symmetry and adds one antiunitary generator, $1'$, which reverses the arrow of time and hence flips every spin. Combining $1'$ with the spatial operations enlarges the catalogue dramatically:
| Level | Ordinary | Magnetic (Shubnikov) | Composition |
|---|---|---|---|
| Point groups | 32 | 122 | 32 + 32 grey + 58 black-white |
| Space groups | 230 | 1651 | 230 + 230 grey + 1191 black-white |
The three families have a clean physical reading. Colourless (type I) groups contain no $1'$ at all — a fully ordered magnet. Grey (type II) groups contain the bare $1'$: time reversal is a symmetry, so no moment can survive it — these are the paramagnets, the disordered phase. Black-white (types III–IV) groups contain $1'$ only in combination with a spatial operation (a rotation or translation) — these are the antiferromagnets and their relatives, where the spin pattern is invariant under "flip and shift." For still more intricate order that never quite repeats with the chemical cell, one passes to spin space groups and magnetic superspace, the setting for incommensurate structures and the recently recognised altermagnets.
shubnikov_census ($230+230+1191 = 1651$) and magnetic_point_census ($32+32+58 = 122$). Time reversal is an involution, tr_involution ($1'\!\circ 1' = \mathrm{id}$), and tr_fixed_iff_zero proves its only fixed moment is zero — the grey-group paramagnet. All proved without sorry.
X-rays scatter off electron clouds. They read the chemical structure beautifully and are almost blind to magnetic order, because the charge distribution barely notices which way a spin points. To see the spins you need a probe that carries a spin of its own. The neutron is exactly that: electrically neutral, so it ignores charge, but carrying a magnetic moment ($\mu_n \approx -1.913\,\mu_N$) that couples directly to the atomic moments. Neutron diffraction is the gold standard for deciding whether a material is ferromagnetic, antiferromagnetic, or helimagnetic, and for measuring the magnetic unit cell. Where the chemical cell alone would forbid a Bragg peak, an antiferromagnet's doubled magnetic cell produces one — a reflection that appears only to neutrons.
A complementary probe, resonant elastic X-ray scattering (REXS), tunes polarized X-rays to an element's absorption edge to extract element-specific magnetic structure. And because refining a magnetic structure means fitting group theory to diffraction data, the field runs on specialised software: FullProf (neutron/X-ray Rietveld with magnetic phases), JANA2020 (commensurate and incommensurate magnetic superspace), and MagStREXS (magnetic structure from REXS data).
The neutron/X-ray split is the physical shadow of the dm³ idea that the important structure is often the one the obvious probe cannot see. X-rays see the manifest lattice; neutrons see the hidden phase. In the framework this is exactly the role of the contact form $\alpha$: the chemical periodicity is the base, and the magnetic order is a section over it that only the right (spin-carrying) instrument resolves. The antiferromagnet's "flip-and-shift" invariance is the operator $K$ — conjugation — made physical.
Collinear order comes in two flavours. A ferromagnet has every moment parallel: its magnetic cell equals its chemical cell, and it carries a net moment. An antiferromagnet alternates $+,-,+,-$: its magnetic cell is doubled, and the net moment cancels. But the richest case is helimagnetism, where the moment rotates by a fixed pitch angle $q$ from site to site, tracing a spiral:
$\displaystyle \mathbf{S}_n = \big(\cos(nq),\ \sin(nq)\big).$
Write that down and the bridge announces itself. Every helimagnetic spin has unit length — it lives on the circle $r=1$, which is precisely the dm³ limit cycle $\Gamma$. The pitch $q$ is the discrete image of the dm³ angular velocity $\dot\theta = 1$; the spiral closes into a repeating pattern exactly when $q$ completes a whole turn, $p\,q = 2\pi = T^\ast$, after $p$ sites. When $q/2\pi$ is irrational the spiral never closes — the incommensurate helimagnet, winding forever around $\Gamma$ without repeating.
heliSpin_on_limit_cycle: $\cos^2(nq) + \sin^2(nq) = 1$ — every helimagnetic spin lies on $\Gamma = \{r=1\}$. Proved.ferromagnet_is_zero_pitch: $\mathbf{S}_n = (1,0)$ at $q=0$ — ferromagnetism is the degenerate helix. Proved.heliSpin_period: if $p\,q = 2\pi = T^\ast$ then $\mathbf{S}_{n+p} = \mathbf{S}_n$ — commensurability is governed by the dm³ period. Proved.magnetic_bridge bundles these with the collinear facts (afm_period_two, afm_cell_neutral) and the time-reversal involution into one proposition — proved without sorry.
The interactive lattice below places $37$ spins on a centered-hexagonal patch — the same $\mathrm{cHex}(3)$ colony from Chapter 16 — and lets you switch between the three orders. Ferromagnet ($q=0$), antiferromagnet (flip-and-shift), and helimagnet (a live pitch winding around $\Gamma$). Watch the net moment vector at the corner.
ferromagnet_is_zero_pitch.
heliSpin_on_limit_cycle).
Here is the whole chapter in your hands. Take a set of small magnetic spheres — the kind sold as desk toys. Each sphere is a tiny magnetic dipole, a north and a south. Pour a pile onto a flat surface and let them settle. They will not scatter randomly and they will not form a square grid. They snap, every time, into a hexagonal arrangement: each sphere ringed by exactly six others.
Now try to defeat it. Try to lay the spheres out in a spiral, or a square, or any pattern you like. Within a few beads the structure fights back and relaxes into the hexagon. People find this genuinely counterintuitive — surely, with your own hands, you can arrange them however you want? You cannot, not for long. The geometry forces it. Six equal circles fit exactly around a seventh with no gap and no strain ($6 \times 60^\circ = 360^\circ$), and the dipole attraction pulls every sphere into that lowest-energy, most-tightly-packed frame. The spiral you intended collapses into the lattice the packing prefers.
Two effects conspire, and it is worth separating them. The first is pure geometry: six equal circles are the most that fit around one, so dense packing alone already prefers the hexagon — this is the $\mathrm{CN}=6$ we met in Chapter 16, true of oranges and ball bearings with no magnetism at all. The second is what makes the assembly snap rather than merely settle: because each sphere is round it is free to rotate, so its north–south axis turns until the poles of neighbouring spheres align into closed magnetic loops. Those loops minimise the field energy, and a square or a spiral would force the field into strained, high-energy angles. Geometry says "hexagon is tightest"; the magnet says "and I will pull you there myself." That second voice — the dipole doing the work — is the operator $F$ made physical.
1. Drop the spheres loosely and watch them self-assemble. Count the neighbours of an interior sphere — you will find six.
2. Deliberately build a spiral or a square block. Add beads and watch the edges reorganise toward the hexagonal frame.
3. Build one central sphere and add a ring around it. It closes at exactly seven — one plus six — the same $\mathrm{cHex}(1)=7$ that opens the colony in Chapter 16.
What you are seeing by hand is the coordination number $\mathrm{CN}=6$ of two-dimensional close packing, and the isoperimetric optimum $\sqrt3/24 > 1/16$ that Chapter 16 proved: the hexagon wins on area per boundary, so equal attracting bodies fall into it. The magnet adds the dipole that makes the assembly happen on its own — the physics doing the operator $F$ for you.
The demonstration is the reason the G6 Crystal of Chapter 16 is hexagonal and the reason a helimagnet's spins settle onto a circle here: in both cases a field of equal, interacting units is driven to the packing the geometry already prefers. The magnet just lets you feel the operator pull the structure into place.
The four base operators map onto magnetic order directly:
| Operator | Magnetic realisation | Lean anchor |
|---|---|---|
| C · Contact | The exchange coupling that defines which neighbours talk — the contact form on the spin lattice | heliSpin def |
| K · Conjugate | Time reversal $1'$ and the flip-and-shift of antiferromagnetism — cell doubling | tr_involution, afm_period_two |
| F · Fold / fixed point | The ferromagnetic aligned ground state — the single well | ferromagnet_is_zero_pitch |
| U · Unfold | The helimagnetic spiral unfolding onto the dm³ limit cycle $\Gamma$ | heliSpin_on_limit_cycle, heliSpin_period |
Time reversal also has a purely dynamical face. In the smooth dm³ system the transverse Lyapunov exponent is $\mu_{\max} = -2$; sending $t \mapsto -t$ flips the sign of every Lyapunov exponent, turning a contracting direction into an expanding one. The magnetic $1'$ and the dynamical time reversal are the same generator seen in two languages — spin flip and stability flip. The signs $\mu_{\max}<0$ and $T^\ast>0$ are carried over and proved (mu_max_neg, T_star_pos).
Sixteen facts are formalized without sorry in MagneticLattice.lean; three hard obligations are named and left open. Because the file is new, its proofs are elementary Mathlib (trigonometric identities, parity, arithmetic) — stated below and slated for the same kernel CI that gates the rest of the repository. None depends on the Structural Hypothesis, so none carries an (under SH) caveat.
| Claim | Lean name | Status |
|---|---|---|
| Magnetic space-group census $230+230+1191=1651$ | shubnikov_census | ✓ Formalized |
| Magnetic point-group census $32+32+58=122$ | magnetic_point_census | ✓ Formalized |
| Magnetic order enlarges the census ($230<1651$) | magnetic_exceeds_ordinary | ✓ Formalized |
| Time reversal $1'$ is an involution | tr_involution | ✓ Formalized |
| Only zero moment is $1'$-invariant (paramagnet) | tr_fixed_iff_zero | ✓ Formalized |
| Ferromagnet period 1; antiferromagnet period 2 (cell doubling) | ferro_period_one, afm_period_two | ✓ Formalized |
| Antiferromagnetic cell is neutral; flips site to site | afm_cell_neutral, afm_flips | ✓ Formalized |
| Helimagnet spins lie on $\Gamma=\{r=1\}$ | heliSpin_on_limit_cycle | ✓ Formalized |
| Ferromagnet = zero-pitch helix | ferromagnet_is_zero_pitch | ✓ Formalized |
| $p\,q = T^\ast = 2\pi \Rightarrow$ $p$-periodic | heliSpin_period | ✓ Formalized |
| dm³ invariant signs $\mu_{\max}<0$, $T^\ast>0$ | mu_max_neg, T_star_pos | ✓ Formalized |
| Bundled proved core | magnetic_bridge | ✓ Formalized |
| M1 · Kramers degeneracy $T^2=-1$ (spin-½) — needs SU(2)/projective rep of time reversal | kramers_degeneracy_placeholder | ○ OPEN |
| M2 · incommensurate helimagnet is aperiodic — needs irrationality of $q/2\pi$ + equidistribution | heliSpin_incommensurate_aperiodic | ○ OPEN (sorry) |
| M3 · neutron magnetic structure-factor selection rule — needs scattering theory | neutron_selection_rule_placeholder | ○ OPEN |
sorry), or the neutron selection rule (M3). And the hand experiment of §17.4 is a demonstration of close packing, not a proof that dipolar spheres must minimise to the hexagon — that energy-minimisation statement is its own open problem. Every gap is named.
Chapter 16 gave the crystal its shape; Chapter 17 gives it its spin. Together they are the two orders a single lattice can carry — position and moment, space group and Shubnikov group — and the framework treats them as $C$-and-$F$ versus $K$-and-$U$ faces of the same operator chain. Upstream this depends on Chapter 10 (the smooth dm³ system and its helical attractor, the $\Gamma$ that the helimagnet realises) and on Chapter 16 (the hexagonal packing the magnet experiment makes visible). Its narrative companions are the magnetism chapters on Curie and Faraday. The formal content lives in MagneticLattice.lean, beside G6Crystal.lean and DM3Bridge.lean.
afm_period_two and afm_cell_neutral, explain in three sentences why the magnetic peak appears at half the reciprocal-lattice spacing of the chemical peaks, and why a charge probe is blind to it.
heliSpin_period proves a helix with $p\,q = 2\pi$ is $p$-periodic, while heliSpin_incommensurate_aperiodic (open) asserts irrational $q/2\pi$ never repeats. Pick $q = 2\pi/5$ and $q = 2\pi/\varphi$ (golden angle). For each, describe what a neutron diffraction pattern would show, and explain which one equidistributes on $\Gamma$.
MagneticLattice.lean, the statement "a spiral of $N$ dipolar spheres has higher energy than the hexagonal packing of the same $N$." Identify precisely which term (dipole energy, packing constraint) makes it hard to prove, and why the hand demonstration is convincing even though the theorem is open.