W7-1: the table of lines 75, 179, 265, 597 — informal proof, revision 2 (STUCK)

• Machine (line 75, start A): 1RB1RC_1LC1LE_1RD0RA_1LB0RA_0LD1LF_1LD---.
• The same table from the other starts: line 597 (start B, mirrored), line 265 (start C), line 179 (start D, mirrored). Table key (ledger canon): 1LB1LC_1RC1RD_1LE0LA_0RE1RF_1RB0LA_1RE---.
• Written for: all four strings at once. One argument on the line-75 table, with one opening run per start (§5).
• Nearest kill: #3 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB--- (Skelet 1-like Class 2). §8 is the lemma plan against it.

State of the argument (2026-10-14, revision 2).

• Proved (modulo the mechanical cell bookkeeping that check_proof.py replays):
• the configuration family and the 7 sweep lemmas (§1–2);
• 15 macro rules with exact step counts (the 13 of revision 1, plus the two far-end rules FAR-0-PLUS-EVEN and FAR-0-PLUS-ODD), and the list of outside cases (§3);
• the region counter calculus (§4): one counter step per half-cycle (C1), ruler counts (C2), the boundary events and the merged state (C3), the death dance (C4), the climb automaton with its two modes (C5), and the reflection lemma in both branches (C6);
• the four opening runs into the common family K(c) = c | 66 | 18 | 64, and the start-parametric lemma (§5);
• the legal-event lemma: every configuration that satisfies the condition J has a rule, so the machine does not halt in that half-cycle (§6.2).
• Open, fatal: O1. No inductive invariant. J is left in five one-step ways, and some J-members halt (2 + 1 # 2 halts after 186 steps). §6.3 lists what an inductive J* must contain.
• New in revision 2, and the reason for STUCK (§6.4): the far end decides halting by a race. Each time the first field is used up, the far-end prefix passes through shapes such as 1 + 0 | 0 | x. From there, the order of two events decides whether the orbit stays inside the rule set or leaves it, sometimes into the halting pattern + 0 +. That order depends on the far region's direction, a parity that the whole history sets.
• 24 of 300 perturbations of line 75's own configuration at 10^13 leave the rule set before 10^100 steps. 22 of them do it at the far end, between 10^14 and 10^85 steps, and 3 of those reach the halting pattern + 0 +.
• The four real orbits pass their windows. They meet no outside case to 10^150 steps.
• So J would have to predict a pseudo-random far-end race forever. Under the cryptid protocol, this is flag-and-stop: status STUCK*, with a decision card (decision.json).
• Nothing here is a kill.

0. Machine and the halting transition

F is entered only by E1 → 1LF, and E only by B1 → 1LE. So the machine halts exactly when B reads a 1 whose two left neighbours are 1 1 (B1, then E1, then F1).

The four listed strings are this table under a renaming of the states (check_proof.py §E checks each map):

Renaming and mirroring do not change halting. So each listed line halts iff the line-75 table halts from the blank tape in the start state of that row. The rest of this file works with the line-75 table and a start state s ∈ {A, B, C, D}.

1. The configuration family

A field of size f ≥ 0 is the word

[f] := 1 (01)^f          (2f+1 cells; f gaps of one 0 between its 1s)

Fields are joined by separators, the runs of 0s between two fields:

A token list is T = f_1 s_1 f_2 s_2 … s_{k−1} f_k. The last field L := f_k is the growing end. The family is the set of configurations

X(T) := 0^inf [f_1] s_1 [f_2] … s_{k-1} [f_k] 0 0 1 1 D> 0^inf

with the head on the blank cell right of 0011, in state D. The machine enters X(T) by C0 → 1RD at the right end. A half-cycle is the run from one X(T) to the next configuration of the form X(T′). Some half-cycles pass through other D:R configurations that are not of the form X(T) (the re-pairings do).

2. Sweep lemmas

Each lemma is an exact run on the cells shown. The head never reads a cell outside them, except that the last move may land on the cell named x. Notation: D> u means the head is in state D on the first cell of u.

Corollaries (induction on f with S).

• Even field: for f even,

1 (01)^f D> 0 --> 1 D> 0 1^(2f) in 4f steps

• Odd field: for f odd, with x the cell left of the field,

x 1 (01)^f D> 0 --> D> x 1^(2f+2) in 4f+4 steps

So the leftward sweep converts fields into runs of 1s. After an even field it lands on the field's own leading 1 and crosses a pipe by P. After an odd field it lands on the separator itself, out of phase.

The ODD half-cycle, composed. Let the scan (below) stop at an odd field j whose left separator is a pipe, and let d := f_{j−1} ≥ 1.

1. R enters the sweep.
2. L and every even field between j and L are swept (even corollary), each followed by P across its pipe. Each pipe leaves one single 0, a hole, behind.
3. j is swept (odd corollary). The head lands out of phase, on the second cell of the pipe left of j.
4. T writes 0 on the last cell of d (d loses one unit) and turns the head into state A.
5. The A sweep rewrites the 1-runs as (10)^m. H rebuilds a 00 pipe at every hole, and E closes the right end with 0011 D>.

Cell bookkeeping: d ends 2 cells shorter, every field and pipe from j to the field before L is rebuilt 2 cells further left, and the closing 0011 D> lands 4 cells further right than before. So L gains 6 cells: L grows by 3. Total: 6S + 12n + 12 steps, where S is the sum of the fields from j to L and n is their number (§3).

All other rules are compositions of the same lemmas, plus the variants at + and # (the sweep hits 1 1 or 000 instead of 00). check_proof.py §A checks the seven lemmas and both corollaries (f = 0..29). §B checks every composed rule on random instances, with exact tokens and step counts.

3. Macro rules

3.1 The scan

The sweep reads fields from L leftwards. It passes an even field followed by a pipe on its left (even corollary + P). It stops at the first of:

• (a) an odd field j;
• (b) a + or # to the left of an even field;
• (c) the far end, when every field is even and every separator is a pipe.

Let S be the sum of the fields from the stopping field to L, and n their number. At a stop of type (b), the stopping field is the one right of the separator. For the two OVERFLOWs, S and n are over all fields.

3.2 The rules

Each rule is an exact run from X(T) to X(T′). check_proof.py §B checks 18 cases × 150 random instances. It also checks exhaustively every token list with ≤ 4 fields, values 0..5 and the three separators on which a rule applies: 26,681 instances, 53 more than in revision 1 (the far-end 0 + lists). The other 4,194 are outside cases. All agree with direct simulation, tokens and step counts.

Every rule takes at least 8 steps.

The re-pairings are BOUNCE, the two OVERFLOWs and FAR-0-PLUS-EVEN. In each of them, every field right of the stop gains 1, and the stopping field gains 2 (3 for FAR-0-PLUS-EVEN, where the 0 is absorbed). All their separators become +, the old L becomes an ordinary field, and a new L = 1 is born. The two FAR-0-PLUS rules are new in revision 2. In both of them, S and n are over the fields right of the 0.

3.3 Outside cases

A token list on which no rule of §3.2 applies is outside:

The proof has to keep the orbit out of (o1)–(o8). It never uses what the machine does there. (o5) and then (o8) occur once in each opening run (§5.1), before the base.

4. The region counter

4.1 Regions

Cut the token list at every + and #. The pieces are regions. The last region, the one that contains L, is the active region. Every other region is frozen until the active region reaches its left end.

Write the active region as g_1 | g_2 | … | g_n | L, with left boundary X ∈ {+, #, far end}. Define

b_i := g_i mod 2,  b_L := L mod 2
B_i := b_1 + … + b_i  (mod 2),  for i = 1..n
P   := B_n + b_L      (mod 2)          (the region's direction)
N   := sum_i B_i 2^(n-i)               (the region's counter, 0 <= N < 2^n)

The depth of g_i is n − i. The field next to L has depth 0.

4.2 Counter lemma

Lemma C1. Suppose the scan of a half-cycle stops inside the active region and does not reach X. That is, (N, P) is neither (0, 0) nor (2^n − 1, 1). Then the half-cycle acts on exactly one field g_i and adds 3 to L, and

P = 1:  N' = N + 1,  and g_i has depth v2(N+1)
P = 0:  N' = N - 1,  and g_i has depth v2(N)
P' = P

If g_i ≥ 1, the rule is ODD and g_i loses 1. If g_i = 0, the field dies: by DEATH (pipes on both sides), DEATH-MERGE (+ on its left), DEATH-FAR (it is the first field), or the outside cases (o5) (# on its left) and (o6). After a death, N and P are those of the new active region (C4, C5). The formulas above are for ODD.

Proof. Let j be the last odd field (L counts as field n+1). The rule flips the parity of g_{j−1} and of L. So it flips B_{j−1}, …, B_n and leaves P unchanged.

• j ≤ n. Then b_L = 0, so B_j = … = B_n = P, and B_{j−1} = 1 − P, because b_j = 1. For P = 1 the bits from depth n−j+1 down to 0 read 0 1…1 and become 1 0…0: that is N + 1, and its carry depth is n − j + 1, the depth of g_{j−1}. For P = 0 they read 1 0…0 and become 0 1…1: that is N − 1.
• j = n + 1 (L odd). Then g_n flips, which is bit 0: N ± 1 with v2 = 0.
• j = 1 would mean B_1 = … = B_n = 1 with b_L = 0, which is (2^n − 1, 1). No odd field at all would mean (0, 0). Both are excluded. ∎

A field is reached by a carry only when every bit below it equals P and its own bit is 1 − P. A field of value 0 has b = 0, so the region's top field g_1 (B_1 = b_1 = 0) can die only in an up-run (P = 1).

Corollary C2 (runs and ruler counts). Suppose no field dies. From (N, P = 1), the region runs 2^n − 1 − N half-cycles to the top. From (N, P = 0), it runs N half-cycles to the bottom. In a run between counter values N₀ and N₁, the field at depth u loses one unit for every x in the run with v2(x) = u: that is, once per odd multiple of 2^u. The fields are budgets, and their parities are the bits of a binary counter, whose direction P is fixed for the whole run. A full run of 2^m − 1 steps takes 2^(m−1−u) from the field at depth u. (check_proof.py §D: exhaustive on bit patterns for n ≤ 10, and on random regions of the abstract map.)

4.3 Boundary events

At the end of a run, the scan reaches X. At the bottom (N = 0, P = 0), every field of the region is even and L is even. At the top (N = 2^n − 1, P = 1), g_1 is odd, the other fields are even, and L is even.

The top field can also die in an up-run (C1). Its death is DEATH-MERGE when X is + (and is (o6) if g_2 = L), DEATH-FAR at the far end, and (o5) when X is #.

Lemma C3 (merged state). Consider one of these events: a boundary event at a + (PLUS, ODD-PLUS, PLUS-MERGE-1), or a DEATH-MERGE of the top field. Afterwards the new active region is

H, x*, e_2, …, e_m | L

Here x is the field the event changed or created, and H is the list of fields left of x in its region. Every e_i is even, and L is odd. So its counter is

(H's bits) B* B* … B*,     P = 1 − B*

where B is the B-bit of x:

After PLUS-FAR-1, the region has no H and no x*. All its fields are even, so N = 0 and P = 1. After DEATH-FAR, the first field is odd and the others are even, so N = 2^n − 1 and P = 0.

Proof. Use the event's row of §3.2 and the parities above.

• At the bottom every old field is even. PLUS-MERGE-1 adds the even g_1 and 1 to y.
• At the top, ODD-PLUS makes the odd g_1 even.
• In DEATH-MERGE, j is odd and every field right of j is even (C1).
• In every case L was even and gains 3, so it ends odd. Then every bit after x repeats B, and P = B* + 1. ∎

4.4 The death dance

Lemma C4. Suppose a field at depth w ≥ 1 of the active region is 0 when a carry reaches it, and has pipes on both sides (a | 0 | b …). Then DEATH gives a # b …, and the new active region (b … L, w fields) has N = 2^w − 1 and P = 0. If no further field of that region dies, the next 2^(w+1) half-cycles are

(2^w - 1) x ODD,   HASH-ODD (a -> a-1),   (2^w - 1) x ODD,   BOUNCE

Field b (depth w − 1) loses exactly 1 in each of the two runs. So it reaches the BOUNCE as b − 2, and the BOUNCE gives it back as b. A field at depth u < w − 1 loses 2^(w−u) in all. If a = 0 is the first field, HASH-FAR-0 replaces HASH-ODD: 0 # is removed and the region runs up to the far end, where OVERFLOW-ODD follows.

Proof. At the carry, the bits at depths below w are all equal to P, and the dying field's bit is 1 − P (C1). The dying field is even, so its B equals that of the field before it. After DEATH, b is the only odd field among b … L−1, and L has turned odd. Then C2 and §4.3 give the sequence. ∎

The dance is legal if b ≥ 3 (b is odd at the DEATH, so b − 1 ≥ 2 and b − 2 ≥ 1) and a ≥ 1 or a is the first field.

A death inside the dance. If a field of the region b … L dies before the BOUNCE, C1–C3 still describe every step, with the inner death first. The inner death leaves a second #, and C6 reverses the region (when its climb ends at a PLUS). At the far end this can give BOUNCE with a = 0 as the first field. The result 0 + (b+2) + … is no longer an outside case: the climb then ends with FAR-0-PLUS-EVEN or FAR-0-PLUS-ODD (§3.2). This is the reviewer's case 22 | 59 (half-cycles 6082–8108). Interior inner deaths still leave two #, and only a budget clause can rule them out (§6.3).

4.5 Re-pairing and the climb automaton

After a re-pairing the list is

W  s_1 + s_2 + … + s_r | 1

Here W is Z + for BOUNCE (Z = a, the field left of the old #) and for OVERFLOW-EVEN (Z = the prefix 1, the first field). W is empty for OVERFLOW-ODD and FAR-0-PLUS-EVEN. Every singleton s_i is odd and ≥ 1, because the re-pairing adds 1 to an even field, 2 to an odd one, or 3 to the even field after a far-end 0.

Lemma C5 (climb). While the active region g_1 | … | g_m | L has + or the far end on the left of g_1 (and no field dies):

• Mode. Every g_i with i ≥ 2 is even and L is odd (C3 with H empty). If g_1 is odd, the next run is a down-run from 2^m − 1 (mode D). If g_1 is even, it is an up-run from 0 (mode U). Either way it has 2^m − 1 ODD steps, and the field at depth u loses 2^(m−1−u) (C2).
• Stage end in mode D, at the field z left of the +:
• z ≥ 3 (a singleton): PLUS, and z − 2 is the new g_1. It is odd, so the climb stays in D.
• z = 1 with + on its left: PLUS-MERGE-1, and y + g_1 + 1 is the new g_1. When y is a singleton it is even: the climb switches to U. The singleton y is absorbed, so the next stage again has m fields.
• z = 1 as the first field: PLUS-FAR-1.
• Stage end in mode U: ODD-PLUS takes 1 from z and 1 from g_1, and z − 1 is the new g_1. For a singleton z it is even, so the climb stays in U.
• If z = 1, then z − 1 = 0. The next up-run reaches it after 2^(m−1) − 1 steps (with m the new number of fields), and DEATH-MERGE merges y, 0 and g_2 into y + g_2 + 1. For a singleton y this is odd: the climb is back in D.
• The end of the climb is the event on Z, or the far end:
• BOUNCE: the last stage ends on Z = a − 1 (after HASH-ODD). In mode D this is PLUS (a − 1 ≥ 2), so a loses 3 in all. In mode U it is ODD-PLUS (a − 1 ≥ 1), so a loses 2 in all.
• OVERFLOW-EVEN: in mode D, PLUS-FAR-1 removes the prefix. The region then runs up (N = 0, P = 1) and OVERFLOW-ODD follows. In mode U, ODD-PLUS makes the prefix 0. DEATH-FAR removes it 2^(n−1) − 1 steps later, and the down-run that follows ends in OVERFLOW-EVEN.
• OVERFLOW-ODD, FAR-0-PLUS-EVEN: the last stage ends on s_1. The full region then runs to the far end: down (OVERFLOW-EVEN next) after a PLUS, up (OVERFLOW-ODD next) after an ODD-PLUS.

So a climb starts in D, because s_r = L + 1 and the new L = 1 are odd. It stays in D while the singletons it meets are ≥ 3. It switches to U at a singleton 1, that is, after a re-paired field equal to 0. It goes back to D only through a singleton 1 met in mode U.

In mode D with no singleton 1 (revision 1's case), stage t has t fields and the field at depth u loses 2^(t−1−u) in it. A field keeps its depth once it has joined. So over a climb of T stages, the field at depth u loses 2^(T−u) − 1, plus 2 at its own PLUS.

Proof. Induction on the stages. C3 (H empty, B* = parity of the new g_1) gives the mode after each event, C2 the run, and §4.3 the stage-end event. ∎

On the orbit. The U-branch occurs on the four orbits (4 of the 200 climbs to 10^13). One example is the reviewer's: at step 1.53·10^6 (line 75), OVERFLOW-EVEN of 38 | 42 | 0 | 168 | … gives 1 + 39 + 43 + 1 + 169 + …. The climb then meets the singleton 1: 1 + 39 + 43 + 1 + 166 | … becomes 1 + 39 + 210 | … (PLUS-MERGE-1, mode U). Next come ODD-PLUS on 39, ODD-PLUS on the prefix (1 + 37 | … becomes 0 | 36 | …) and DEATH-FAR, as C5 says. check_proof.py §H replays C5 stage by stage, with the exact token list at every stage end:

• after every re-pairing on the four orbits to 10^13: 200 climbs and 1,108 stage ends. In 60 of these climbs a field dies inside a stage, mostly in the long OVERFLOW climbs. C5 is checked up to that death, and C1–C3 then take over;
• on 3,000 random climbs with singletons equal to 1, prefixes and +-bounded Z;
• on the reviewer's reproducer 9 + 5 + 1 + 7 + 5 | 1 (PLUS, PLUS-MERGE-1, ODD-PLUS, then a death inside the next stage).

4.6 Reflection

Lemma C6. Take a death a | 0 | b … at depth w in a run of direction P. Suppose the dance (C4) and the climb (C5) complete without further deaths. Then the enclosing region comes back with the dying field removed and the w + 1 re-paired fields (the w fields right of the dying field, plus the old L) in its place. H is the list of bits above a. Before the death the counter is

P = 1:  N = H 0 0 1^w        P = 0:  N = H 1 1 0^w        (B_a = 1 − P)

The climb ends on a in one of two ways:

• D-end (PLUS on a − 1): a loses 3 and its bit flips. The direction is reversed:

N' = H P^(w+2), P' = 1 − P

• U-end (ODD-PLUS on a − 1, after a singleton 1 in the climb): a loses 2 and its bit is kept. The direction is kept, and the counter is rewound to the start of the block:

N' = H (1−P)^(w+2), P' = P

Proof. Apply C3 to the event on a. HASH-ODD has flipped a's bit once. PLUS keeps it and ODD-PLUS flips it back. Every field after a is even, and L is odd. ∎

So a death is a mirror (D-end) or a rewind (U-end). On line 75's orbit to 10^13, all 31 deaths whose dance and climb complete have a D-end, and check_proof.py §H checks C6 on each one. The 32nd has a nested death. The U-end appears in random climbs (522 of 3,000 meet PLUS-MERGE-1), and on the orbits after OVERFLOW-EVEN (above).

Nested deaths. C4–C6 assume that no second field dies before the climb ends. On line 75's orbit to 10^13, 1 of 32 interior deaths breaks this: a second death comes 2,695 half-cycles into a depth-9 dance and climb. C1–C3 still describe every step. Only the closed-form sequences of C4–C6 need the hypothesis, and they then apply to the inner death first.

5. Starts, opening runs, and the start-parametric lemma

5.1 Opening runs (direct simulation, check_proof.py §E)

The four bases are one family:

K(c) := X(c | 66 | 18 | 64),     c in {47, 51, 73, 71}  (all odd)

The opening passes once through the outside cases (o5) and (o8): X # 0 | 53 | 70 → X <4> 53 | 73 → (ODD) X <4> 52 | 76 → X + 1 + 53 + 77 | 1, with X = 0, 4, 26, 24. That is why the argument starts at K(c) and treats the opening as a finite computation.

From each base, check_proof.py §E checks every D:R event predicted by the abstract map against direct simulation of the start, to 3·10^7 steps by default. Before this, the observe stage compared the exact accelerated simulator with direct simulation at 10^10 on all four starts. The oracle-checked runs (data/abstract_runs.md) then match the abstract map on every non-ODD/PLUS event to 10^13 for all four starts.

5.2 Start-parametric lemma

Lemma SP. Let T₂ arise from T₁ by adding 2e (e > 0) to one field, so T₁ is the smaller copy. Suppose that field of T₁ is not the value tested by the applicable rule with value ≤ 1: not d of ODD/DEATH or ODD-PLUS, not x of PLUS, and not a of HASH-ODD. Then T₁ and T₂ take the same rule. The results again differ in one field only, by 2e, with T₂ the larger: the same field, the field it was merged into, or its re-paired copy (+1, +2 or +3 on both).

Proof. Every rule tests parities, which an even offset does not change. Besides that, it tests only the values ≥ 1 / ≥ 2 / = 0 / = 1 listed. Since T₁ is the smaller copy and its field passes the test, the larger copy passes the same test. Every rule is affine in each field, with coefficient 1. ∎

So from the bases, the four orbits take the same rules in the same order, with one field offset by 47 − c, until the smallest copy of that field is tested at value ≤ 1 at the far end. check_proof.py §F: the four rule sequences agree on all 2,208,574 half-cycles to 10^13, and Lemma SP holds on 12,435 random paired half-cycles. The abstract runs to 10^16 (data/abstract_runs.md §3) give the first divergences:

• line 75 leaves the others at 5.98·10^14: a far-end 0 | 0 | 117 …, DEATH next to a 0 first field, then HASH-FAR-0 at 7.07·10^14;
• line 597 leaves 265/179 at 2.13·10^15 (DEATH-FAR);
• lines 265 and 179 agree on every event to 10^16.

After that, the far ends differ. So the four proofs would share everything but the far-end bookkeeping, and that bookkeeping is exactly where §6.4 finds the race.

6. Invariant

6.1 Statement of J (revision 2)

J(T) is the conjunction of:

• (J0) every field ≥ 0, and L ≥ 1;
• (J1) every separator is |, + or #;
• (J2) at most one #. If there is one:
• every separator to its right is a pipe (so # is the active region's left end);
• the field right of it is ≥ 1;
• the field left of it is ≥ 1, unless it is the first field;
• (J3) the field left of any + is ≥ 1, unless it is the first field (a far-end 0 +, revision 2). If it is 1, it is the first field or has + on its left;
• (J4) the separator left of L is | or #;
• (J5) no + 0 | L.

6.2 Legal-event lemma (proved)

Lemma LE. If J(T), then a rule of §3.2 applies to T. In particular, the machine does not halt between X(T) and X(T′), and X(T′) is reached in at least 8 steps.

Proof. Go through the outside cases of §3.3:

• (o1) x = 0 at a +, not first: excluded by (J3). A first x = 0 is FAR-0-PLUS-EVEN.
• (o2) x = 1 with a pipe or # on its left: excluded by (J3).
• (o3) y + 1 + L: excluded by (J4).
• (o4) a = 0 not first: excluded by (J2).
• (o5) DEATH with # left of d: d would be the field right of #, which is ≥ 1 by (J2).
• (o6): excluded by (J5).
• (o7) d = 0 at +, not first: excluded by (J3). A first d = 0 is FAR-0-PLUS-ODD.
• (o8): excluded by (J1).

Every other configuration is covered by a row of §3.2. ∎

check_proof.py §G confirms LE exhaustively: every token list with ≤ 5 fields, values 0..4 and separators | + # that satisfies J has a rule (39,644 lists).

Reduction. Suppose J holds at every X(T) reached by the macro steps from K(c). Then the machine never halts from that start. Each step X(T) → X(T′) is an exact run of at least 8 steps (§3.2, LE), so multistep_nonhalt + progress_nonhalt_cond apply with P := J (as in #3).

6.3 What is open: O1, an inductive J* ⇒ J

J is not inductive. The reviewer's one-step catalogue (all 100,575 J-states with ≤ 5 fields and values ≤ 5) shows that J is left in exactly five ways. check_proof.py §G recomputes it on the LE domain and finds the same five classes:

Revision 2's J3 admits a far-end 0 +, so the old exit 0 # 1 → 0 + 3 | 1 is no longer an exit.

J-members that halt. 2 + 1 # 2 satisfies J and halts after 186 steps (direct simulation). Its path is HASH-ODD 2 + 0 # 5, then BOUNCE 2 + 0 + 7 | 1, then ODD 2 + 0 + 6 | 4, then (o1). The reviewer found 1,675 such halting members among the 9,150 J-states with ≤ 4 fields and values ≤ 5.

What J* must contain. The dance and the climb are deterministic given (N, P) and the field values (C4, C5). So the local clauses can be written exactly, as functions of the counter:

• (B1) at a # with right region (N, P, w fields), the field b right of # must be ≥ 1 + (the number of carries still due to depth w − 1 before the BOUNCE). That is 2 at the DEATH, as C4 says. This closes exit (c).
• (B2) the field a left of # must be ≥ [P = 0] + 2 if the climb will end in mode D (PLUS needs x ≥ 2), and ≥ [P = 0] + 1 if it will end in mode U (ODD-PLUS needs d ≥ 1). Here P is the phase of the # region: P = 0 means HASH-ODD is still due. Alternatively, a is 1 at a D-end with + on its left (PLUS-MERGE-1), or a is the first field (HASH-FAR-0, or FAR-0-PLUS after a far-end BOUNCE). The mode at the end is itself decided by the singletons (C5). This closes exits (a) and (b): 2 + 1 # 2 has a = 1 with P = 0.
• (B3) inside a climb, every singleton must cover its stage losses (C5). The field right of a + must not reach + 0 | L (exit (e)), and must not reach 0 under a + in mode U (the DEATH-MERGE path of C5).
• (B4) nested deaths (exit (d)) need either several # in J* (one per pending dance, nested by C1–C3), or a budget clause that rules them out.
• The scaled budget of a field at depth u is f·2^u. By C2 the field lasts f·2^(u+1) half-cycles at depth u, so the inequalities between neighbours must compare f·2^u (revision 1's f/2^u was inverted). On line 75 at 10^13, f·2^u spans 0.38 M to 69 M over the 19 fields.

These clauses close the one-step catalogue only if the values they demand are present when each death happens. Those values are fixed by the global budget race: which field runs out first, and what its neighbours hold at that moment. For the bulk of the list this looks tractable: the observed margins are wide (min b = 29 and min a = 6 at interior deaths to 10^16), and no perturbation of the bulk below fails there. The far end is different (§6.4).

6.4 The far-end race (new in revision 2; why the status is STUCK)

Fast exact map. check_proof.py §I runs the abstract map with C1/C2 jumps. A run of ODD half-cycles that meets no zero field is applied in one step: the per-depth carry counts, L + 3s, and the exact machine steps in closed form. Every other event goes through step(). On all four orbits it reproduces the plain map event for event, steps included, to 10^11. With it:

• The four orbits meet no outside case to 10^100 steps (§I: 7.0–8.1·10^49 half-cycles, 165–166 fields, about 17,400 non-ODD events each). Scratch runs extend this to 10^150 (248 fields; work/rev2/far.py).
• The far end is eaten in windows. The first field is consumed about one unit per far-end visit. A visit comes once per run of the full region, and runs get longer geometrically.
• Line 75's first field c = 47 is gone at 7.1·10^14, when the next field is 116. Fields of 105 and 69 follow, by 8.3·10^24. From 4.9·10^60 on, the first bulk field is about 1,900, and it loses about 60 units by 10^77.
• Meanwhile the prefix keeps passing through small shapes. Each orbit has 64–88 episodes to 10^150 in which the first field after the 1 + prefixes is ≤ 2 (work/rev2/windows.py).
• Line 75's first window runs from 2.4·10^14 to 7.07·10^14: 1 + 1 + 3 | 122 → 1 + 0 | 1 | 120 → 1 + 0 | 0 | 118 → (PLUS-FAR-1) 0 | 0 | 117 → (DEATH) 0 # 116 → HASH-FAR-0.

The race. At a prefix such as 1 + 0 | 0 | x …, two events compete. In a down-run of the far region, PLUS-FAR-1 removes the 1 + first. In an up-run, the carry reaches the second 0 first, and DEATH gives 1 + 0 # x. The direction is a parity that the whole history fixes (C1, C6). check_proof.py §C shows both orders on 1 + 0 | 0 | 23 | 86 | 300 | L, a J-member:

• with L = 1201 (down-run), PLUS-FAR-1 comes first, and the map stays inside the rule set;
• with L = 1200 (up-run), DEATH comes first. The dance then meets (o4), HASH-ODD with a = 0 not first.

Line 75's first window took the safe order. The unsafe order leaves the rule set:

• at (o4) after 1 + 0 # x;
• at (o7) after 1 + 0 + x;
• or, when a death reverses the far region first, at BOUNCE 1 + 0 + …. In that last case the climb reaches + 0 +, which is (o1): halt.

What the machine does after (o4) and (o7) is not in the rule set. (o1) with + on the left halts (§C: every example, and 300 of 300 random lists).

Perturbation evidence (work/rev2/perturb2.py, exact map to 10^100; outputs in work/rev2/). The configuration of line 75 at 10^13 was perturbed 300 times: L redrawn, three fields changed by up to ±50 %, or all fields scaled by 0.5–1.5.

• 276 of the 300 run to 10^100 with no outside case.
• 24 leave the rule set, at times from 2.8·10^14 to 1.2·10^85 (work/rev2/p2pos.py). 22 of them do it at the far-end prefix (field 2 or 3 of 24–141):
• 14 at (o4) 1 + 0 # x;
• 5 at (o7) 1 + 0 + x;
• 3 at the halting pattern (o1) 1 + 0 + x, with the scan on the 0, at 2.8·10^14, 4.8·10^16 and 1.2·10^85 steps.
• The other 2 are bulk (o5) events at 1.6·10^18. Both come from runs whose L was redrawn small, which planted a small field.
• In 600 random small starts, 139 meet an outside case before 10^80 steps. The late ones (10^25 to 10^71 steps) all come at the far-end prefix.

Conclusion.

• The bulk behaves like a budget counter with wide margins. Its only failures here come from a planted small L.
• Every far-end window, by contrast, is a race. A history-dependent parity decides it, and the wrong outcome halts (or at least leaves the rule set). Windows recur forever, because the far end eats one field at a time and births go on at the right.
• So an inductive J* must certify, in every future window, that the far region's counter runs the safe way. With no structure that forces this, it is a statement about a pseudo-random bit sequence.
• That is the cryptid-protocol situation. The rules are formalized here (§3, §4), the behaviour is flagged, and the work stops.
• A rough rate: 24 failures in 300 perturbed runs of about 50 episodes each is about 0.2 % per episode, and each real orbit has passed about 80 episodes. If the rate stays fixed, each start eventually leaves the rule set (heuristically after hundreds of episodes, around 10^1000 steps). About 1 exit in 8 is the halting (o1); the others need rules for (o4) and (o7). Nothing here proves either outcome.

7. Progress and halting

• Every macro step is ≥ 8 machine steps (§3.2).
• If J held at every configuration on the orbit from K(c) (O1), a rule would always apply (LE). By §0, the only halting configuration is B reading 1 next to 11, and an exact rule run never presents it. Then the machine would never halt from any of the four starts.
• O1 is open, and §6.4 shows that it contains a far-end race that no budget threshold settles.

8. Lemma plan against kill #3

Same architecture as #3: one macro rule per half-cycle, merges, a re-pairing at overflow, a per-step invariant. The digits are different.

Formalization route (only if O1 were closed):

1. Definition X (T: list (nat * sep)) on the left side of the head. The shift lemmas S and A by ind.
2. One lemma per rule of §3.2, by follow over the sweep lemmas. The scan is an induction over the even suffix.
3. init: one es call per start to K(c) (≈ 3·10^4 steps).
4. nonhalt by progress_nonhalt_cond with P := J*.

Upstream Sk1Machines.v and the Sk1like_TC_v*.v files (mxdys) are not templates: they use different word sets and different digits.

9. Evidence: python3 -B check_proof.py

The script is self-contained: stdlib only, with its own simulator, parser, abstract map and fast map. The SUMMARY is PASS only if A, B, D, E, F, G, H and I pass; C is informational. PASS covers the proved parts; it does not prove O1. The defaults (--direct 3e7 --far 1e13 --fast 1e100) take about 160 s, and the latest run (PASS) is in data/check_proof.out.

10. Review log

• Revision 1 (2026-10-14): first write-up. Open: O1 (J*).
• Skeptic review of revision 1 (2026-10-14): not sound. One fatal gap (J not inductive: five one-step exits, halting J-members), two major gaps (PLUS-MERGE-1 breaks C3/C5/C6; far-end 0 + after a nested far-end death), three minor ones.
• Revision 2 (2026-10-14): what changed for each item.
• Fatal gap (O1). Still open. The one-step catalogue and the halting J-members are in §6.3. The clauses an inductive J* needs are written in counter terms (B1–B4), with the scaled budget corrected to f·2^u. §6.4 adds the far-end race: perturbations of the real configuration leave the rule set as late as 10^85 steps, and some halt. Status STUCK under the cryptid protocol.
• Major gap, PLUS-MERGE-1. Fixed:
  • C3 now covers every merge event (B* table).
  • C5 is now a two-mode climb automaton.
  • C6 has both branches (D-end reversed, U-end kept).
  • The §4.3 table is complete.
  • §H replays the automaton after every re-pairing, on random climbs and on the reproducer.
• Major gap, far-end 0 +. Fixed: the FAR-0-PLUS-EVEN and FAR-0-PLUS-ODD rules (§3.2, checked in §B), and J3 now admits a first field 0 before +.
• Minor gaps. Fixed:
  • the scaled budget is f·2^u;
  • SP names the smaller copy;
  • the rule count is 15;
  • the (o1) wording;
  • the C1 statement;
  • the Reduction now says "every X(T) reached by the macro steps";
  • (o5) comes three half-cycles after 9 # 0 | 3 | 15.