Bells eating counters

1Read the tape at an eat

W5-3 at step 165. Left is the bell, 2 pairs of 10 (cells −2 to 1). Then 0 1 1, and the head: B reads the 0 after them (cell 5). Right is the counter: digit 0 is 00, digit 1 is 11, lowest digit first.

The counter reads 0, 0, 1 from the head outward, so N = 100 in binary = 4. We call this tape E(2,4): p = 2 pairs in the bell, counter N = 4. Every eat configuration has the same shape:

C(N) is the counter: N's binary digits, lowest first, each written twice (00 or 11). B> means "state B reads the next cell to the right".

2One round: count, count, …, count

One row each time the head is back at the counter: B reads the 0 just right of 0 1 1. These moments are the count configurations. Here they go from E(2,4) at step 165 to E(5,7) at step 451, the round in the left picture above. Row 2 is right after the eat (section 3). Rows 3 to 8 are counts, and each one adds 1 to N.

Step through it and watch the bracket marked defect:

• an extra 1 becomes an extra 0 in the same place (rows 3 → 4 and 5 → 6);
• an extra 0 becomes an extra 1 two pairs further left (rows 4 → 5 and 6 → 7);
• at row 8 the defect has walked off the left end. The bell is clean again, (10)^5, and N = 7: that is E(5,7).

Inside two counts, every step (steps 225 to 301)

E runs left over the 10 pairs until it meets the defect, and changes it. Then A runs back right into the counter and adds 1 there (the carry of module 3), and the head ends at B again. The first trip takes 30 steps, the second 46.

3The eat, every step (steps 165 to 197)

With no defect, E's sweep does not stop: it runs off the left end of the bell into the blank. There B and C write 1s, and then C and F sweep right over the whole bell. C writes 1 on each 0 and F writes 0 on each 1, so the stripes slide over by one cell: watch rows 177 to 187. The bell now starts 3 cells further left (cell −5 instead of −2).

Then A runs on into the counter and bites its low digits: 00 00 11 (N = 4) becomes 11 (N = 1), and the head ends 4 cells further right (cell 9 instead of 5). The bell has grown into the eaten cells too and ends with 1 1 1. The next count turns that into a single extra 1: the new defect, at the counter end, ready to walk left.

Why eats are where proofs get hard: W5-3's only undefined transition is F reading 0 (the red cell in the table), and F runs only in this sweep. On a clean bell every cell F reads is a 1, so the machine cannot halt here. The proof has to show that every future eat is like this one.

4Eat to eat: from E(p, N) to E(p′, N′)

Now skip the counts: one row per eat configuration, from the blank tape. The strip shows 14 cells on each side of the head: the end of the bell, 0 1 1, and the counter. Each line of the history starts with its E(p, N). Watch the two numbers.

Which rule comes next depends only on N's lowest binary digits: the digits right of the head. These are rules M1–M5 of W5-3's write-up, in plain words.

"+1 if p is odd" means p′ gets one more when p is odd. In M5, write N + 2 = (2m + 1)·2^(t+3) with t ≥ 1. For N = 110: N + 2 = 112 = 7·16, so m = 3, t = 1 and N′ = 3 + 2 + 1 + 1 = 7. (The write-up also asks for p + 7 ≥ 2^t; that always holds while N ≤ 2p, module 5's invariant.)

Why N stays small. The eat leaves about half or a quarter of N: (N + 1)/2 for odd N, N/4 for N a multiple of 4. Then each count adds 1, and a round has about as many counts as the bell has pairs (drill 2). From E(2,4): the eat leaves 1, then 6 counts give N = 7.

Why M4 and M5 drop N so far. They eat, count once, and eat again. From E(14,22): eat (steps 2,725 → 2,822), one count (→ 2,846), eat (→ 2,953). The two eats bite the four low digits of 22 = 10110 and leave m + 1 = 2. Then two defects cancel each other after just 4 counts (N = 2, 3, 4, 5, 6, steps 2,953 → 3,097), instead of one defect walking across the whole bell. So N′ = m + 5 = 6.

5The family

Eight more of our kills are in the spreadsheet's class "Bell eats counter"; here are four of them. Each has its own bell and its own counter. In each proof, rules take one eat configuration to the next, and an invariant (module 5) shows that no eat ever lands at a bad moment.

W4-2 and W5-1: one table, mirrored

How to read these: bbchallenge.org's Blaze view squeezes the first 10⁶ steps into 500 rows, time going down; orange is a 1, white a 0. The wide striped part is the bell. The narrow, ragged edge is the counter it eats: on the left in W4-2, on the right in W5-1. Each horizontal band is one round of bounces, from one eat to the next, and the bell's outer edge steps out once per band. The early, short rounds are squeezed into the top rows. (Rendered by tools/diagram.py.)

W4-2 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF is a machine already proved in busycoq (the Coq library that bbchallenge proofs are written in), file BECv5.v, Module TM1, with one transition changed (F1). Its proof: from step 32 on, the counter stays between 1 and about 2.5 times the length of the last round.

W5-1 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB--- is W4-2 with one transition changed (F1), mirrored left to right, with the states permuted. Its start state A plays the role of W4-2's state F. That is why its picture looks like W4-2's flipped left to right.

W4-2 machine pageW5-1 machine page

#2 against its template

Same reading as above: the first 10⁶ steps, Blaze view, orange = 1, white = 0, time going down. Look at the overall shape, not the details.

#2 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---, our first accepted kill (PR #14), is busycoq's file SOMDCv6.v, Module TM7, with one transition changed: A1 is 0RF instead of 0RC. From far away they look the same. The explorer preset plays both from the same tape, step by step, and marks where they split.

#2 vs TM7 in the explorer#2 machine page

The other four: #30, #7 and W4-1 share one table (mirrored or with the states permuted) and start in different states; W5-5 is the one that halts.