1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA: never halts

• Machine: 1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA, viewer https://bbchallenge.org/1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA. A BB(6) holdout on every holdout list from the June 2024 one (12,325 machines) to the current 740-machine list (line 381 there), class "Bell eats counter".
• Written for: the string itself. This is a delta write-up against the write-up for 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC, which is shipped alongside as parent-proof.md. Below, the parent is that machine and "parent §n" is section n of its write-up. This machine's table is the parent's, mirrored (every L↔R) and with its states renamed by σ: A↦E, B↦A, C↦B, D↦F, E↦C, F↦D (§1). So this machine from the blank tape is the parent started from 0^inf E> 0^inf instead of 0^inf A> 0^inf.
• Template: the parent's .v, whose development is reused verbatim for the parent's table. The parent's own template is verify/FractalBEC.v, tm10 (1LB0LF_1LC1LF_1RD1LB_---0RE_1RA0RE_0LA0RC), of which it keeps only the marker bounce RInc. Mirrored, tm10 differs from the parent only in C1 (parent §8.1). The mirror and the renaming use busycoq's verify/Flip.v (flip, flip_halts) and verify/Permute.v (Perm, perm_halts). Relative to the parent's .v, only the start, the finite part and the final transfer to this machine differ (§6). By table this machine is also one entry away from verify/BECv1_6x2_solved.v's tm10 (1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF1LE_---0RA: E1 is 0LA here and 1LE there), but that file's counter does not carry over, and nothing of it is used.
• Status: formalized in the accompanying 1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA.v (1,790 lines), which proves Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9c), importing only Individual62 from busycoq. Print Assumptions nonhalt: Closed under the global context. It compiles in about 17 s with -native-compiler yes, and coqchk re-checks it in about 72 s, most of it the finite part's vm_compute.
• Where each section lives in the .v:
• §1: tm, tm30 (the parent's table), phi, perm7, and busycoq's flip_halts and perm_halts inside nonhalt (end of Section 11);
• §2: solve_initE and init7 : E;; tape0 -->* K 17 t1 (Section 4);
• §3: the base of the write-up's induction at e5. The .v does not use it: it starts its induction at e692 with inv7 (§5);
• §4: Sections 1–10, and Section 11 up to orbit_sound, which are the parent's text, now about tm30;
• §5: B692, Y692, fin7 and inv7 (Section 11);
• §6: the whole file; the conclusion is nonhalt_from_c, nonhalt_E and nonhalt.

Summary

• The parent is a counter fed by a marker bounce. Its hub is K(a, b, X) = 0^inf (110)^a 0 (011)^b C> X 0^inf. Each bounce adds 1 to the counter word X, and at b = 1 the machine eats the lowest digit of X and leaves a residue. The next epoch restarts with budget N = k + 1 and digests the residue recursively. The parent's Lemma D shows that the digestion always fits in the budget (parent Summary, §5).
• This machine's table is the parent's, mirrored and renamed (§1). So from the blank tape it runs the parent's table from 0^inf E> 0^inf, on the mirror-image tape. That is a different orbit of the same epoch map.
• Its first four left records are outside the parent's invariant family. The fifth, L(16, 0001) at step 1,059, is inside it, and the restart gives the hub K(1, 17, t1) at step 1,114 (§2). There the parent's orbit invariant (I1)–(I4) holds: it is the parent's own base case "κ = 0, special", with t1 in place of t2 (§3).
• Everything else in the parent's argument is a statement about the table, about one epoch, or about the induction step, so it holds unchanged (§4).
• Only the finite part is new. This machine's orbit shares no epoch with the parent's below N = 20,000, so it is computed again: 587 epochs below the write-up's threshold N* = 14,796, and 687 epochs up to N = 17,724 for the .v's invariant (§5).

1. The conjugacy: this machine is the parent mirrored and renamed

       this machine            parent
      0     1               0     1
 A   1RB   0RA          A  1RB   0RF
 B   1LC   0LD          B  1RC   1RF
 C   1LE   1LD          C  1LD   0RE
 D   0LB   0RE          D  ---   0LE
 E   1RF   0LA          E  1LA   0LE
 F   ---   0RA          F  0RA   0LC

The map. Let σ send this machine's states to the parent's:

Its inverse sends the parent's A, B, C, D, E, F to this machine's B, C, E, F, A, D. For every state q and symbol s:

M[q][s] = (w, d, q') ⟺ P[σq][s] = (w, −d, σq'),

where M is this machine's table and P the parent's, and M[q][s] is undefined exactly when P[σq][s] is. The only such pair is this machine's F0 and the parent's D0. For example, this machine's A row 1RB 0RA becomes 1LA 0LE, which is the parent's E row.

• Uniqueness. Among all 720 permutations and both orientations, σ with the mirror is the only map that sends this machine's table onto the parent's (X1).
• Consequence. Map a configuration of this machine to its mirror image (cell x goes to cell −x) and rename its state by σ. One step of this machine then becomes one step of the parent's table. The start 0^inf A> 0^inf maps to 0^inf E> 0^inf. So this machine halts from the blank tape if and only if the parent's table halts from the blank tape in state E. In busycoq this is flip_halts plus perm_halts (§6). X2 checks the step-for-step correspondence over 2·10^6 steps, with full-tape comparisons at 27 intermediate steps.
• Reading configurations across the mirror. l q> r in the parent's frame is rev(r) <(σ⁻¹q) rev(l) in this machine's frame. The two configurations that §2 needs:
• L(16, 0001) = 0^inf <A 101 (001)^16 0001 0^inf is 0^inf 1000 (100)^16 101 B> 0^inf in this machine's frame;
• K(1, 17, 1) = 0^inf 110 0 (011)^17 C> 1 0^inf is 0^inf 1 <E (110)^17 0 011 0^inf in this machine's frame.
• A third start. The same table is on the holdout list a third time: 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB is the parent's table renamed, with no mirror, and it starts in the parent's state B (X1). It is not covered here.

From here on everything is in the parent's frame and uses the parent's notation (parent §2): hubs K(a, b, X), left records L(k, T), pre-records L'(k, T), the grammars G ⊂ O ⊂ H, the end words E*, budgets N = k + 1, ordinary and special residues.

2. Initial segment (direct simulation)

Start from 0^inf E> 0^inf and use the parent's table. Up to step 1059, the configurations of the form L(k, T) are exactly the five below. Here "of the form" means that state A reads a blank, every cell to its left is blank, and 101 follows. X3 checks this at every step, also with this machine's own table in its own frame.

• The machine gets through e2 and e3 by eats at non-G words that happen not to halt, just as the parent's own epoch 2 does (parent §6). This part is pure simulation, so no rule is claimed for it.
• e4's residue is outside the invariant family, so e5 is the first record from which every record is in the family. Every epoch from there on is also covered by the rules.
• At step 1059 the whole tape is exactly L(16, 0001). In this machine's frame it is 0^inf 1000 (100)^16 101 B> 0^inf.
• The restart R (parent §3.7, 3k + 7 = 55 steps) gives the hub K(1, 17, t1) at step 1114. In this machine's frame it is 0^inf 1 <E (110)^17 0 011 0^inf. X3 checks this tape cell by cell.
• No halt occurs before step 1114. X3 runs this machine's own table, and X2 runs the parent's table in lockstep with it.
• The column k is the record index of L(k, T), the number of 001 blocks. It is not the k of the parent's orbit invariant (parent D.6), which is k(W), the number of blocks of the residue's W (§3).

The next record is e6 = L(23, 000 10 00 010001) at step 2915, with N = 24.

3. The base of the parent's orbit induction, clause by clause

The parent's induction (parent §5, D.6) starts at its epoch 3: L(7, 000 t2), N = 8, a special residue, κ = 0. This machine's base is e5: L(16, 000 t1), N = 17, also a special residue.

The running maximum. In D.6, k_t is k(W_t), the number of blocks of the W in the residue Y_t = 11 a^x z W, and k(W) = 0 for a special residue. It is not the record index of L(k, T) in §2's table. The running maximum is taken from e5 on: κ_t := max_{5 ≤ s ≤ t} k(W_s). At the base, κ_5 = k(W_5) = 0: Y_5 = t1 is special and has no W. The record index of e5 is 16, but it does not enter the invariant. Read with it, (I4) would fail at the base, since N_lo(16) = 2^19 − 2^14 is far above 17. X4 checks both readings.

This is the parent's base case, "κ = 0, special", word for word, with t1 in place of t2. Both are tails in G, so the digestion is empty and the reset D.4(r) applies.

No earlier record can serve as the base. At e1 (N = 1) the budget is below β + 2. The induction step from e2 or e3 fails, because their digestion does not fit in N, and the parent's rules indeed do not cover those epochs. e4's residue is not in H, so (I1) fails there, although its epoch is computed by the rules and ends at e5. X4n checks all of this.

4. Why the rest of the parent's argument applies unchanged

The parent's argument has three kinds of parts. Statements about the table hold for every configuration. Statements about one epoch hold for any epoch K(1, N, Y) with Y ∈ H and enough budget. The rest is the orbit induction with its base and its finite part. Only the base and the finite part refer to the starting configuration.

Spelled out: - The induction runs from t = 5. While N_t < N*, the step "epoch t finishes" (β_t ≤ N_t − 2) is the explicit computation of §5. For N_t ≥ N* it is D.7, with the same case split on κ_t ∈ F. - Every epoch has N_{t+1} ≥ N_t + 1 (parent §4, corollary), so N reaches N* after finitely many epochs and stays above it. - Every epoch reaches the next left record. So the sequence of left records is infinite, and this machine never halts.

The parent's finite part cannot be reused. This machine's orbit from e5 shares no epoch (N, Y) with the parent's orbit from its epoch 3, nor with the third start's orbit, up to N = 20,000 (X6). The starts do not merge before the threshold, so this machine needs its own finite part.

5. The finite part

With the write-up's threshold (parent D.7, N* = 14,796). The rules-only orbit (parent §3, no TM inside) runs from K(1, 17, t1) (e5) on. - The epochs with N < 14,796 are e5 to e591, 587 epochs. e592 has N = 14,804. - None of them has an eat at a word outside G or a word without a rule, and each has β ≤ N − 2. - The parent's checks of Lemma D (parent §9) run on this orbit from e5 to N ≥ 400,000, and every link holds on every epoch (D, §7). - The same orbit equals the TM's left records, in a fresh simulation to 2·10^7 steps and in a C simulation to 10^11 steps (X5).

With the .v's invariant (parent §8.3: Inv, threshold 17,705). The parent's .v closes with the invariant ∃κ, Inv κ N Y (parent §8.3). Inv contains N ≥ 17,705, so the .v's finite part must run until N first reaches 17,705: - orbit f 687 17 t1 = Some (17724, Y_692): 687 epochs (e5..e691), landing at e692, the first record with N ≥ 17,705 (e691 has N = 17,670). In the .v this is fin7 : orbit 100000 687 17 t1 = Some (17724, Y692), by vm_compute, with Y692 := p11 16 (gw B692 0), where B692 lists the ten blocks of W below (§6). - Y_692 = '11' a^16 z W, with W = a(6) z a(1) z b(1) z b(1) z a(1) z b(1) z a(1) z a(1) z b(1) z a(0) (bare tail). So k(W) = 10 and m(W) = 4,396. - Inv 10 17724 Y_692 holds, clause by clause:

(κ = 11 also works; κ = 10 is the least.) From there inv_step carries Inv to every later epoch. It is proved in the parent's .v, does not depend on the start, and is kept verbatim. As a check, Inv also holds at every later epoch of the rules-only orbit, with κ the running maximum, up to N ≥ 400,000 (V2). - Cross-check. An independent implementation of the bound functions reproduces the parent's §8.3 table for κ = 8..13, and an independent implementation of the model reproduces the parent's fin694 (orbit 691 8 t2 = (17713, Y694)) and inv694 (Mw 77, M2 1,054) exactly (V0). It gives the numbers above, and the .v's fin7 and inv7 compute the same values in Coq.

6. The formal proof

The .v is the parent's .v, with a new start, a new finite part, and busycoq's bridge for a mirrored and renamed table. 1. Top of the file. tm := TM_from_str "1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA" (this machine) and tm30 := TM_from_str "1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC" (the parent). The three step notations -->, -->* and -->+ are on tm30. 2. Kept verbatim: Sections 1–10, and Section 11 up to orbit_sound. This is LP, Phi, sound, epoch_tm, the model, the potentials, Inv, next_inv, inv_step, the threshold, orbit and orbit_sound. None of it depends on the start. It refers to the machine only through the notations, so it is about tm30 unchanged. 3. Not taken over from the parent's .v: its three lemmas about its own start K(1, 8, t2) (init : c0 -->* K 8 t2, fin694, inv694), and its nonhalt_from and nonhalt, which are stated for the parent's own tm. Apart from these, the tm definition and the three step notations (now on tm30), the parent's code is kept verbatim (comments aside). 4. New (in Section 4 and at the end of Section 11): - init7 : E;; tape0 -->* K 17 t1, 1,114 steps from state E. The proof is unfold K. cbn - [tape0]. followed by solve_initE, which is busycoq's solve_init with its first line replaced by change (E, tape0) with (cconfig_to_config (nil,nil,S0,E)). Two tactic details: in this scope the literal 0 in a cconfig head parses as a nat, so the head symbol is written S0; and cbn -[tape0] collides with busycoq's -[ step-notation token, so it is written cbn - [tape0], with a space. - B692, Y692 and fin7 : orbit 100000 687 17 t1 = Some (17724, Y692) by vm_compute. It is about the size of the parent's 691-epoch fin694. - inv7 : Inv 10 17724 Y692, by the script of the parent's inv694 with x = 16 (exists 16, B692, 0). - nonhalt_from_c c N0 y0 P : c -->* K N0 y0 → P N0 y0 → (∀ N y, P N y → ∃ k y', Phi 1 N y k y' ∧ P (S k) y') → ~ halts tm30 c. This is the parent's nonhalt_from with the start made generic and tm30 in place of tm. - nonhalt_E : ~ halts tm30 (E;; tape0), from nonhalt_from_c with P N y := ∃ k, Inv k N y: the start is init7 followed by orbit_sound … fin7, the base is inv7 and the step is inv_step. - phi = σ (A↦E, B↦A, C↦B, D↦F, E↦C, F↦D) and perm7 : Perm (flip tm) tm30 phi, checked by case analysis over every state and symbol. - nonhalt : ~halts tm c0: flip_halts (the blank tape is symmetric, so the flipped start is A;; tape0), then perm_halts with perm7 (σ(A) = E), and nonhalt_E. 5. Every lemma is top level (no Section, Module, Hypothesis or Axiom). Besides busycoq's Individual62, the file imports only the stdlib Lia, String, List and Arith. Section numbers in its comments (write-up 3.x, D.x, Lemma C) refer to the parent's write-up.

7. Numerical checks

All of these are by direct simulation of the two transition tables, or by the rules-only model (no TM inside). They are evidence only; the result rests on the .v alone. The randomized checks ran with two seeds, and every check below passed. - X0: the string is on the 740-machine list (line 381), and exactly once on each holdout list since June 2024. - X1: σ with the mirror is the unique conjugacy of this machine's table onto the parent's, among 720 × 2 maps. This machine's start A is the parent's E. The third start 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB is the parent's table renamed, with start B. - X2: lockstep for 2·10^6 steps: this machine from blank in A against the parent's table from blank in E, mirrored and renamed. States and positions are compared at every step, and the full tapes at 27 intermediate steps. No halt. - X3: with this machine's own table, the L-form configurations up to step 1059 are exactly e1–e5 (steps 15, 81, 183, 573, 1059). The tapes at steps 1059 and 1114 are exactly the mirrors of L(16, 0001) and K(1, 17, t1). The parent's table from E gives the same records, and the hub at step 1114 = 1059 + 3·16 + 7. - X4: (I1)–(I4) at e5, with κ_5 = k(W_5) = 0 (not the record index 16; N_lo(16) = 2^19 − 2^14 > 17), Γ(0, 0) = 0, G(0) = 0 and N_lo(0) = −8. e5's epoch ends at e6 = L(23, 000 1000010001). X4n: e1–e4 are not a valid base, and e4's epoch, although it is rule-covered, starts outside the family. - X5: the rules-only orbit from e5 equals the TM's left records. - A fresh simulation to 2·10^7 steps: 46 records, of which 41 are compared, from e6 on. - A C simulation of the parent's table started in E, to 10^11 steps: 517 records, of which 512 are compared, from e6 to N = 12,674. - Neither run halts. - X6: the third start's first records (the parent's table from B) are L(0, '')@4, L(2, 0001)@42 and L(7, 0001)@194. The orbits of this machine (from e5), of the parent (from its epoch 3) and of the third start (from L(2, 0001)) share no epoch (N, Y) up to N ≥ 20,000. - D (the parent's checks of Lemma D, parent §9, from e5): to N = 400,004, that is 11,077 epochs, e5 to e11,081. On every epoch: Lemma C, D.1–D.5 (D.4(a)–(c), (e), (r) included), the orbit invariant of D.6, and the bounds of D.7 (β ≤ Bnd ≤ Bnd_worst(κ_t) and β ≤ N − 2). - Finite part below N*: 587 epochs. N* is first reached at e592, with N = 14,804. - Special residues: 2 in G, 4 end words. - Not used by the proof: c_t ∈ {0, 1} (7,134 and 3,943 epochs), β/Bnd ≤ 0.3788, κ = 15 at the end. - V: V0 checks the implementation against the parent's §8.3 table and the parent's fin694 and inv694. V1: orbit 687 17 t1 = (17724, Y_692), that is, 687 epochs (e5..e691) landing at e692, with N = 17,670 at e691; Inv 10 holds at e692. V2: Inv holds at the 10,389 later epochs, up to N ≥ 400,000 (κ goes up to 15). - The parent's table-level checks (parent §9), unchanged: W1–W11, S1–S3, RP0/RP1, the LP rules, D6, B, E1g/E2g/E0/Et1–Et3, R, H1/H2 (10,529 H words), the end of digestion (D.0/D.3), the threshold (N* = 14,796, F = {0..11}, the κ ≥ 64 tail), and the adversarial residues (1,504 per seed, 40 TM epochs). They depend only on the table, and they pass here as they do for the parent.

Gaps: none.

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