/machines/1RB0RA_1LC0RE_0LD0LB_1LA1LF_1RA0LF_1LC---/notes.md · raw

W4-4 `1RB0RA_1LC0RE_0LD0LB_1LA1LF_1RA0LF_1LC---` (740 line 156)

     0    1
A   1RB  0RA
B   1LC  0RE
C   0LD  0LB
D   1LA  1LF
E   1RA  0LF
F   1LC  ---        halts only if F reads 1

Checks before starting

Byte-exact on data/holdouts/BB6_holdouts_740.txt line 156 (also 778 line 166).
Sheet: Results row 66, class Unknown, no status/notes/done-by; Classifications column "Unknown". No hit in data/discord/*.txt. Unclaimed.
busycoq: upstream Eqv_v3.v module TM23 proves halts tm c0 <-> halts tm' c0 with tm' = this machine and tm = 1RB0RA_1LC0RE_0LD0LB_1LA1LF_1RA0LB_1LC--- (E1 = 0LB). That is the whole eqv group (eqv_1590 lines 994-995); it reduces nothing for us, both stay open.
Same table, other starts (canon up to renaming + mirror, starts.py): start B = line 450 1RB0LE_0RC0RA_1RD1RF_1LA0LD_1LD0RF_1RB---, start D = line 188 1RB1RF_1LC0LB_1RE0LD_1LB0RF_0RA0RC_1RE---, start E = line 564 1RB0LF_1RC0RB_1LD0RA_0LE0LC_1LB1LF_1LD---. Start C is on no list; start F is in Eqv_v2 (not on 740). So the family is 156/188/450/564, four holdouts.

Observation

No halt to 1e10 (C tracker scripts/gapsim.c, ch1e10.txt). At 1e9: span 76,685 (lo -57,552, hi 19,132), 38,338 nonzeros; span 25,552 at 1e8, so span ~ t^0.48.
Halting analysis from the table: E is entered only by B1 = 0RE, so after E1 = 0LF the cell F reads is the 0 that B just wrote. So F reads 1 only after C0 = 0LD, D1 = 1LF, i.e. the machine halts iff it reaches 1 1 0 <C (C on a 0 with 11 directly to its left).
Transition counts to 1e9: sweep transitions A0/A1/B0/B1/C1/E0 ~1.25e8 each; events C0 116,549, F0 107,067, D1 92,695, D0 23,854, E1 14,372.

The tape: alternation plus extra symbols ("pair frame")

The tape is the background 1010... with isolated defects 00 (an extra 0) and 11 (an extra 1). Read from the leftmost 1 greedily in 10 pairs: 0^inf (10)^n0 x1 (10)^n1 x2 ... xk (10)^nk [end], x_i in {0,1}. Both sweeps complement every cell they cross (A> (10)^n -> (01)^n, (10)^n <B -> <B (01)^n), so a region crossed twice is restored and only the defects move. scripts/pf.c prints this list at every left/right record in state A (LA / RA records).

Rightward sweeps read pairs alternately in A-mode (A1 A0) and B-mode (B1 E0). Window lemmas (exact finite runs, scripts/val_W.py, 6/6; shifts 120/120): | | window | steps | meaning | |---|---|---|---| | W1 | A> 100 -> <C 101 | 5 | A-mode pair, extra 0: turn, extra becomes 1 in place | | W2 | B> 100 -> 011 B> | 3 | B-mode pair, extra 0: pass (mode parity flips) | | W3 | A> 1011 -> <C 1010 | 7 | A-mode pair, extra 1: turn, extra becomes 0 one pair right | | W4 | B> 101 -> 010 A> | 3 | B-mode pair, extra 1: pass | | W5 | 0100 <B -> <C 1101 | 4 | leftward sweep passes 00, which lands 2 cells left as 11 (C0 D1 F0) | | W6 | 110 <B -> 010 A> | 5 | leftward sweep turns at 11 | W5 is the only place a sweep makes C read 0 next to a 1; with 11 directly left of the 00 (1100 <B) it is the halting window.

Candidate rules (validated)

E, eat bounce (RA record to RA record):

0^inf L 0 (10)^(a+1) 0 0 [(10)^q_i 0]_{i=1..k} (10)^c A> 0^inf
  --> 0^inf L 0 (10)^a 0 0 [(10)^q_i 0]_i (10)^(c+2) A> 0^inf
steps 4c + 4 sum q_i + 2k + 12,   needs a >= 1, every q_i even, c even

The 000 marker walks left 2 cells per bounce, eating the segment to its left and paying 2 pairs to the right end; L is never read. 200/200 random instances (p 1-20, a 1-30, k 0-4, q_i, c even), step formula exact (residual 0). Case split is sharp: with any q_i or c odd it fails 0/n in every one of 24 parity classes (val_E2.py).

L, left-end bounce (LA record to LA record) = a 4-state carry transducer read left to right on (n_i mod 2, x_{i+1}) ('E' = the end):

S : (even,1) n0+=3, x1:=0, n1-=1, STOP      (odd,1) n0+=1 -> T      (odd,0) x1:=1 -> Z+
T : (odd,1)  n_i+=2, x:=0, n_{i+1}-=1, STOP
Z+: (even,0) n_i+=1, x:=1 -> Z-    (even,1) n_i+=3, n_{i+1}-=1, STOP
    (odd,1) -> Q                   (odd,E) n_i+=4, STOP
Z-: (even,0) n_i-=1, x:=1 -> Z+    (even,1) -> Z-
    (odd,1)  n_i+=2, x:=0, n_{i+1}-=1, STOP          (even,E) n_i+=2, STOP
Q : (even,1) -> Q                  (even,E) n_i+=4, STOP

Undefined entries (e.g. Z-(odd,E)) are where the bounce runs to the right end instead (an LA>RA move). Validation: 900/900 random constructed LA configs (3 seeds; n_i in [2,30], [1,30], and [0,30] incl. adjacent extras) and every one of the 14,266 real LA>LA moves to 1e9 (30,720 to 1e10). The 1e8 parity-signature classification (la_classes_1e8.txt): 58 classes, 0 inconsistent.

Coverage of record-to-record moves (cover.py): to 1e9, 23,912 moves: L 14,266 (59.7%), E 9,265 (38.7%), other 381 (1.6%). To 1e10, 98,334 moves: E 66,946, L 30,720, other 668 (0.7%): 251 RA>RA (the 6-step end rule ... 1 A> -> ... 0 (10) A> and the 76/502-step first eat bounce), 207 LA>RA (a Z- chain that runs off the end), 207 RA>LA (full return: every 0-extra becomes 1), 3 merges (1 (10)^0 1 cancels). They look like a handful of fixed shapes (uncovered_1e9.txt), not yet ruled.

Macro picture (not understood)

At eat-phase starts (58 to 1e10, history_rows.json) the list has 2-13 separators; it does not grow steadily. Tail motifs recur (... 8 |4 3, 44 |4 17 |3 13 |3 1 |3 3, 130 |4 113) while the left digits grow; e.g. from 4.44e6 to 5.62e6 the first six digits move by +180, +90, -30, +30, -10, +10 (powers of 3 per pair), so it looks like a hierarchical counter over digit pairs.
Parity law observed but broken: at most eat starts the digits left of 000 are even (gap form) and those right of it odd, but 9 of 33 eat starts to 1e9 (17 of 60 to 1e10) break it (two 000 at once, an even digit right of the marker, an odd digit left of it after an inner eat phase).
Not cryptid-like so far: every rule is linear with parity case splits, and nothing multiplies. But each branch is chosen by parities of large transferred numbers, so a pseudo-random parity sequence is not excluded.

Siblings

Same rule coverage from starts B, D, E to 1e9 (cover_1e9_start*.txt: L 14,263-14,266, E 9,265, other ~380). The four orbits are near-twins: at 1e9 they differ only in the first 3-4 digits (19181 0 4576 0 270 0 1522 ... vs 19179 1 4575 1 271 0 1522 ...), with an identical tail, and no record configuration is shared (0 of 23,913). One architecture, four inits.

Template check

Nearest proved neighbour: kill #11 (1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---.v, and #11b 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---, which is 6 cells from this table). #11's rule set: S1-S6 shifts, T1-T14 windows, K(ds; a, b) over digits d0/d1 (u, v), carry M, drop, overflow O, one INV. Shared: a list-of-digits K-config with a bit per digit, induction lemmas for sweeping a list (LbS/RbS/RoS). Different: our left-end carry is a 4-state transducer that changes digit lengths by 0, ±1, +2, +3, +4 depending on parities, there is a separate eat phase E that pays one digit into the right end, and the macro behaviour is multi-level. Applies: partly (infrastructure only).

Checkpoint A (Dennis)

Confidence LOW: rules cover 99.3% of record moves to 1e10, but 5 event families are unruled and there is no macro rule and no non-halting argument. Priority call in decision.json.

Informal proof

Not started.

Decision (2026-10-11)

Question: W4-4 and its three sibling starts (188, 450, 564) share one defect-list mechanism: fund one ~2 h rules stage to close the abstract model and probe the macro hierarchy, or park the family with R4/#32? Answer: rules_stage (Fund one ~2 h rules stage for the whole family). Dennis: go with recommendations (2026-10-11).

Funded stage (2026-10-10, rules_stage)

Run 2026-10-11, ~2 h, light compute (C tracker 1 min per orbit to 1e10; everything else seconds). Files: scripts/rules/.

Tools. rec.c prints every A-record of a run as canonical pair-frame tokens n0 x1 n1 ... xk nk (word from the first 1 to the last 1 (LA) or to the head (RA), read greedily as 10 pairs). Checked: at LA records the head is on the 0 just left of the first 1 and the last visited cell is the last 1; at RA records the first visited cell is the first 1 and the gap is 0 or 1. So a record is fully given by (side, tokens), and oracle.c runs the TM exactly from any such constructed record to the next A-record. model.py holds the rules, validate.py tests them on random canonical configs against the oracle, absim.py iterates the rules alone from the first record and compares every record with the TM.

Rules (all in model.py; random validation: 2,000/2,000 each, seeds 6 and 7, validation_final.txt). - L (observe stage, unchanged table) with its domain now stated: the chain stops inside the list and no segment up to the one after the stop is 0. Outside it L was wrong: in all four orbits every chain that reaches the end entry runs off to the right (LA>RA), never stays LA, so the end entries Z+(odd,E), Q(even,E), Z-(even,E) are not used; zero segments make merges. - R6, end rule: w 1 A> -> w 0 (10) A>, 6 steps (local window, exact). - RE, right-end eat bounce, generalizes E. Read right to left from c = n_k: c even: +2, state P0; c odd: +1, state P1. In P0: even 0, odd -1 -> P1. In P1: even +2, odd +3 -> P0. It stops in P0 at the first turning point. At a 000 marker the segment left of it absorbs the balance, so the total change is +1 pair. At an extra 1 reached through even segments only (rule E1), the segment right of the 1 absorbs the balance and the 1 becomes 0. Domain: the stop is reached in P0, no segment on the way is or becomes 0, the eaten segment is not n0 and stays >= 0 (if it becomes 0, the extra on its left is 0). E is the all-even case. The 76- and 502-step "first eat bounces" are odd-segment cases, e.g. 15 0 9 0 0 0 3 0 1 -> 15 0 6 0 0 0 6 0 2. The RA records with one extra 1 are E1 cases. - F, full return (RA>LA): no marker and every extra 0: every extra becomes 1, the last segment +2, end 1. - FM, full return through a double marker 0000: (10)^a 0 0 0 (10)^q 0 (10)^r ... 0 (10)^c -> (10)^(a-1) 1 (10)^(q+3) 1 (10)^(r-1) 1 ... 1 (10)^(c+2) 1, or c+1 when r is c. Domain: a >= 2, q and every later segment even. - LR, left-end run-off (LA>RA, partial): the chain S(odd,0) then Z+/Z- over (even,0) segments, +1/-1 as in L, but the extras stay 0. Z- passes (even,1) and sets it to 0. Ending (a): Z- on an odd last segment gives an RA record with end 1. Ending (b): Z+ on (odd,1) adds 1 to that segment, makes the extra on its left 1 and every other extra 0, then (even,1) segments up to an even last segment; the end 1 is used up.

Exact model check (absim_1e10.txt). Iterating the rules alone from the first record reproduces every A-record of all four orbits to 1e10 with 0 mismatches. Only 63-64 moves per orbit (0.064%) have no rule and are taken from the oracle. Start A: 98,334 moves = RE 67,063 + L 30,720 + F 153 + LR 150 + R6 133 + FM 52 + 63 unruled. Starts B/D/E give the same table to within 1-2 moves. Unruled before: 668 moves in 5 families; now 63: - 57 LA>RA run-offs: other endings, Z+ on an odd last segment (... 6 0 91 1 0 -> ... 5 1 92) and Z- through (even,1) to an even last segment (... 2 1 108 1 0 -> ... 2 0 108), plus merges where the chain meets a zero segment (93 0 48 0 0 1 15 1 12 1 3 1 3 1 0 -> 93 0 45 0 0 0 18 0 14 0 2 0 3 1 0) and the first 3 start-up moves; - 3 LA>LA merges (169 1 19 1 0 1 100 ... -> 170 1 121 ...: 1 1 cancels into 2 pairs); - 2 RA>LA returns through a triple marker; 1 RA>RA with a double marker right of another marker.

Each is one fixed shape, so the model is exact but not closed.

Record language (all four orbits to 1e10, 393k records). RA records are very restricted. Every extra is 0, except 268 records with exactly one extra 1. There are 0-3 markers, exactly 1 in 98.2% of records. All RA dynamics is the one parity transducer RE plus the returns F/FM. LA records are rich: up to 14 extras with free bits, markers rare. This is where the counter lives (L transducer).

Still open (exit condition reached). - No invariant handle. Nothing yet says why the halting window 1 1 0 <C never occurs; in record terms this is a closed language containing the orbit and stable under the rules. Random configs outside the record language do halt (104 of 4,000 random RA configs). - The macro hierarchy was not probed further. The time went into the rules, and the counter is the LA side (L), whose branch structure is driven by parities of large segments. - 63 unruled moves per orbit (above).

The decision's stop rule ("park if the stage finds no invariant handle") applies, so the family 156/188/450/564 is parked. To resume: absim.py is a 1-second exact record simulator to 1e10, a base for an accelerated macro simulator past 1e10 and for searching a closed record language.