Let \(S\) be a declared state space and let every legal move \(m\) be a reversible map \(S\to S\). A notation parser is correct only if it maps a token to one such map, with an inverse token satisfying

For a word \(w=m_1m_2\cdots m_k\), we read moves from left to right as in the complete layer-first method:

A replay test therefore records the initial state, the token list, the convention for viewing each face, and the final state. Replaying \(w\) followed by \(w^{-1}\) must return to \(s\); two displays are equivalent only after their resulting states, rather than their typography, agree.

The tetrahedron turn gives a short noncommuting trace. Starting at the recorded incidence position \((1,124)\), the \(H\)-move followed by the \(K\)-move reaches \((4,134)\). Reversing the order reaches \((3,234)\). The two words are therefore different maps, even though each move separately has order three. A player can check this by stepping through the two token lists and comparing the final records.

The cube face turn fixes the frame and turns only the chosen layer. The global shape map \(q(x,y,z)=(y,-x,z)\) sends the four \(z=1\) corners around a four-cycle; the local puzzle move restricts this map to that layer and fixes the opposite layer pointwise. This is a useful display test: a global rotation of the drawing is not the same operation as the local puzzle move, and the unturned center must not move merely because the picture was rotated.

A reproducible solve has five recorded stages: identify the state in the chosen coordinates; state the target condition; choose a move word; replay it from the recorded state; and check the target and preserved invariants. The layer-first method supplies a human version: each stage fixes information and uses a stabilizer for what remains. The computer account supplies a search version: a returned word is an upper bound, while a projected-distance table gives a lower bound.

These certificates should be reported separately. A valid replay shows that the word reaches the target. A short word improves an upper bound in the named metric. A shortest-path claim additionally needs an exhaustive search or a matching lower bound. The distinction also applies to a scramble: scrambling and spectra requires the move law and length before a distributional claim can be evaluated.

The worked replay and projected lower bound makes this separation concrete: one fixed-frame scramble is replayed by its inverse, a projected search supplies a lower bound, and the ten-token word supplies an upper bound. The example closes the replay loop while leaving the all-state method and any optimality claim at their stated scopes.

A small interface can make the contract visible without pretending to replace it. It can reject an unknown token, show the affected pieces, step through a word, undo by inverse tokens, and compare the final state with a target. It can also display parity, orientation, or subgroup coordinates as diagnostics, provided each coordinate is tied to the declared state model.

An animation illustrates a claim; the move map and replay log are the evidence for it. The interface should therefore expose the convention, the exact token sequence, and the before-and-after state so another person or program can reproduce the check. The existing Rubik's Cube resources collect notation, methods, and demonstrations; the companion FRAP repository can later host executable versions of these checks.