1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB halts

• Machine: 1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB, a BB(6) holdout (https://bbchallenge.org/1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB).
• Class: "Skelet 1-like Class 2".
• Result: Lemma halt: halts tm c0. in Coq 8.20.1 against unmodified busycoq (commit 0940bb9). Print Assumptions halt lists only functional_extensionality_dep, from the framework's flip_halts_iff.
• Check time: it compiles in 70.0 s with -native-compiler yes, and coqchk re-checks it, the computed run included, in 536.5 s.
• Halting time: 176,522,930,997,643,289,094,015,905,898,381,767,890,130,463 ≈ 1.77 × 10^44 steps, the halting step included. This count is computed from per-rule step costs over the same run (section 9 of the write-up); the .v proves halting, not the count.

Mechanism

• At each right record the tape is a binary counter of units [x, M, m_1, Q_1, …, y] cut by 11 walls. The lead M (00 or 1111) is the bit, the Q are passive walls, and the last gap y is fuel that every carry burns.
• Walls migrate toward the head: a multi-marker unit whose fuel runs out glues its last wall onto its right boundary, and the next time the right neighbour is passed, that wall becomes the neighbour's new lead. New digits are born at the right end (resets), and old walls fossilize at the left edge.
• The times between resets grow by a factor that oscillates with growing swings. When it nears 2, a single-marker digit gets bit 0 and no fuel, and the next carry into it halts the machine (F reads a 1 after 00), during increment 11,631,266,794,472,450,654,093 after step 342.

How the proof works

• Rules. Every kind of carry step is one parametric lemma on the mirrored machine (t_stop, t_pass, t_ungl1, t_ungl2, t_halt, five lemmas for the unit next to the edge, root_step, reset1, reset2), proved by solve_seg / es on short words plus generic composition.
• Records. Configurations are records with binary numbers; inc1 computes one increment, and inc1_ok / inc1_halt prove it sound.
• Batches. Between structural events the changes are linear, so batchL applies d increments in closed form (closedU_spec, closedZ_spec, batchL_spec). The batch size comes from an untrusted propose, and every batch is guarded.
• The run. init reaches the step-342 configuration by solve_init. Iterating next (a batch, else one increment) reports the halt at move 107,781. The run is checked in pieces of 5,000 moves by vm_cast_no_check: s1 … s21 are full pieces, and s22 ends in the halt. halt is flip_halts_iff applied to halt_tmf.

Template

verify/Sk1Machines.v, Module TM91 (a halting Skelet 1 machine) with Module Sk1Auto: a checker iterated by Eqb.N_iter_until and proved sound once (check_spec), with untrusted proposals certified at each use. - Kept: the checker architecture (one step function iterated by N_iter_until and proved sound with N_iter_until_spec: advance on run-length tapes there, next on unit records here), the call-segment calculus of verify/Individual.v (instantiated in verify/Individual62.v), and sideRLs_halt of verify/LongitudinalHalt.v. - Changed: the records are this machine's units (stack lists with binary-number gaps) instead of run-length tapes; the rules are unit-level lemmas rather than scans; closed-form batches replace bulk steps; and the run is split into 22 chunks so that coqchk finishes.

Files

• 1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB.v: the proof (1,142 lines), upstream verify/Skelet1LikeC2Halt_1RB0RD_1LC0RA.v.
• The informal write-up and the full output of the automated checks (statement, forbidden tokens, compile, Print Assumptions, coqchk).

AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).