Submissions

**A nested bell counter never halts**

`1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB`

PR: https://github.com/ccz181078/busycoq/pull/28

The head shuttles between a wall and a binary counter whose bits are three cells apart. Each round consumes two pairs of the bell and decrements the counter. When the bell runs low, the wall bites the counter; a bite on low set bits can open several nested copies of the same process.

The proof keeps two facts: the bell is large enough, and a nonzero residue modulo 3 changes sign at each completed cycle. The tape's left side acts as a stack of pending levels.

The useful part is the induction: we prove safety for every finite number of steps, so we do not need to prove that each nested level eventually returns. After a checked 327-step prefix, the invariant rules out halting forever.

The Rocq file proves `nonhalt: ~halts tm c0.` against busycoq BB6. `Print Assumptions nonhalt` is closed. The low-level rule layout builds on BECv5's TM1.

Write-up (ZIP): https://raw.githubusercontent.com/DennisKoshta/busycoq/bbd8dec7ca70afd80523654b85ed142c3742e163/materials/bell-counter/writeups.zip
Image (ZIP): https://raw.githubusercontent.com/DennisKoshta/busycoq/bbd8dec7ca70afd80523654b85ed142c3742e163/materials/bell-counter/images.zip

AI assistance: the original proof, proof sketch and checks were produced with the help of Claude (Anthropic); independent audit and submission preparation with GPT-6 Astra (OpenAI).

Three more BB(6) nonhalting proofs: a bouncer whose apparent chaotic edge follows an exact recurrence.

```text
1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF
1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF
1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA
```

These are three starts of one transition table, after renaming states and reflecting one machine. The head crosses five blocks of ones separated by short words. Every twelve trips, two separators move closer; their collision rebuilds the blocks. Two collision types then alternate forever.

At the boundaries of each double cycle, the relevant block lengths obey:

```text
(n,x) → (n + 12x + 808, x + 32)
```

Each start has a separately proved opening into this family. They reach it at steps 153,126,993; 153,013,640; and 163,638,058 respectively. The closed recurrence then proves all three never halt.

Rocq proof PR: https://github.com/ccz181078/busycoq/pull/27
Full write-ups: https://raw.githubusercontent.com/DennisKoshta/busycoq/bbd8dec7ca70afd80523654b85ed142c3742e163/materials/chaotic-edge/writeups.zip
Space-time images (ZIP): https://raw.githubusercontent.com/DennisKoshta/busycoq/bbd8dec7ca70afd80523654b85ed142c3742e163/materials/chaotic-edge/images.zip

AI assistance: Claude (Anthropic) assisted with the original formal proofs, proof sketches, scripts and checks. GPT-6 Astra (OpenAI) assisted with independent audit and submission preparation.

A spread-digit bouncer counter: nonhalting proof submitted in https://github.com/ccz181078/busycoq/pull/26

`1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB`

This machine is a binary counter with variable gaps between its digits. Ordinary bounces increment the counter. At overflow, a finite tail either lets it wrap or triggers a long pause: the left side freezes into a wall, which is consumed two increments at a time while the gaps are rebuilt and new digits can be inserted.

The key is a four-rule token transducer for the return from the tail. Together with the tail's small front-unit cycle, it reduces the behavior between normal overflows to four paths. An interval invariant is preserved by every path, so the proof does not have to predict the tail's choices.

The blank run enters the invariant after 92,299 steps. The Rocq file proves blank-tape nonhalting directly, using Individual62 and standard libraries. Its structure follows CounterClass3v2 TM1's sweep/carry/macro-step approach.

Write-up (ZIP): https://raw.githubusercontent.com/DennisKoshta/busycoq/bbd8dec7ca70afd80523654b85ed142c3742e163/materials/spread-counter/writeups.zip
Image (ZIP): https://raw.githubusercontent.com/DennisKoshta/busycoq/bbd8dec7ca70afd80523654b85ed142c3742e163/materials/spread-counter/images.zip

AI assistance: proof and original write-up with Claude (Anthropic); independent review and submission preparation with GPT-6 Astra (OpenAI).

**A recursive Bell-eats-counter machine never halts**

`1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC`

PR: https://github.com/ccz181078/busycoq/pull/25

A marker moves along the tape while incrementing a counter. When its budget runs out, it consumes one counter digit and leaves a residue. Cleaning up that residue can launch a whole nested epoch inside a single outer bounce.

The proof bounds that cleanup with weighted potentials: it always finishes before the next potentially unsafe consumption. A checked prefix of 691 epochs reaches budget 17,713; from there, an invariant gives an infinite run.

The marker bounce comes from FractalBEC's tm10. The partial consumption and recursive cleanup need their own argument. This submission covers a different blank start of the transition table whose two other starts appear in PR #22.

The Rocq file proves `nonhalt: ~halts tm c0.` against busycoq BB6. `Print Assumptions nonhalt` is closed.

Write-up (ZIP): https://raw.githubusercontent.com/DennisKoshta/busycoq/bbd8dec7ca70afd80523654b85ed142c3742e163/materials/recursive-bell/writeups.zip
Image (ZIP): https://raw.githubusercontent.com/DennisKoshta/busycoq/bbd8dec7ca70afd80523654b85ed142c3742e163/materials/recursive-bell/images.zip

AI assistance: the original proof, proof sketch and checks were produced with the help of Claude (Anthropic); independent audit and submission preparation with GPT-6 Astra (OpenAI).

Two sync bouncer counters: nonhalting proofs submitted in https://github.com/ccz181078/busycoq/pull/24

`1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---`
`1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA`

These are different blank-start orbits of the same transition table, up to state renaming. A binary counter on the left drives a front through a row of blocks. Each overflow adds a digit; the front eventually converts the blocks and begins another cycle. Sometimes the next overflow arrives while the conversion is still running.

The useful simplification is that the cycle map has two affine branches, and both preserve one hexagon in the scaled block counts. We never need to predict which parity branch comes next. The two runs enter this invariant after 17,215 and 16,590 steps.

Both holdouts appear in dyuan01's October 1 longitudinal-filter list. The proofs build on the particles and digits of SBCv7 TM4, with direct window lemmas and the shared arithmetic invariant.

Each file proves blank-tape nonhalting on its exact machine string.
Write-ups (ZIP): https://raw.githubusercontent.com/DennisKoshta/busycoq/bbd8dec7ca70afd80523654b85ed142c3742e163/materials/sync-counter/writeups.zip
Images (ZIP): https://raw.githubusercontent.com/DennisKoshta/busycoq/bbd8dec7ca70afd80523654b85ed142c3742e163/materials/sync-counter/images.zip

AI assistance: proofs and original write-ups with Claude (Anthropic); independent review and submission preparation with GPT-6 Astra (OpenAI).

I believe I have a proof for 1 more holdout (identified and proved halting with AI-assistance). Skelet 1-like Class 2 again, but this one halts! :skull_crossbones:

`1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB` halts after 176,522,930,997,643,289,094,015,905,898,381,767,890,130,463 ≈ 1.77 × 10^44 steps. That count is computed from per-rule step formulas checked against simulation; the Coq proof shows only that it halts.
File: https://github.com/DennisKoshta/busycoq/blob/halt-skelet1like-c2-1RB0RD_1LC0RA/verify/Skelet1LikeC2Halt_1RB0RD_1LC0RA.v
PR: https://github.com/ccz181078/busycoq/pull/18
Informal write-up: attached

Watched each time the head reaches new ground on the right, the tape is a binary counter, and every carry burns fuel in each digit it touches. A digit that runs dry sheds a spare wall toward the head (walls drift right and refill the digits there), but a digit with a single marker has none to shed. New digits are born at the right end, and the time between births grows by a ratio that oscillates with growing swings; when the third swing crosses 2, a single-marker digit is left with bit 0 and no fuel, and the next carry into it halts the machine.

The .v replays the whole run in 107,781 checked moves (closed-form batches between structural events). It compiles against unmodified busycoq, Print Assumptions lists only functional_extensionality_dep (from flip_halts_iff), and coqchk passes.

AI disclosure: as before, produced with Claude Code (Opus 5.5). The results rest on the Coq files; extra verification and feedback are very welcome!

I believe I have proofs for 3 more holdouts (identified and proved non-halting with AI-assistance): one transition table started in A, B and F. One proof idea, three .v files, Skelet 1-like Class 2 again! :skull_crossbones:

`1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---` (start A): https://github.com/DennisKoshta/busycoq/blob/nonhalt-skelet1like-c2-1RB0RF-family/verify/Skelet1LikeC2_1RB0RF_1RC0RB.v
`1RB0RA_1LC0RE_1LD0LC_1RA0LB_1RA0RF_1LE---` (start B): https://github.com/DennisKoshta/busycoq/blob/nonhalt-skelet1like-c2-1RB0RF-family/verify/Skelet1LikeC2_1RB0RA_1LC0RE.v
`1RB---_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD` (start F, mirrored): https://github.com/DennisKoshta/busycoq/blob/nonhalt-skelet1like-c2-1RB0RF-family/verify/Skelet1LikeC2_1RB1RZ_1LC0LA.v
PR: https://github.com/ccz181078/busycoq/pull/17
Informal write-ups: attached

The tape alternates except at defects (two equal neighbours), and the defects are a base-3 counter: a left word counting to 81, a chain of digit blocks bumped once per visit, and two growing blocks at the right end keeping pace with it. Every 81·3^K visits the left word overflows and the chain regroups; after six of these K is 2 larger and every long gap 9x longer.

The A file carries one invariant from overflow to overflow, with every finite piece run by a verified symbolic run-length simulator (lengths are linear forms, so one run covers every gap). B and F keep its lemmas verbatim for the A table and add their own base case plus busycoq's perm_halts (and flip_halts for F).

All three compile against unmodified busycoq and Print Assumptions is closed. The base case is ~2.6e12 steps in 38 native_compute pieces, so coqchk doesn't finish in 10 min.

AI disclosure: the informal proofs and the Coq formalizations were produced with Claude Code (Opus 5.5) and checked by compiling against unmodified busycoq, with Print Assumptions. The results rest on the Coq files; extra verification and feedback are very welcome!

I believe I have proofs for 4 more holdouts (identified and proved non-halting with AI-assistance): one transition table started in A, B, C and D. One proof idea, four .v files, Skelet 1-like Class 2 again! :skull_crossbones:

`1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---` (start A): https://github.com/DennisKoshta/busycoq/blob/nonhalt-skelet1like-c2-1RB0LE-family/verify/Skelet1LikeC2_1RB0LE_1RC0RC.v
`1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---` (start B): https://github.com/DennisKoshta/busycoq/blob/nonhalt-skelet1like-c2-1RB0LE-family/verify/Skelet1LikeC2_1RB0RB_1LC0RA.v
`1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---` (start C, mirrored): https://github.com/DennisKoshta/busycoq/blob/nonhalt-skelet1like-c2-1RB0LE-family/verify/Skelet1LikeC2_1RB0LD_1RC0RE.v
`1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---` (start D, mirrored): https://github.com/DennisKoshta/busycoq/blob/nonhalt-skelet1like-c2-1RB0LE-family/verify/Skelet1LikeC2_1RB0RE_1LC0RE.v
PR: https://github.com/ccz181078/busycoq/pull/16
Informal write-ups: attached

The tape is a binary counter on (10)^u (01)^v digits, with 00 between the halves for a 0. A carry costs every digit it touches one 01, and a digit that runs out merges into the next. On overflow every digit swaps its halves and a digit is added.

The A file composes window lemmas into these rules and carries a per-step invariant (parities and lower bounds; architecture of SBCv6 TM21). B is that file with renamed states and its own start. D mirrors it by hand, keeping the invariant part verbatim, and C is the D file renamed.

Thanks to hipparcos for his analysis of `1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---` in his thread; §7 of its write-up answers his `C C0` right-end question.

All four compile against unmodified busycoq, Print Assumptions is closed, and coqchk passes.

AI disclosure: as before, produced with Claude Code (Opus 5.5). The results rest on the Coq files; extra verification and feedback are very welcome!

Also, I believe I have 4 new proofs for 4 holdouts (holdouts identified and proved non-halting with AI-assistance) that share one transition table but start in different states (A, B, C and D). So one proof idea, but four .v files. They are of the Skelet 1-like Class 2! :skull_crossbones:

`1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---` (the table started in A)
`1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---` (started in B)
`1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---` (started in C)
`1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---` (started in D; stored mirrored)

PR: https://github.com/ccz181078/busycoq/pull/15
Informal write-ups: attached

The mechanism is a binary down-counter on a list of (10)^p (01)^q pairs behind a left marker; when the counter runs out, the list is re-paired. The A-start proof proves each macro rule as a lemma and carries a per-step invariant (loose template: SBCv6 TM21). The other three reuse that file with renamed states and their own opening run; the D start goes through busycoq's flip/permute lemmas. All four compile against unmodified busycoq, Print Assumptions is closed, and coqchk passes.

AI disclosure: as before, produced with Claude Code (Opus 5.5) and checked by compiling against unmodified busycoq, with Print Assumptions and coqchk. I read through the main write-up, but the results rest on the Coq files; feedback welcome!

`1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---` (Bell eats counter, sheet row 1035) never halts. Coq proof: <LINK>

It is busycoq's SOMDCv6 TM7 (`1RB0RC_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---`) with A1 changed from 0RC to 0RF. The sweep config is the same, `0^inf 11 D> <r> 0^inf` over the digits L=110, 0=000, 1=100. The difference: whenever a sweep enters an L digit (eater or drain pass), A1 now runs one extra h-pass to the right. That pass adds +1 to the 0/1 digits (little-endian binary, L skipped) and comes back to exactly where TM7 is one step after its A1. The proof is TM7's with three changes:
- an `Inc` relation, added as a premise to the two L clauses of `RIncs`;
- two zero-pass end clauses, `RIncs h1 0 [D1] [LD]` and `RIncs h1 0 [D0] [D1]`. They are just `1 100 0^inf = 110 0^inf` and `1 000 0^inf = 100 0^inf`, but without them the domain is not closed;
- the domain lemma, redone with a count j of pending +1 passes. At j = 0 it reduces to TM7's conditions.
It is one file with a top-level `Lemma nonhalt: ~halts tm c0.`, built with Coq 8.20.1 against busycoq 0940bb9c. It compiles in about 4 s, `Print Assumptions` is closed, and coqchk passes.

AI disclosure: the informal proof and the Coq formalization were produced with Claude Code (AI-assisted) under my direction, and checked by compiling against unmodified busycoq, with Print Assumptions and coqchk.

The first candidate I discovered:

`1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---` (Bell eats counter, sheet row 1035)

My Coq proof that it never halts: https://github.com/DennisKoshta/busycoq/blob/59de13796aa9dbccedd52bc5d081e87980dd2f7e/verify/BellEatsCounter_1RB0RF.v
PR: https://github.com/ccz181078/busycoq/pull/14
Informal write-up: attached

It is very similar to busycoq's SOMDCv6 TM7 (`1RB0RC_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---`) with the only difference being that A1 changed from 0RC to 0RF. The sweep config is the same, `0^inf 11 D> <r> 0^inf` over the digits L=110, 0=000, 1=100. The behavioural difference: whenever a sweep enters an L digit (eater or drain pass), A1 now runs one extra h-pass to the right. That pass adds +1 to the 0/1 digits (little-endian binary, L skipped) and comes back to exactly where TM7 is one step after its A1. The proof is TM7's with three changes:
- an `Inc` relation, added as a premise to the two L clauses of `RIncs`;
- two zero-pass end clauses, `RIncs h1 0 [D1] [LD]` and `RIncs h1 0 [D0] [D1]`. They are just `1 100 0^inf = 110 0^inf` and `1 000 0^inf = 100 0^inf`, but without them the domain is not closed;
- the domain lemma, redone with a count j of pending +1 passes. At j = 0 it reduces to TM7's conditions.

It is one file with a top-level `Lemma nonhalt: ~halts tm c0.`, built with Coq 8.20.1 against busycoq 0940bb9c. It compiles in about 4 s, `Print Assumptions` is closed, and coqchk passes.

AI disclosure: as I mentioned above, the informal proof and the Coq formalization were produced with Claude Code (Opus 5.5), and checked by compiling against unmodified busycoq, with Print Assumptions and coqchk. I then manually reviewed everything, and it seems to check out, but I am quite new to this and so would appreciate extra verification and any feedback!