MODEL CONVENTION AND PRIOR-ART AUDIT

For a deck with distinct cards and a base R mapping old positions to new:
  ordinary p emits the old card at R^{-1}(p);
  the off-top exception emits the old card at R^{-1}(0).
Hence immediate unique decoding requires distinct ordinary slots and excludes
ordinary p=0 when the exceptional type is present. At most one off-top-only
type is allowed under this immediate-decoding definition. This does not purport
to rule out codes decoded with future lookahead or context.

An ordinary action repeats the previous output precisely when p=R(0).
An exceptional action repeats it precisely when R(0)=0. Thus M002 normalized
to R(j)=j+1 has ordinary slots 0 and 1 unavailable for two DIFFERENT reasons:
0 conflicts with the exceptional type, whereas 1 always causes a double.
For M003 with a fixed top, no exceptional event can occur after a recorded
previous output in a no-doubles message. A first message operation is different:
the initial top is unobserved, so an otherwise double-making instruction could
occur only there. Solvers that forbid p=1 globally choose a structural
no-doubles model, or the stronger assumption that the first marker is governed
by the same admissible instruction alphabet; absence of observed doubles alone
does not justify forbidding a type used only at message starts.

This last distinction affects exact scope. No-doubles within observed messages
forbids p=R(0) at indices >=1, but not necessarily at index0. Keeping the global
ban is a reasonable explicit model branch, not a logical consequence of the
finite corpus. Model records should also specify u != v for a genuine exception.
M002's standard conjugacy to the successor cycle is valid because the entire
base is a single cycle and conjugation fixes the distinguished top0. Arbitrary
numeric ciphertext labels impose no additional restrictions.

PRIOR-ART MATRIX (local immutable source snapshots)

Lymm37/eye-messages wiki, Deck-Cipher.md lines5-7 and
Proof-that-GAK-is-uniquely-reversible.md lines7-11:
Defines immediate reversibility by distinct output source positions and
structural avoidance of unchanged top. These are established conventions,
not new results here.
https://github.com/Lymm37/eye-messages/wiki/Deck-Cipher
https://github.com/Lymm37/eye-messages/wiki/Proof-that-GAK-is-uniquely-reversible

mvelzel/eye-vibe src/eye_mystery/sparse_deck.py lines1-8,59-117:
Each instruction performs a top swap followed by a fixed non-top swap;
identity non-top rules allowed. Rank0 top swap is itself identity. Therefore
M002 is REPRESENTABLE as a subset: hidden rule at rank0 is (u,v); every other
hidden rule is identity. This base-free module alone corresponds to R=identity,
where the exception would always double after an earlier recorded output.
https://github.com/mvelzel/eye-vibe/blob/0ba8ca9ed4660d74f68abafa3e4743935222e885/src/eye_mystery/sparse_deck.py

deck_base_generic.py lines152-200 and optimize_sparse_deck.py:
General fixed-base sparse decoder applies selected top swap then rank-specific
hidden swap. The same subset relation holds when a full-cycle base is supplied.
The source's base array convention is inverse to the lab's old->new convention;
that is representational, but matters when comparing exact keys. The hidden
decoder initializes the card-coordinate map naturally rather than searching
all initial orders. optimize_sparse_deck.py starts a standard chosen base,
learns arbitrary rank-specific hidden transpositions by coordinate descent,
and permits an initial rule at rank0. It does NOT exhaust all initial decks.
https://github.com/mvelzel/eye-vibe/blob/0ba8ca9ed4660d74f68abafa3e4743935222e885/scripts/optimize_sparse_deck.py

docs/research-log.md lines75-149:
6,806 affine bases;8,430 standard bases; formulaic hidden rules; then arbitrary
one-coordinate hidden-swap optimization. One/five planted active-rule recovery
worked for a specific base while26 active rules failed. Report explicitly warns
against extending that calibrated negative to arbitrary unknown bases. None
of these are a complete test of arbitrary initial-order M002.

docs/research-log.md lines724-767; scripts/solve_sparse_crib_z3.py:
Exact SAT/UNSAT results concern particular proposed plaintext prefixes and
specific chosen bases, with multiple fixed hidden swaps per plaintext letter.
Concrete witnesses demonstrate compatibility for broad sparse models; they do
not establish M002 feasibility for the complete corpus. A broad-family UNSAT
for an additional crib would not exclude all possible plaintexts.

Conclusion: the one-exception construction is not a new cipher family.
No exact full-corpus, arbitrary-initial-deck M002 exclusion was found in the
inspected implementation/log. This is a bounded prior-art finding, not proof
that no community researcher has tested it. No external downloads or messages
were made in this audit.

CONTROLS
control_models.py materializes every permutation on3..6 positions, every
unordered pair of distinct nonzero positions, and every ordinary slot.
All7,998 base/pair fixtures and47,106 ordinary-action checks agree with the
source-position identities. Deliberately allowing ordinary0 produces an
output collision in all7,998 fixtures. Identity-state testing is sufficient
because arbitrary relabeling of distinct card labels preserves equality.
