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

W7-5 · 1RB0RD_0LC0RA_1LA1LC_1RE0LF_0RA1RF_1LB--- (740 line 274; table family 514)

Status: CHECKPOINT_B, stage informal_proof (proof.md written 2026-10-14; Checkpoint B review: sound, 5 minor gaps, all fixed; check_proof.py 82/82). Confidence on the mechanism: high. Class: sheet "Skelet 1-like Class 1". Ours: an exact base-4 counter. Its digits are four fixed-size defect words in a sea of 100; the least significant digit sits at the right end; every other overflow gives birth to a new digit at the right end; the most significant digits pile up in a zero-field cluster at the left wall and keep counting there (pushes). Viewer: https://bbchallenge.org/1RB0RD_0LC0RA_1LA1LC_1RE0LF_0RA1RF_1LB---

Checks

Halting condition

F1 is the only undefined transition. F is entered by D1 (0LF) and E1 (1RF). So a halt needs D reading a 1 with a 1 on its left, or E reading a 1 with a 1 on its right. Never seen; no sweep of any tested kind (real, random, exhaustive small) halts.

Mechanism (exact)

Notation: s = 100 (sea word). Digit words, phase p:

p word token
0 11001100 tt
1 110000 v
2 1001100 s t
3 10000 u

Wall: 1100 (t) or nothing. A D-record is the moment the head steps onto a fresh cell at the right end in state D. At every D-record from step 108 (274) or step 792 (514) on, the tape is

0^inf [wall] P(p1) s^f1 P(p2) ... s^f(k-1) P(pk) s^R 100 D> 0^inf

with the first digit right after the wall (no leading field), fields f >= 0 and R >= 2. scripts/macro.py and model.decode_rle decode any drec line into this form.

  1. Sweep = increment (R1, R2). From a D-record the head runs left to the first digit with p < 3 and back. - Every digit with p = 3 wraps to p = 0 and moves 2 cells left. The first digit with p < 3 goes to p + 1 in place. The right end grows by 4 cells. - Fields follow from positions (the sea between two digits is never touched except by the head crossing it). So the field to the right of a digit loses 1 at its 1->2 and 3->0 steps (2 per full cycle), and R gains 2, 1, 2, 1 for p = 0, 1, 2, 3 (6 per 4 sweeps).
  2. PUSH (zero fields). A digit never overlaps its left neighbour. When a field would become -1, the right digit is pushed 3 cells right and the field to its own right pays (cascading through zero fields). So fields never go negative, and digits whose field died stay separate digits in a cluster at the left and keep counting.
  3. Overflow (O1, O2). When every digit is 3, the carry reaches the wall. All digits wrap. - O1, wall 1100 -> none: the wall disappears. - O2, none -> wall 1100: a wall appears 5 cells left of the old left end; every digit moves 2 more cells left (an extra pass over the whole tape); a new digit P(3) is born at the right end with R = 2 (the old R becomes its left field); the right end grows by 7.
  4. Steps (R3), exact. With pre-sweep fields: R1/R2 = 8(R + fields crossed) + 52 per wrapping digit + 32 (stop at p = 0, 2) or 76 (p = 1) + 20 per push word; O1 = 8(R + all fields) + 52k + 32 + 20 per push word; O2 = 10(R + all fields) + 50k + 101 + 20 per push word.
  5. Counting. It is a plain base-4 counter. O1 -> O2 takes exactly 4^k sweeps and O2 -> O1 takes 4^k - 3 (the newborn starts at 3). One new digit per two overflows: births at steps 477, 7,910, 119,447, 1,874,600, 29,808,277, 476,169,214, 7,615,621,471 (274). At birth the newborn's left field is 3·4^(k-1) - 5 (3067, 12283, 49147, ...) and R at O1 is 1.5·4^k - 3. Each field then shrinks by 2 per cycle of its left digit, dies, and its digit joins the cluster. At 1e9: [t] P1 P3 P1 P1 | 128 P1 | 1809 P2 | 11344 P1 | R 11267; at 1e11: 6 cluster digits and 2 isolated ones.

Validation

Both starts (start-parametric)

514 is start F of the same table, mirrored. Both enter the same language (274 at step 108 as P1 s^2; 514 at step 792 as [t] P0 s^7 P3 s^2) and then follow the same rules with the same counter value and the same field sizes, except one field that is 4 words longer on 514 (128 vs 132 at 1e9, 199 vs 203 at 1e11). That offset moves into the next field each time the cluster absorbs a digit. So one closed-language argument covers both lines; each start needs only its entry lemma (108 and 792 steps of direct simulation).

Cryptid check (stop rule applied early)

Not a cryptid. Every branch is on a phase (mod 4), the wall bit, or a field being zero; every event rule is affine in the field sizes; the counter runs through every value 0..4^k - 1 in order; no x(p/q) maps, no branching on residues of growing numbers. The class kill switch is not triggered by this table. Stop rule respected: no stage 1 work was started (W7-4's stage 1 has not reported; its observe says GO).

Template check

Route and next step

Proof = a closed language L plus rule lemmas: 1. sea-crossing lemmas (left and right passes over 100^n); 2. digit lemmas: 4 phases x (stop or wrap), plus the zero-field neighbour cases; 3. a push lemma by induction over a run of zero fields; 4. the two overflow lemmas (O1, O2 with birth); 5. an invariant for the domain condition (R >= sweeps since the last birth, which exceeds 2k + 2 when the next O2 comes), or explicit closed forms for all fields in terms of the counter value; 6. entry lemmas for 274 (108 steps) and 514 (792 steps).

The counter is simpler than W7-4's (fixed digit words, no glue), so this table does not really depend on W7-4's stage 1. A purely regular certificate is unlikely as is, because the domain condition counts. The planner's stop rule still holds; decision.json asks whether to lift it.

Attempts

Files