A proof that one BB(6) holdout of class Skelet 1-like Class 2 halts: 1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB (sheet row 1286). It halts after about 1.77 × 10^44 steps. The Coq proof shows only that it halts; the step count is computed outside Coq (see below).

No other holdout has this table under a state renaming or the mirror. A separate PR covers the other table of this batch, 1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---, and the two holdouts that are that table (renamed, one of them also mirrored) from other start states.

One file, verify/Skelet1LikeC2Halt_1RB0RD_1LC0RA.v (1,142 lines), with a top-level Lemma halt: halts tm c0. for this string. It imports Individual62, LongitudinalHalt, Flip and Eqb from busycoq.

Where it can halt. The only halting transition is C0. C is entered only by B0 and E0, and in every case except B0 right after F1, C reads a 1. So the machine halts exactly when the head is in F on a 1 whose two left neighbours are 0 0:

0 0 1      with F on the 1

The counter. A right record is a configuration with the head in A on a blank cell and only blanks to its right. An increment is the run from one right record to the next.

At right records the tape reads as walls (maximal runs of at least two equal symbols) and gaps (the alternating stretches between them, given by their length):

0^inf  E  U_0  b_1  U_1  b_2  ..  b_n  U_n  b_T  [t]  A>

U_i = [x, M, m_1, Q_1, .., Q_r, y]        a digit, i >= 1

• The boundaries b_i (11, or longer when walls are glued onto them) cut the tape into units. E is the edge at the far left, U_0 is the unit next to it, and [t] is the tail next to the head.
• In a digit the lead M is the bit (00 = 0, 1111 = 1), Q_1, .., Q_r are passive walls (or stacks of glued ones), and the last gap y is the fuel.
• U_n, next to the tail, is the least significant digit.

Each increment is one carry from the right. It passes the digits with bit 1 and stops at the first digit with bit 0. Every touch flips the bit and burns fuel: y − 1 in a single-marker digit (r = 0), y − 2 in a multi-marker one.

Why it runs out of fuel.

• A multi-marker digit whose fuel runs out glues its last passive wall onto the boundary to its right. At the next pass that wall enters the right neighbour as its new lead. So walls drift toward the head and refill digits that run low.
• A single-marker digit has no wall to hand on. A carry that touches it as [x, 00, 0] finds the lead 00 right next to the 11 boundary, reaches that 11 in F, and halts.
• At each reset a new least significant digit is born, with the old tail as its fuel. Roughly, the counter survives while the time between resets less than doubles.
• That ratio oscillates with growing swings. Its peaks are 1.882 at reset 45 and 1.977 at reset 62, and at reset 82 it is 1.969 and still rising.
• After reset 82 the next reset never comes. The digit next to the least significant one runs dry, its left neighbour is single-marker, and the carry of increment 11,631,266,794,472,450,654,093 (counted from the right record at step 342) halts the machine.

Proof (verify/Skelet1LikeC2Halt_1RB0RD_1LC0RA.v).

The proof is a checked replay of the run, built on one general lemma per kind of carry step. Everything runs in the mirrored machine tmf = flip tm, where the counter lies to the right of the head, and halt is flip_halts_iff applied to halt_tmf.

The rules.

• Each touch is one parametric lemma, stated with the call-segment predicates of verify/Individual.v as instantiated in verify/Individual62.v:
• t_stop (segRL), and t_pass, t_ungl1, t_ungl2 (segRLs, one call forwarded to the next unit);
• z_lead, z_empty, z_absorb, z_stop, z_1111 for the unit next to the edge (sideRL);
• root_step, reset1 and reset2 for the tail and the resets;
• t_halt, the halting touch (halts tmf ..).
• Each is proved from short fixed-word cores (solve_seg, es) and generic composition. Runs of passive walls are crossed by chainRR/chainLL (list induction), and gen_RL, gen_fwd, gen_side put a core behind any such run.
• The halting touch is carried out through the rest of the carry with the halting streams of verify/LongitudinalHalt.v (sideRLs_halt, segRLs_sideRLs_halt_concat).

Records and batches.

• A configuration at a right record is a record with binary-number fields (unitN, zN, tailN, cfg), and denote maps it to a tape.
• inc1 computes one increment on records (touchN, ztouch, callN). inc1_ok and inc1_halt prove it sound.
• Between structural events (glue, unglue, resets, edge events) every change is linear in the number of touches. batchL applies d increments in closed form, proved by closedU_spec, closedZ_spec and batchL_spec (from the pair lemmas pairK, pair1).
• d comes from propose, which is untrusted. Every batch is checked by the guards of closedU/closedZ, and when no batch is allowed, next does one exact increment.

The run.

init     : c0 -[tmf]->* denote c342                 (* 342 steps, solve_init *)
run T c  := N_iter_until next (inl c) T
s_i      : run 5000 k_(i-1) = inl k_i               (* i = 1 .. 21, k_0 = c342 *)
s22      : run 5000 k21 = inr tt                    (* the halt *)

• run_ok and run_halt follow from N_iter_until_spec and next_spec.
• The halting touch is move 107,781 (move 2,781 of the last chunk). About half of the moves are batches.
• Each s_i is vm_cast_no_check (eq_refl _), so the kernel checks it when the lemma is closed, and coqchk checks it again. The k_i are Eval vm_compute definitions, certified by the s_i.
• The run is cut into 22 chunks so that coqchk fits in memory; one cast over the whole run did not.

Relation to verify/Sk1Machines.v (Module TM91, a halting Skelet 1 machine, and Module Sk1Auto).

Step count (computed, not proved). From the blank tape, the halting step included:

N = 176,522,930,997,643,289,094,015,905,898,381,767,890,130,463  ≈ 1.77 × 10^44

In busycoq's convention this is halts_in tm c0 (N − 1). The .v does not prove this number.

• N sums one step-cost formula per kind of carry action (section 9 of the write-up) over the same run.
• The formulas agree with direct simulation on all 276,427 increments from step 342 to 10^11 steps. They were also checked on smaller tapes of the same shape for each of the 53,973 increments that the count takes one at a time.
• A second implementation of the run, written from the transition table alone, halts in the same increment, after the same 82 resets and through the same configuration three increments before the halt. It does not count steps.

Checked on this branch (BB6 @ d026880) with Coq 8.20.1. The framework .vo files were built with make at 9cf9e88 and reused: d026880 differs from 9cf9e88 only by the eight Skelet1LikeC2 files of PR 15 and PR 16, so the framework is the same. Then, in verify/:

coqc -Q . BusyCoq -Q ./BigInt BigInt -native-compiler yes Skelet1LikeC2Halt_1RB0RD_1LC0RA.v
Print Assumptions Skelet1LikeC2Halt_1RB0RD_1LC0RA.halt.
coqchk -Q . BusyCoq -Q ./BigInt BigInt -norec BusyCoq.Skelet1LikeC2Halt_1RB0RD_1LC0RA

functional_extensionality_dep comes from the framework lemma flip_halts_iff.

coqchk re-checks the 22 vm_cast_no_check chunks, and with them the whole run. The times were measured on a lightly loaded machine.

File name. As in PR 15 and PR 16, the name is the class name plus the first transitions, here four, because verify/Skelet1LikeC2_1RB0RD.v is already taken by PR 15 for another machine. Halt right after the class name marks a halting proof, as in verify/CubicCapHalt.v and verify/ChaoticBell1Halt.v.

Happy to rename it if you prefer another name.

Informal write-up: in the bbchallenge Discord (#bb6).

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 and coqchk. The results rest on the Coq files; extra verification and feedback are very welcome.

🤖 Generated with Claude Code