Scramble a picture with the kicked rotor, then run the same rule backwards. Floating point brings back only the islands of stability. A lattice version brings back every pixel.
A rod spins freely and is kicked at regular intervals. Each kick changes its momentum by an amount that depends on its angle; between kicks the angle drifts forward.
p ← p + K sin x, x ← x + p
Both wrap around, so each pixel of the picture is a state on a torus. Undo the drift, then the kick, and you are back where you started.
A double carries about sixteen digits. In the chaotic sea a rounding error grows about a hundredfold every ten steps, so after roughly fifty steps each way the first pixels miss home.
Points on the islands of stability drift apart slowly, so they return. The picture that comes back is a map of where the motion is chaotic. This is Loschmidt's echo.
On a 256 × 256 grid, round the kick to a whole number of cells and keep everything else exact. A kick then slides each column by whole cells, and a drift slides each row. Neither can make two cells collide, so each step is a reshuffle of the 65,536 cells.
Nothing is merged or lost, so running backwards is exact at any K and any number of steps.
The lattice step is 11 AArch64 instructions forward and 12 backward. Each point is two bytes, so wrapping at 256 is free. In HOL Light, against s2n-bignum's formal model of ARM, the exact object bytes are proven to compute this map for every input array and every 256-byte kick table. The backward routine is also proven to undo the forward one. The proof covers the machine code, not the page's loop or its pixels. This page runs a JavaScript port whose output was checked, step by step, against the verified code.
lattice_fwd:
cbz x1, 2f
1: ldrb w3, [x0] // x
ldrb w4, [x0, #1] // p
ldrb w5, [x2, x3] // kick[x]
add w4, w4, w5 // p + kick[x]
add w3, w3, w4 // x + p
strb w4, [x0, #1] // low byte = mod 256
strb w3, [x0], #2
subs x1, x1, #1
b.ne 1b
2: ret
New: Do, Undo, Repeat. Four programs undone ten times in a row, including the 1982 Vancouver Stock Exchange index and the 1991 Patriot clock.
Source, proof and video pipeline: github.com/BenKnill/lattice-echo · Episode 1: the symplectic camel