Corrected card-position linking is sound under the listed fixed-output model.
Let D_A and D_B be the two full decks immediately before a shared plaintext
word, and define phi(D_A[q])=D_B[q] at every position q. This is a bijection
because each deck contains each card exactly once. Every action in the shared
word applies the same position permutation in both messages. Consequently
the relation D_B[q]=phi(D_A[q]) holds at every intervening state boundary.

Whenever paired observations emit x and y during that word, phi(x)=y. Thus
those two cards occupy equal positions throughout the entire word. Because
every action is invertible, the equality also holds at the incoming state.
The implementation's state index t means BEFORE action t (equivalently after
observed output t-1); the first action at i has output at state i+1. Linking
states i..i+length therefore includes exactly the incoming state and all
post-action states, with no extra preceding action.

Under D003, the first aligned E4 action is69, so its incoming observation is
E4[68], notE4[67]. This avoids the earlier strict30 boundary assumption.
The independent checker begins with unrestricted actions and positions and
does not import old strict30 pruning. Its30 physical fixtures retain23,544
true card positions and2,548 true cross-message position links. An explicit
fixture with differing incoming actions survives the corrected windows and
rejects the stronger false alignment.

Forward/backward pruning preserves every real key: each true card follows a
valid path in the transition relation, so every true action has path support.
Intersections across cards and true equal-plaintext links cannot remove that
action. The check ignores simultaneous all-different card positions and the
26-slot alphabet constraint. These omissions enlarge feasibility, so any
empty domain is still a valid exclusion, while a nonempty fixed point remains
only a necessary relaxation.

Independent literal transitions and boolean position sets reproduced all35
classifications. Thirty pairs fail action-only propagation; four more fail
position linking. The remaining pair(1,82) has the same fixed-point action
domains as the producer despite a different card visitation order. Its full
boolean position domains are saved in states_1_82.npz for later work.
