51 SEDAPS.Beta

Each live queue exposes its first card. Highest strength wins; the winner appends its own card first, then the others clockwise. Strength is rank, with A = 1, then suit ♠ < ♥ < ♦ < ♣.

Under this three-queue played-turn rule, every endpoint has at most four legal predecessors. This endpoint attains four. Two fixed-width bits therefore suffice in the worst case for one predecessor choice, given the endpoint and shared conventions. A known move count lets the same reconstruction run backward along a trajectory.

Here, the first bit identifies the winning queue: 0 means H1, 1 means H0. The second records whether H2 participated: 0 means no, 1 means yes.

Reachability update (v0.4.1): the original constructed witness cannot arise from 17–17–17. Each queue must be a prefix of at most 17 cards followed by legal capture packets; its H0 needs at least 44. The turn-85 endpoint is reached by a complete recorded replay. Of its four legal predecessors, only 00 occurs at turn 84 from a 17–17–17 deal (certified: two independent returns). While three queues are live, every queue length is ≡ 17 − t (mod 3). The lengths of 01 (36, 14, 1) and of 11 (33, 17, 1) fall in three different classes mod 3, so no fair deal reaches either at any turn. A complete backward search rules out 10 at turn 84: its deepest history reaches turn 66. The turn count matters: fair deals do reach 10 at turns 24, 27, 30 and 33 (four frozen certificates). Without the turn count, 00 and 10 both survive and the first bit alone recovers the past. Four remains the true maximum among reached states: at five certified presents (turns 32, 35, 41, 50 and 53) all four pasts come from different 17–17–17 deals. One step back there are four pasts; all the way back there are many more histories. Exactly 484,731,472 deals reach the turn-32 present, by a proved counting formula checked deal by deal. Terminal self-loops are excluded.

The prefix invariant alone is necessary, not sufficient; the v0.4 verdicts add the time-aware shape lemma and an exhaustive search. A game that never ends falls into a loop. Every loop a dealt game has reached keeps two live queues, and its length is a multiple of 52. With two queues left, the rule is War with the winning card placed first. For an odd deck its cycles alternate winners (Spivey 2010), which forces a period that is a multiple of n + 1 (see research update v0.4.1). Loops that keep all three queues live do exist at 51 cards (proved). A construction gives them for every multiple of 3 from 12 cards up; one at 51 cards returns after 180 turns, which is not a multiple of 52. None exists for 11 cards or fewer, or for 13; 14 and the other sizes above 13 not divisible by 3 are untested. No equal deal reaches the loops this construction gives: while three queues are live, the three sizes stay congruent mod 3 if they start that way, and theirs never are. Whether a 17–17–17 deal can reach any three-live loop is open. Only a "synchronised" loop could be reached, and complete searches find none at 9, 12 or 15 cards. These are exact card-model results; there is no zero-data test or RH inference.

This disclosed example was found in one seeded, bounded run. Move through the complete queue states below. Turn 0 is the 17–17–17 deal. The verifier checks every move and predecessor index.