693: 1RB0LD_0RC---_0LD0RF_1LE1LD_0LA0RD_0RB1RA (working version, PARKED)

Status: not a proof yet. This is the working document of the three funded proof stages of 2026-10-14. Sections 1-7 are stage 1: notation, the local facts, the word-level rules (checked on random constructed tapes, step counts included), the observed mechanism and the open closure lemma. Section 8 is stage 2: the closed-tape-language attempt on that lemma, which did not close, and the exact obstruction. Section 9 is stage 3: the obstruction's two sources repaired (faithful digit bookkeeping, a floor on the counter); the shape set still did not close within the stage.

Checker: python3 -B scripts/check_proof.py (claims C1-C6; --random adds C7; --ctl adds C8-C9, the checks of the stage-2 shape explorer; --ctl3 adds C10-C11, the checks of the stage-3 explorer). Result on 2026-10-14: all checks pass.

The main finding of the stage: the left-edge records of the burst look are not the rounds of the machine. Between two records the machine runs a binary counter of 3-cell digits that counts wall steps of a rotating period-4 field. The record-level laws of notes.md (drop law, catch-up lists, bursts) are consequences of that two-speed arithmetic. A nonhalting proof most likely does not need them at all (section 7).

1. Machine and the halting criterion

The only undefined transition is B1 (B reading 1). The computed task text calls it C1; in the standard string the second triple pair 0RC--- belongs to B.

C2 (proved). B is entered only by A0 (1RB) and F0 (0RB), both moving right. So the machine halts exactly when, at some step, the head is in state A or F on a 0 and the cell to its right holds 1:

A> 0 1 ...   or   F> 0 1 ...   (one step later B reads 1)

2. Notation

• Directed head as in busycoq: S> x means state S reads the first cell of x; x <S means S reads the last cell of x. 0^inf are the blank ends.
• Positions are counted from the leftmost 1 of the tape, the marker (position 0).
• Field words: the four rotations of the period-4 pattern, 0011, 1001, 1100, 0110.
• Digits: 3-cell words 000 (bit 0), 001 (bit 1), and the transient carry digit 010.
• For a digit string g = g_1 ... g_D (each 000 or 001, most significant first), g + 1 is the binary successor (None when g is all 001), and t(g) is the number of trailing 001 digits.

C1 (proved, finite check). The eight rotation rules, 4 steps each:

A> 0011 -> 1001 A>        1001 <D -> <D 0011
F> 1001 -> 1100 F>        1100 <D -> <D 1001
C> 1100 -> 0110 C>        0011 <A -> <A 0110
B> 0110 -> 0011 B>        0110 <E -> <E 1100

By induction on n each gives the run rule, for example A> (0011)^n -> (1001)^n A> in 4n steps. Right-moving passes shift the field pattern one cell to the right, left-moving passes shift it back.

Inside the four right-moving rules B reads only 0: it reads cell 2 of 0011 (after A), cell 3 of 1001 (after F, A), cell 4 of 1100 (after C, F, A) and cell 1 of 0110. So a run rule never halts, and halting can only happen at the counter, the interface, the wall or the right end.

C3a (proved). B> 010 -> 000 B> in 3 steps (B0, C1, F0). This is the pass that clears carry digits.

3. The tape between records

Between two left-edge records the tape has four parts:

0^inf  1 <g>  I  [field: (w)^x  h  (w')^y]  R  0^inf
       counter  interface  wall          right end

• Counter 1 <g>: the marker and D digits at positions 1 .. 3D, big-endian binary.
• Interface I: 13 cells (positions 19-31 in the round of section 5) that hold the low bit and, after an eating step, one frozen 011 digit.
• Field: two runs of consecutive field rotations, separated by a wall (with an optional half-block h), followed by a short right end R.

The head shuttles between the counter and the wall. Each shuttle is one counter step (an increment of the counter) and moves the wall one block or half a block to the left.

3.1 Phase-1 rules (checked on random tapes, C4)

Put R1 = (0011)^2 0^3 1^2. The two configurations at the counter turn are

X0(g, c, d) = 0^inf 1 <g> 0011 0011 0 01 B> 01 (0011)^c (1001)^d R1 0^inf
X1(g, c, d) = 0^inf 1 <g> B> 0110 0110 01001 (0011)^c (1001)^d R1 0^inf

Rules, for c >= 0, d >= 1, D >= 1:

P1a  X1(g, c+1, d)  -(16c + 49)->         X0(g, c, d+1)
P1b  X0(g, c+1, d)  -(16c + 49 + 6 t(g))-> X1(g + 1, c, d+1)      (g + 1 defined)

• The step counts do not depend on d: the head turns at the wall and never visits (1001)^d or R1.
• In P1b the head carries through the t(g) trailing 001 digits (each becomes 010), sets the next 000 to 001, and clears the carries with C3a on the way back (6 steps per carried digit).
• So in phase 1 the pair (g, low bit) counts one step per block of the wall: the wall moves one block per counter step.

3.2 Phase-2 rules (checked on random tapes, C5)

Put R2 = 1001 1001 1000 11. Then

Z0(g, x, y) = 0^inf 1 <g> 0011 0011 0 01 B> 01 (1001)^x 1000 (1100)^y R2 0^inf
Z1(g, x, y) = 0^inf 1 <g> B> 0110 0110 01001 (1001)^x (1100)^y R2 0^inf

Rules, for x, y >= 0, D >= 1:

P2a  Z1(g, x, y+1)  -(8x + 19)->          Z0(g, x, y)
P2b  Z0(g, x+1, y)  -(8x + 43 + 6 t(g))-> Z1(g + 1, x, y+2)       (g + 1 defined)

• Again the counts do not depend on y: the wall between 1001 and 1100 reflects the head.
• The half-block 1000 makes the wall move half a block per counter step, so in phase 2 there are two counter steps per block.

Status of P1a, P1b, P2a, P2b: checked only. Each is a fixed sequence of passes (the run rules of C1 over the c- or x-run, then a bounded bounce at the wall and at the interface). The pass-by-pass derivations are not written out yet.

4. The rest of a revolution (observed on the orbit, not yet rules)

From the record at step 1,128,713 the run was followed for 12 records, with the field written in 4-blocks aligned at position 32.

1. Phase change. When the wall reaches the interface (c = 0 in phase 1, x = 0 in phase 2), the whole field has rotated one step, the head runs once to the right end, R changes shape (R1 to R2 in phase 1 to 2), and a new wall starts at the right end.
2. Phase 3 (field (1100)^x [1110] (0110)^y 0100 (1100)^z 011, interface 0110011001100): every counter step is a digit increment (the low bit is gone), two steps per block.
3. Eating. At the end of phase 3 the wall enters the interface. In about 20 short shuttles the interface moves 3 cells to the left and the lowest digit becomes the frozen word 011. The counter is one digit shorter: the bell eats one digit per revolution of the field.
4. Phase 4 (field (0110)^x [0111] (0011)^y 0010 (0110)^z 0011, interface 0011001100110): two steps per block.
5. Overflow = left-edge record. When the counter is all 001, the carry runs through the marker to the blank end. A0 writes a new marker 3 cells further left, all digits become 010 and then 000. The counter is one digit longer and restarts at 0. This is exactly a left-edge record in state A.

Because the interface moves 3 cells per revolution and the field has period 4, the field alignment relative to the interface changes from revolution to revolution. It returns after 4 revolutions, so there are up to 16 phase types, each with rules of the shape of section 3.

C6 (checked). From the blank tape, the records at steps 1,128,713 and 1,173,120 are consecutive, with no record between them. Between them there are exactly 127 = 2^7 - 1 counter steps (6 digits plus the low bit, counting from 0). The tape at step 1,128,893 is X0(000^6, 7, 64) (C6c).

Observed in the same round (not in the checker): 8 counter steps in phase 1 (c = 8 at the record), the other 119 in phase 2, ending at x = 12 when the counter overflows.

5. What the record-level laws of notes.md are

• A left-edge record is a counter overflow. Its "c" is the position of the wall at that moment.
• Records add one digit, revolutions remove one. In an epoch both rates match, so k + j stays constant (notes.md section 1).
• The wall advances one block per counter step in phase 1 and half a block in the other phases. So the wall position at overflow is an arithmetic function of the counter length, the field size s and the phase. The drop law 3 * 2^(j-2) - 2, the catch-up gain lists and the burst tapes O(n), E(n), V(n), W(n,i) are values of that function.
• None of this was derived in this stage. The stop rule ("park if the catch-up law does not close for all j") applies.

6. Evidence that the arithmetic is not needed

Random constructed tapes, with parameters that the orbit never produces, were run with the C simulator:

So nothing seems to depend on how the counter value, the counter length, the wall position and the field size are correlated. That is the situation in which a closed family with free parameters (a regular invariant) exists.

7. The open lemma and the route

Open lemma (closure). Let F be the set of configurations

0^inf 1 <g> I_k (u_k)^x h_k (v_k)^y R_k 0^inf

over all phase types k (up to 16), all digit strings g over {000, 001} (any length D >= 0), all x, y >= 0, with the finitely many interfaces I_k, half-blocks h_k and right ends R_k that occur, together with the finitely many transient shapes of the phase change, the eating step and the overflow. Then:

1. F contains a configuration reached from the blank tape (X0(000^6, 7, 64) at step 1,128,893, C6c).
2. Every member of F reaches another member of F in finitely many steps.
3. No step of these transitions is A or F on a 0 followed by a 1 (C2).

Parts 1 and 3 are easy once F is written down; P1a, P1b, P2a, P2b are four of the cases of part 2. Still open: the wall-step rules of the other phase types, the phase change at x = 0 (including the right-end change), the eating step, and the overflow in every phase. The overflow case must allow every wall position, which is why the random-parameter tests matter.

Route for a second stage. Do not prove the catch-up law. Instead:

1. Write a symbolic shape explorer (tokens: literals, runs w^(>=m), and a star {000,001}* for the counter), with the run rules of C1 as accelerations.
2. Compute the closure of the shape set from the X0 shape and check part 3 on it.
3. Turn each explored transition into a rule of the shape of P1a (with its step count), checked on random tapes like C4 and C5. These rules are the case list of proof.md.

This is a CTL-style (closed tape language) proof. Its formal version would use the busycoq style of the house Bell-eats-counter proofs: one Lemma per shape transition, plus the run lemmas.

8. Stage 2: the closed-tape-language attempt (2026-10-14)

Stage 2 tried to prove the open lemma of section 7 without the catch-up arithmetic: find a set of tape shapes with free parameters that contains a configuration of the orbit, is closed under the machine, and never shows a halting step. It did not close. This section records the method, what was checked, and why it fails.

8.1 Verified deciders first

busycoq's CTL deciders (CTL62.decide_nonhalt, the Coq-verified closed-tape-language deciders behind the upstream RWL_mod, CPS_LRU, NG, NG_cr, RNGS_* and *_FAR certificates) were extracted to OCaml and run natively on 693 (scripts/ctl_extract/). A true would have been re-checked in Coq with solve_cert.

RWLAcc is a loop detector on one orbit (it needs a configuration that repeats with growing counts), so it cannot handle a binary counter. No verified decider decides 693 with these parameters (work/ctl_sweep_A.jsonl, work/ctl_sweep_B.jsonl).

8.2 The shape language of the explorer

scripts/ctl_explore.py explores shapes symbolically. A shape is a directed-head configuration L S> R or L <S R whose two sides are lists of tokens:

The language of a shape is the set of all concrete configurations obtained by choosing the free counts and the counter word.

Every symbolic step is one of:

1. one machine step on a literal cell;
2. a run rule S> (w)^n -> (w')^n S> (or the left-moving form) when the head crosses one copy of w in state S and leaves it on the far side in the same state S. By induction on n this holds for every n, and it has no halting step. The eight rules C1 are the cases that occur.

Before a step the token under the head is split into cases that cover it exactly:

(w)^>=m, m >= 1        ->  w (w)^>=m-1
(w)^>=0                ->  (empty)  |  w (w)^>=0
(w)^n,   n >= 1        ->  w (w)^n-1
{000,001}^>=m, m >= 1  ->  {000,001}^>=m-1 000  |  {000,001}^>=m-1 001     (head arriving from the right)
{000,001}^>=0          ->  (empty)  |  {000,001}^>=0 000  |  {000,001}^>=0 001
0^inf                  ->  0 0^inf

After a step the shape is normalised. Every normalisation replaces the shape by one with a larger (or equal) language:

• merge literals, write k >= 2 adjacent copies of a word as (w)^k, absorb an adjacent copy of w into (w)^n or (w)^>=m;
• cap: (w)^>=m with m > K becomes (w)^>=K, and (w)^n with n > K becomes (w)^>=K;
• counter folding, only when a field run lies between the counter and the head: digit groups 000, 001 right of {000,001}^>=m are folded into it. An explicit counter with more than Q digits is replaced by {000,001}^>=Q+1.

Folding needs to know which cells are counter digits. Cells split off the counter carry a bookkeeping mark with their position in the digit. A digit loses its marks when it takes a value other than 000, 001, 010 (counter digits never do), or when the head enters it from the right in a state other than A, or from the left in a state other than B. Both happen exactly when the wall eats the digit. The marks never change the language, so they cannot affect soundness.

Soundness. Let F be the union of the languages of the explored shapes. Every concrete configuration in a shape is mapped by one machine step, or by one run pass, to a configuration in one of the successor shapes, because the case splits are exhaustive and normalisation only enlarges. So if the exploration closes (every successor of an explored shape is again explored) and no explored step is "B reads 1", then no configuration in F halts.

The start shape is

0^inf 1 {000,001}^>=6 0011 0011 0 01 B> 01 (0011)^>=7 (1001)^>=64 (0011)^2 0^3 1^2 0^inf

It contains X0(000^6, 7, 64), the tape at step 1,128,893 (C6c).

8.3 Checks of the explorer

So the explorer is sound on the tested steps and it follows the real orbit. No explored step was a halting step in any run after the digit-mark fix.

8.4 Result: the shape set does not close

"Skeletons" (the token sequence without counts and literals) keep appearing. In the Q = 0 run there were 300 after 100,000 shapes, 1,215 after 1 million and 3,460 after 2.5 million; the Q = 3 run is similar (288, 1,341, 3,031). The growth slowed between 0.5 and 1.5 million shapes and then sped up again, so the set is not about to close.

Random concrete members of explored shapes do not halt: 300 members (150 from all shapes, 150 from the newest quarter), 1e7 steps each with the C simulator, 0 halts.

8.5 The obstruction

The explored set is the closure of a free-parameter family, and that family contains far more than the orbit. On the orbit the region between the counter and the first field run is the 13-cell interface. Late in every run the explored shapes have much longer such regions, for example (K = 64, Q = 0)

0^inf 1 {000,001}* 1001 (0000)^1 01 (0000)^2 00 (0110)^3 0 (1100)^>=59 111 B> 011101 (1001)^3 (0011)^2 00011 0^inf

with 34 cells between the counter and the run (1100)^>=59. (0000 blocks alone are not a sign of junk: the orbit has them in the interface while the head is out in the field during P1a.) Each new such region brings new literal patterns, so the shape count does not level off. Concrete members of these shapes do not halt (section 8.4).

Two sources were identified.

1. The counter length is free. The real counter has n + 2 digits with 2^n <= s < 2^(n+1): overflows add digits as fast as eatings remove them (k + j constant, notes.md section 1). In the shape language the counter value is free, so a branch can avoid overflows for ever while the wall keeps eating digits. The counter then becomes empty or one digit long, and overflows and eatings interleave every few counter steps. Keeping short counters exact (Q = 3) does not help. A counter is exact only once it is written out in full; while it is {000,001}^>=m its value is free, and each eating lowers m by one.

2. The digit bookkeeping drifts on the orbit itself. A diagnostic run that forbids the counter to run out of digits (unsound, so it proves nothing, but it removes source 1) still does not close: K = 64, 1.9 million shapes, 2,848 skeletons and growing, with the same long interface regions. An exact replay of the orbit through the explorer (scripts/ctl_replay.py: X0 with every count exact and the counter written out, so every symbolic step is the real orbit) shows why. The eaten-digit rule (unmark a digit that the head enters from the right in a state other than A) fires at the real eatings (first at step 1,222,705), but also on ordinary counter digits: after the first eating the head enters the low digits in state D during normal counter steps, and the replay loses four real digits within about 440 symbolic steps. At step 1,642,188 the real tape is

1 000 001 001 001 001 001 001 001 001 100 110 011 ... (head in D at position 6)

and the replay shows it as 2 marked digits followed by 5 plain 001 groups. Plain digits are never folded back into the counter, so even the orbit's own configurations get longer and longer counter-to-field regions in the explorer's representation. That is the period-3 001001... pattern seen in the junk shapes. It is a precision defect of the explorer (soundness is not affected): the rule "entered by a state other than A means eaten" is wrong after the first eating. It has to be fixed before the closure question can be answered. A quick mark-free variant (fold digit groups while at least G cells remain before the field run) grows even faster (G = 13: 1,321 skeletons at 0.7 million shapes; G = 16: 3,935 at 1 million).

3. Short fields (with a small cap K) behave like the start-up of the machine, where phase changes rebuild the right end. This is an artefact of K. It did not show up with K = 64, but exact counts up to 64 multiply the shape count.

So the closure needs at least the relation between counter length and field size, D ≈ log2 s, or "an overflow happens in every revolution while D is small". That is arithmetic about the counter value. It also needs a faithful digit bookkeeping (source 2): until the exact replay keeps the orbit's counter foldable, the explorer cannot tell whether the free-parameter family closes. This is the stop condition of the stage ("park if the shape set does not close").

8.6 What a third stage would need

• A counter with a clock. Replace {000,001}^>=m by a counter token that keeps the number of digits D, plus the lemma "a counter of D digits overflows within 2^D increments". Together with "every phase has at least s/2 counter steps" this bounds the eatings between two overflows. This is the catch-up arithmetic in a weaker, inequality form. It removes source 1 only.
• First, though, fix the digit bookkeeping (source 2): the entering rule unmarks real digits that D enters during ordinary counter steps after the first eating. Replace it (for example by an eating detector tied to the wall reaching the counter) until the exact replay scripts/ctl_replay.py keeps every real counter digit marked over many revolutions and unmarks exactly one digit per revolution. Only then is the no-empty diagnostic run a test of the machine rather than of the explorer.
• Or prove the healing. Show that every malformed interface (eaten-digit remnants, 0000 blocks) returns to a normal interface within a bounded number of revolutions. The explorer's shapes give the list of malformed interfaces to cover, but the list kept growing up to the end of this stage.
• The twins 528, 310 and 548 run the same bell with other words. A third stage would apply to them with their own run rules. The decider sweep was not repeated on them, since it found nothing for 693.

9. Stage 3: faithful digit bookkeeping and a counter floor (2026-10-14)

Stage 3 did the two repairs of section 8.6 and reran the closure. The digit bookkeeping is now faithful on the orbit, and the floor on the counter removes source 1. The shape set still does not close within the stage, so the stop rule applies. This section records what changed and what is left.

New scripts: scripts/ctl_explore3.py (explorer), scripts/ctl_replay3.py (guided replay of the orbit), scripts/ctl_validate3.py (step check, member runs). Checker: python3 -B scripts/check_proof.py --ctl3 (claims C10, C11).

9.1 What the counter really is

The stage-2 bookkeeping assumed that the counter digits sit at fixed offsets from the marker. They do not. Two local facts, read off the transition table, explain the eating:

001 <D  ->  <A 011        (3 steps: D1, D0, E0)
000 <D  ->  1 0 1, then B and C pass right:  100 C/F> ...

The carry of an ordinary increment enters each digit in state A and leaves it in state A (001 <A -> <A 010). At an eating the lowest digit is entered in state D instead:

• a lowest digit 001 becomes the frozen word 011 and the carry goes on in A, as if the eaten bit had been carried;
• a lowest digit 000 turns its first cell into a 1, which becomes the low end of a counter shifted by one cell.

So after the first eatings the counter is no longer one aligned block. On the orbit it is

1  H  sep  L  I  field ...

with two digit blocks H and L, each made of 000 / 001 digits in its own alignment, and a short separator such as 1, 0011 or 011 between them. The records of notes.md show the same thing: (010)^k 011 (001)^j is H, the separator 011 and L at the moment of an overflow.

9.2 Writer marks

The new bookkeeping does not use positions at all. A cell written by a left-moving step of E, D or A gets the mark e, d or a. Cells written by right-moving steps keep their mark.

The carry of an increment runs right to left as A (cell 3), D (cell 2), E (cell 1). So every counter digit reads e d a from left to right, in whatever alignment its block has. A digit of the explorer is a triple with marks e d a and value 000 or 001. The frozen 011, the separators and the interface never carry these marks in this order with these values on the orbit (section 9.4).

Marks are bookkeeping only: the language of a shape ignores them, so they cannot affect soundness. They are kept only left of the first field run.

9.3 The counter floor (the clock)

The counter token S now means "at least Q+1 digits, any value" (Q = 2 in the runs below). Blocks of at most Q digits are always written out exactly. Splitting S at its low end gives exactly three kinds of case:

S  =  S 000  |  S 001  |  w   for each of the 2^(Q+1) words w of Q+1 digits

This is an identity of languages, so it is sound. Its effect:

• S never shrinks below Q+1 digits. An S that is eaten keeps its floor, so a free-valued counter can no longer be eaten down to nothing (source 1 of section 8.5).
• A counter that really has Q+1 digits becomes exact at the split. An exact counter of D digits overflows within 2^D increments, and a phase lasts at least K counter steps (its field run starts at length at least K). With K = 64 and 2^(Q+1) = 8, an exact counter overflows several times per phase and cannot be eaten to nothing.

That is the inequality form of the clock: no symbolic parameter is needed, because the only counters that could be eaten away are short ones, and short ones are exact.

Folding (with a field run between the counter region and the head) replaces each maximal block of digits left of the first field run by S when the block's language has at least Q+1 digits. Blocks can be explicit digits, S tokens or runs (000)^>=m. Several S tokens may appear (H and L). Runs of the carry digit 010 are compressed like field runs, so the carry through a long all-ones counter gives one token (010)^>=m.

9.4 Checks

At the turns of the replay the counter region reads 1 S D, 1 S 0011 S D, 1 S 1 S D, 1 S 0011 (001)^2 and similar: H, a separator and L, with the low digits exact. The stage-2 drift (real digits left as plain cells, counter-to-field regions growing without bound) is gone.

9.5 Closure runs

All runs explore turns and case splits only (straight-line steps are followed without storing), from the start shape of section 8.2 with the writer marks the orbit carries at step 1,128,893. "Digest set" runs keep 8-byte digests of the shapes to save memory; they are for exploration only.

No run found a halting step. With K = 64 the picture differs from stage 2 in kind: the skeleton count levels off (stage 2 grew steadily to 3,460 at 2.5 M shapes), and every late skeleton seen in a diagnostic run is an overflow in some phase type, with long carry runs. But the shapes keep coming, and the queue (10,000-40,000 shapes) does not empty.

9.6 Why it still does not close

The late shapes are the same skeletons with new exact counts. A sample of the queue (K = 32, after 1.5 M shapes) has at most 20 literal cells and 17 tokens per shape. What varies is up to four exact counts per shape, each up to K:

0^inf 1 S <A (010)^30 0110 (010)^20 01 (1001)^2 001 (1001)^15 1 (1001)^16 (0011)^2 00011 0^inf

• two carry runs (010)^n (a carry through a long all-ones counter, in two blocks H and L);
• the run behind the wall (exact, it grows by one block per counter step);
• the lower bound of the run in front of the wall.

So the shape count is roughly (skeletons) x K^3 or K^4, about 10^9 for K = 64: out of reach of the Python explorer in a stage (3.5 M shapes in about 25 minutes). The two obvious ways to shrink it both fail:

• a smaller K (16 or 32) lets fields get short, and short fields behave like the start-up (new skeletons keep appearing);
• capping digit and carry runs at 3 (lower bounds instead of exact counts) is too coarse: new skeletons appear at once (2,435 at 1 M for K = 64).

9.7 What a next stage would need

• A compiled explorer. The same rules in C or OCaml, with a compact shape encoding, to run K = 64 to 10^8-10^9 shapes. If it closes, the explored set is a certificate: an independent checker recomputes every shape's successors and checks that they are in the set, and C11-style step checks test the successor function.
• Or a better abstraction of the counts. For example, carry runs as lower bounds only after the carry has turned (when its exact length no longer matters), and the run behind the wall as a lower bound tied to the phase. Each such change must be re-validated on the guided replay (C10).
• Formalization. Even a closed set of millions of shapes is far from a Coq kill: busycoq's verified CTL deciders do not cover this language (section 8.1), so a verified checker for it would have to be written.