1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---: never halts

• Machine: 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---, viewer https://bbchallenge.org/1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---
• Holdout: on the current BB(6) holdout list (class "Skelet 1-like Class 2"). Not in busycoq.
• Existing work: There may be existing work on this machine by hipparcos (marked done on the community sheet, not yet in busycoq). The sheet's entry for this string links his bbchallenge Discord thread of October 2025 (https://discord.com/channels/960643023006490684/1432566675533992019). Its opening posts analyse this machine (block rules, a stride acceleration, and conjectures on which exponents can reach zero) and say that a proof is not yet in hand. The proof below is adapted from the parent's proof (next item), not from that thread; §7 relates the two.
• Written for: the string itself. The TM_from_str of the .v is this string; no Flip/Permute bridge is used.
• Parent: this is a delta write-up. It relies on the write-up for 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---, called "the parent" below and included as parent-proof.md. "P§n" means §n of that write-up. This machine is the parent's table with its states renamed by τ = (A,B,C,D,E,F) ↦ (E,A,B,C,D,F), with no mirror. So it runs the parent's table started in the parent's state B (§0).
• Template: the parent's .v (694 lines, sha256 8bca47b193b15a0cbd664fcbafa9bf6a39dfc4c9ca261e1d8f95cb0f425553c0), which follows the architecture of busycoq verify/SBCv6.v Module TM21 (a binary counter over digit pairs with a re-pairing overflow). This machine differs from the parent only in state letters, never in a symbol or a direction: row τ(s) here is the parent's row s with each target t replaced by τ(t). The .v differs from the parent's .v in the TM string, τ applied to every state name, and the initial segment with its base case (§5).
• Status: formalized in the accompanying 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---.v (702 lines). It proves Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9c). It compiles in about 9 s (-native-compiler yes), Print Assumptions nonhalt gives "Closed under the global context" (no axioms), and coqchk re-checks the compiled file.
• Where each section lives in the .v: §0 tm; §1 the window lemmas S1_1–S6_1, S1–S6, T1–T14, the digit lemmas Lb, Lf, Rb, Ro, the family K, the sweeps LbS, RbS, RoS, the rules M_spec, Mdrop_spec, O_spec, the invariant INV and its closure step; §2 init and the base goal in nonhalt; §3 nonhalt. The full map is in §5.

Summary. This is the parent's binary counter, with head state A where the parent has B. At each return to the right edge the tape is K = 0^inf 10 01 d_1 .. d_m (10)^a 000 (10)^b A> 0^inf, with digits (10)^u 00 (01)^v (bit 0) and (10)^u (01)^v (bit 1). A carry M adds 1 to the counter, an overflow O re-pairs the halves of every digit, and the three-class invariant INV = Common ∧ (A ∨ B ∨ C) of P§3 is closed under M and O. τ is a pure renaming of states (Lemma R, §0), so every window lemma, rule, step formula and the whole invariant argument carry over word for word. The invariant is not adjusted. Only the start differs, because this machine starts in what is the parent's state B: from the blank tape it follows a different orbit of the same macro map and reaches the INV state K((1,1,10); 8, 1) (class A) at step 732, where the parent reaches K((1,1,2); 8, 5) at step 483. The proof is that 732-step initial segment, a base-case check, and the parent's induction.

0. The map

τ: A↦E, B↦A, C↦B, D↦C, E↦D, F↦F (a 5-cycle on A–E). Row τ(s) of this table is the parent's row s with every target state t replaced by τ(t); symbols and directions are unchanged. For example, the parent's C1 = 0RB becomes 0Rτ(B) = 0RA, which is this machine's B1. Among all 720 state renamings, each with and without mirroring, τ without mirror is the only map from the parent's table to this one.

Lemma R (relabelling). For a configuration c, let τc be c with its head state renamed by τ; the tape and head position stay the same. Then c → c′ under the parent if and only if τc → τc′ under this machine, and c is halted exactly when τc is (F1 is the only undefined cell, and τ fixes F). So every run c →ⁿ c′ of the parent gives a run τc →ⁿ τc′ here, of the same length, and conversely.

Proof. If the parent has δ(s, x) = (y, d, t), this machine has δ(τs, x) = (y, d, τt) by the table above. ∎

Start. This machine's c0 is 0^inf A> 0^inf = τ(0^inf B> 0^inf). So its run is τ of the parent's table run from 0^inf B> 0^inf. This is not the parent's own run, which starts in A.

Halting cell. Only D1 = 1LF enters F (it is τ of the parent's E1), and F1 is ---. So the machine halts exactly when D reads 1 with a 1 to its left.

The four holdouts with this table. Up to renaming and mirroring, four holdouts share this transition table: the parent (start A), this machine (start B), 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB--- (mirrored, start C) and 1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA--- (mirrored, start D). Each has its own .v; this write-up and its .v cover only the string above.

1. What carries over unchanged

Head notation as in P§2.1: X> puts the head in state X on the next cell, and <X on the previous cell. The window lemmas on this table, with their transitions:

      window lemma                 steps  transitions
S1    A>01       -> 10A>             2    A0 B1                 one block of A> (01)^n -> (10)^n A>
S2    B>10       -> 01B>             2    B1 A0                 one block of B> (10)^n -> (01)^n B>
S3    01<C       -> <C10             2    C1 D0                 one block of (01)^n <C -> <C (10)^n
S4    10<D       -> <D01             2    D0 C1                 one block of (10)^n <D -> <D (01)^n
S5    B>1101     -> 10B>11           6    B1 A1 B0 C0 E0 A1     one block of B> 11 (01)^n -> (10)^n B> 11
S6    0A>10      -> 100A>            6    A1 B0 C0 E0 A1 B1     one block of 0 A> (10)^n -> (10)^n 0 A>
T1    A>00       -> <D01             3    A0 B0 C1              (on 0^inf)
T2    000<D      -> 100A>            5    D0 C0 E0 A1 B1
T3    100<D      -> <D011            3    D0 C0 E1
T4    01<D       -> <C11             2    D1 F0
T5    10<C       -> <D01             2    C0 E1
T6    00<C       -> 10B>             3    C0 E0 A1
T7    B>11       -> 00B>             2    B1 A1
T8    B>11011    -> 10000A>          9    B1 A1 B0 C0 E0 A1 B1 A1 B1
T9    0001001<D  -> 1001000A>       13    D1 F0 C0 E1 D0 C0 E0 A1 B1 A0 B1 A1 B1    (0^inf 1001 <D)
T10   A>11       -> 00A>             2    A1 B1
T11   A>0        -> 1B>              1    A0
T12   B>11000    -> <D01101         13    B1 A1 B0 C0 E0 A1 B1 A0 B0 C1 D0 C0 E1    (B> 11 0^inf)
T13   101<D      -> <D011            3    D1 F0 C1
T14   A>1101     -> 0010A>           4    A1 B1 A0 B1

The digit lemmas of P§2.1 read the same with the head states renamed: Lb (10)^u (01)^v <D → <D (01)^u (10)^(v−1) 11, Lf (10)^u 00 (01)^v <D → (10)^(u+1) (01)^(v−1) B> 11, Rb B> 11 (01)^u (10)^(v−1) 11 → (10)^u 00 (01)^(v−1) B> 11, Ro A> (01)^u (10)^(v−1) 11 → (10)^(u−1) 1 (10)^(v−1) 000 A>, with the step counts and side conditions of P§2.1.

The rules in busycoq comment style, for this machine:

1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---     (= tau of 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---, tau = EABCDF)

K(d_1 .. d_m; a, b) := 0^inf 10 01 d_1 .. d_m (10)^a 000 (10)^b A> 0^inf
digit (u,0,v) := (10)^u 00 (01)^v,   (u,1,v) := (10)^u (01)^v      (d_m least significant)

start from K((1,1,10); 8, 1)                                  (step 732, section 2)

M  (carry; some bit is 0; j* = index of the LAST bit-0 digit, k = m - j*):
   K(.., (u,0,v), (u_j,1,v_j)_{j*<j<=m}; a, b) --> K(.., (u+1,1,v-1), (u_j,0,v_j-1)_{j*<j<=m}; a+1, b+2)
   steps 32 + 8a + 8b + 4v + sum_{j>j*} (8 u_j + 4 v_j);  needs v >= 1, u_j, v_j >= 1 (j > j*), a, b >= 0
   if v = 1, the digit (u+1,1,0) drops (re-reading, P section 1)
O  (overflow; all bits 1):
   K((u_1,1,v_1) .. (u_m,1,v_m); a, b) --> K((0,0,u_1), (v_1-1,0,u_2), .., (v_{m-1}-1,0,u_m), (v_m,1,a); b+3, 1)
   steps 89 - 4m + 8a + 20b + 4 sum u_j + 8 sum v_j;  needs m >= 1, all u_j, v_j >= 1, a >= 1, b >= 0
O at m = 0:  K(; a, b) --> K((1,1,a); b+3, 1)   in 89 + 8a + 20b steps (a >= 1); used only inside the initial segment

We write M_k for an M step with k = m − j* trailing bit-1 digits. O at m = 0 is the derivation of P§2.3 with no digits (no Lb and no Ro).

The invariant, restated from P§3 (derived quantities as in P§1):

INV(d_1..d_m; a, b) := Common /\ (A \/ B \/ C)
Common: m >= 1; canonical (every v_j >= 1, every bit-1 u_j >= 1); a >= 1; b odd; a + R_tot even;
        S >= 0; T >= 0; vbar_m >= 1
A:      d_1 = (0,0,v) with v >= 2, or d_1 = (1,1,v); for all j, vbar_j >= 1 and ubar_j odd; S >= 1
B:      d_1 = (0,0,1); for all j, v_j + beta_j odd; for j >= 2, ubar_j >= 2^(j-1)
C:      for all j, v_j + beta_j odd and ubar_j >= 2^j; S >= 1; T >= 2

2. What changes: initial segment and base (replaces P§4)

A K-configuration is state A on a blank cell with only blanks to its right, with the tape to its left parsing as a K. Direct simulation of this machine from the blank tape finds them exactly at these steps up to 732. (The parent's table run from 0^inf B> 0^inf gives the same list, as Lemma R says.)

Each leg is an instance of the rules of §1: 141 = 89 − 4 + 16 + 20 + 4 + 16; 100 = 32 + 32 + 8 + 4 + (16 + 8); 100 = 32 + 40 + 24 + 4; 269 = 89 + 80 + 100. The M_1 at step 263 flips the top (0,0,1) to (1,1,0), which falls into the next digit: (2,0,1) becomes (3,0,1). The M_0 at step 363 flips (3,0,1) to (4,1,0), which joins the block: a = 5 + 1 + 4 = 10. Two legs use rule cases the invariant argument never needs (the LSB drop, and O at m = 0). That does not matter: the proof uses the 732-step run only as one finite computation, and the table only explains it.

For comparison, the parent's run has K-configurations at 142, 283 and 383 (not in INV) and reaches its base K((1,1,2); 8, 5) at 483 (P§4). The mirrored C-start 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB--- reaches K((1,1,9); 8, 1) at step 687.

INV at the base K((1,1,10); 8, 1): - top (1,1,10): bit 1, u_1 = 1; m = 1; - V = 1, R_tot = R_1 = 0, R1_1 = 0; - ubar_1 = 1 (odd), vbar_1 = 10 ≥ 1 (also the LSB condition); - S = 8 + 0 − 2 = 6 ≥ 1, T = 1 − 1 = 0 ≥ 0 (tight, as at the parent's base); - a = 8 ≥ 1, b = 1 odd, a + R_tot = 8 even; - so Common holds, and class A holds (top (1,1,v), every vbar ≥ 1, every ubar odd, S ≥ 1).

In the .v, INV is the parent's additive form (P§6): R = Rof ds is computed by structural recursion on the least-significant-first digit list, and the clauses carry no subtraction or division. At ([d1 1 10], 8, 1), with m = 1 and 2^(m+1) = 4, its 12 clauses are: - ds ≠ [], a = 8 ≥ 1, b mod 2 = 1, (a + R) mod 2 = 0 with R = 0; - a + R + 2 = 10 ≥ 4 (S ≥ 0), b + 3 + 2R = 4 ≥ 4 (T ≥ 0), LSBok: v_m = 10 ≥ R + 1; - class A: a + R + 1 = 9 ≥ 4 (S ≥ 1), and PA (d1 1 10) 0 0, which is canonical (1 ≥ 1, 10 ≥ 1), 10 ≥ Rd + 1 = 1, ub = 1 odd, and ub = 1 for the top digit.

Every clause is linear arithmetic on constants, so the parent's own tactic line for its base goal closes this one (§5).

3. The argument (complete)

Theorem. 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC--- does not halt from the blank tape.

1. Initial segment. The machine runs from c0 to K((1,1,10); 8, 1) in exactly 732 steps without halting. This is a finite exact computation (§2); in Rocq it is init, proved by solve_init.
2. Base. INV([(1,1,10)], 8, 1) holds, in class A (§2).
3. Transfer. P§3.2 (coverage) and P§3.3 (closure): every INV state has a macro step M or O, of at least 32 machine steps, to an INV state. These statements are about the triples and a, b, and the macro steps are rule instances K → K′ of the parent. By Lemma R, each such instance is a run τK →⁺ τK′ of this machine of the same length, and τK is the K of §1. So coverage and closure hold verbatim for this machine's K-configurations.
4. Conclusion. By induction from the base, the run is an infinite chain of macro steps, each of at least one machine step, so it never halts (progress_nonhalt_cond with P := INV, as in P§5). No macro step reaches the halting cell: each is an exact computation from one K to the next, composed of window lemmas in which F reads only 0. ∎

The parent's invariant argument (P§3) never refers to the parent's own orbit, so it applies to this orbit unchanged. The parent's orbit statistics (P§7) are evidence there, not premises.

4. How this orbit relates to its siblings (remark, not used in the proof)

In the shared triple notation, three of the four starts of this table run orbits of the same macro map that lock together: - With the mirrored C-start 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB--- (base K((1,1,9); 8, 1) at step 687): from macro step 0 on, the two states are equal except for one exponent, larger by 1 here, on the top digit, and the same rule fires at every macro step. - With the parent (base K((1,1,2); 8, 5) at step 483): from macro step 54 on (step 25,851 here, 25,618 in the parent), the states are equal except for one top-digit exponent, larger by 4 here, with the same rule at every macro step. - Where the extra exponent sits: v_1 in class A, u_2 in class B (where the top is (0,0,1)), u_1 in class C. O sends it from v_1 to digit 2's u (A → B), the top fall merges it into the new top's u (B → C), and the next O sends it to the new top's v (C → A). - Both couplings were checked on the abstract macro orbits for 1.2·10⁶ macro steps (to t ≈ 3.7·10¹² machine steps, 93 overflows).

This matches the tape widths at 10⁹ steps: 77,693 cells here, against 77,685 for the parent (+8 cells, four 10/01 blocks) and 77,691 for the C-start (+2 cells, one block). The D-start 1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA--- runs a different orbit (76,245 cells at 10⁹ steps).

5. The .v file

The .v is the parent's .v (694 lines, sha256 8bca47b193b15a0cbd664fcbafa9bf6a39dfc4c9ca261e1d8f95cb0f425553c0) with exactly these changes: 1. TM_from_str "1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---". 2. τ applied to every state name {{X}}, simultaneously: {{B}} → {{A}} (22 occurrences), {{C}} → {{B}} (18), {{D}} → {{C}} (5), {{E}} → {{D}} (18). The parent's file names neither A nor F. This covers the window lemmas, the digit lemmas, the sweeps (LbS, RbS, RoS), the chunks and K. The es/follow proofs re-close unchanged, because τ maps each transition of the parent's table to a transition of this one (Lemma R). 3. Lemma init: c0 -->* K [d1 1 10] 8 1. (732 steps, proved by the parent's unfold K, L0. cbn. solve_init.), and in nonhalt, change (K [d1 1 10] 8 1) with (Kc ([d1 1 10], 8, 1)). The base goal is closed by the parent's own tactic line (§2). 4. The header comment, the three chunk comments that name head states, the banner of the invariant part, and the rule block at the end.

Every other line is the parent's text: every proof script, the statements and proofs of M_spec, Mdrop_spec and O_spec, dg, map0, map1, Oz, Oout, INV, step, and the structure of nonhalt. The file imports only Individual62 from busycoq (plus the stdlib ZifyNat, Lia, String, List, Arith), has one TM_from_str, and has no Section, Module or Hypothesis. The closure lemma is called step, as in the parent; it shares its short name with the framework's step function, which is harmless because the final statement uses only tm, halts and c0.

Lemma R is not a premise of the formal proof. Every window lemma, and through them every rule, is proved by es and follow on this machine's own table; Lemma R explains why the parent's scripts close on it. The step counts are not part of the formal statement (the .v proves -->+ for each rule).

6. Numerical checks

These simulation checks are independent of the .v; the result rests on the .v alone. - Table: τ without mirror is the only one of the 720 × 2 renamings that maps the parent's table to this one (12 of 12 cells). D1 is the only cell that enters F, and F1 is the only undefined cell. - Lockstep: from the blank tape, this machine and τ of the parent's table run from 0^inf B> 0^inf agree at every step to 2·10⁷ (state, symbol written, move), with identical tapes at the end. - Window lemmas: each of the 20 lemmas of §1 runs exactly as stated on this table, never reading outside its window, with τ of the parent's transitions. F is entered only in T4, T9 and T13, and reads 0 each time. - Rules: M on 700 random K-configurations (k = 0..6; 273 with a drop, 257 with u* = 0; a, b ≥ 0) and O on 350 (m = 1..7) give exactly the stated result and step count. The leftmost cell read is the first 0 of the flipped 00 (M) and 3 cells left of the leading 1001 (O). 2,868 random INV states, run on the machine for one macro step, give exactly the predicted successor. - Chains: every link of the parent's M and O chains (P§2.2–2.3), renamed by τ, holds on this table (whole tape, head and state) in 47,216 of 47,216 cases: M 37,220 and O 9,995 (exhaustive boxes, O including m = 0, plus random cases), and the initial leg K(; 10, 5) → K((1,1,10); 8, 1). - Initial segment: from blank, K-configurations occur exactly at steps 122, 263, 363, 463 and 732, with the legs of §2. The parent's table from 0^inf B> 0^inf gives the same list. - Real run: all 19,332 macro boundaries from step 732 to step 999,838,005 match the model (whole tape, head and state), and INV holds at each (class A 7,523, B 6,307, C 5,502). Rules used: O 53, M_0 9,639, M_1 4,846, M_2 2,422, M_3 1,209, M_4 602, M_5 298, M_6 and above 262; drops: 30 of the top digit, 12 of a middle digit. - Abstract orbit from the base: INV holds at each of 1.2·10⁶ macro steps (t ≈ 3.7·10¹² machine steps, 16 digits, 93 overflows). - Random INV states (not only reachable ones): 600,000 of 600,000 single macro steps land in INV, each of at least 32 machine steps; all six class transitions A→A, A→B, B→B, B→C, C→A, C→C occur. The drop closed forms of P§3.1 (F2) hold on 20,000 random cases with m = 2..12 and every j*. - No halt in 10⁹ steps from blank; the tape then spans 77,693 cells, 38,841 of them nonzero.

7. Relation to hipparcos's analysis

This section translates hipparcos's analysis (the thread in the header) and says what INV decides about it; it is not used in the proof.

Dictionary. His token n is 1 0^n left of the head and 0 1^n right of it (X = 1, C = 2, C0 = 0, Cs = 4); R = 0^inf, L0 = 0^inf 1001, L3 = 0^inf 1001000; > = A>, b> = B>11, < = <D. In his order, his 14 block rules are S1, S5, S4, T9, T2, Lf with v = 1, T1, T12 less its last 3 steps, T3, T13, T2, T8, T11, Lf with v = 1. - K(d_1..d_m; a, b) = L0 w_1 C0 … C0 w_m C0 X^(a−1) Cs X^b > R, with w = X^(u−1) C X^(v−1) for bit 1 and X^(u−1) Cs X^(v−1) for bit 0; a top (0,0,v) gives L3 X^(v−1) for L0 w_1 (below the top, u ≥ 1 in the run). - His cycle is one turn A → B → C → A. L0 < r is the far-left turn T9 of an overflow from class C, with r = Π_j (X^(u_j−1) C X^(v_j−2) C) X^a C X^(b+2) R for its state K((u_j,1,v_j)_{j≤m}; a, b); L3 < f(r) is the class-A carry into the top, L0 C < f²(r) the overflow from class A, L3 C0 < g(f²(r)) the top fall. So passes 1–2 are class A, 3 is B, 4 is C; his first group is the u_j − 1 and a, his second the v_j − 2 and b + 2; his collisions Cs C0 < are the other drops.

His rules and hypotheses. - Block, stride and collision rules, the cycle, and the exponent table without collisions: true. His 14 rules alone, from L0 b> X^2 R at step 24, reproduce the run to step 10⁹; they miss only C0 C0 < (a halt) and C C0 <. - Collisions only in pass 4: true. INV gives passes 1–2 (class A has no drops) but allows drops in class B. There the top falls by L3 C0 < and the LSB never drops; every other digit j starts with v equal to the u_j of the overflow from class A, which is ubar_j ≥ 2^(j−1) + 1 (F3, F1), and the digit is touched at most 2^(j−1) − 1 times before the top falls, so it never runs out. A collision removes one digit, i.e. two exponents. - First group never 0: true at cycle starts, where u_j − 1 ≥ 2^j − 1 and a ≥ 2^(m+1) − 1 (class C at all bits 1). Mid-cycle the j-th one falls by 2^j, to v_j − 2 at the overflow from class A; there INV proves only the weaker bound ≥ −1 (vbar_j ≥ 1). - Second group even: true for each v_j − 2 (v_j + 1 is odd); the X^n R exponent b + 2 is odd at every left-end visit (b odd), as he guessed.

C C0 at the right end: no. C C0 < is D reading the last 1 of a 1001 with a nonzero cell further left. It does not occur in the first 732 steps; after them D reads 1 only in T4, T9 (L0 <) and T13 (X C0 <), and T4 meets a 1001 only where Lb starts on a digit (u,1,1). So C C0 < is Lb on a bit-1 digit with v = 1 (his <D 0111). The right end is the LSB digit and the block (10)^a 000 (10)^b; the block holds no digit, and INV excludes the LSB. A carry sweeps only digits with v ≥ R + 1 ≥ 3 (class A, F0) or v even (B, C); an overflow from class C has all v even; an overflow from class A has v_m = vbar_m, which is ≥ 1 and even, so v_m ≥ 2: class A starts at the base (vbar = 10) or after an overflow from class C, where F3 gives the new LSB vbar = a − 2^(m+1) + 2 with a even (a + R_tot even, R_tot = 0), and class A keeps it. INV leaves open only a digit (u,1,1) above the LSB at an overflow from class A, which needs u_j = 2^j at the overflow from class C before it (v_j = u_j − 2^j + 1).

Checks (direct simulation to step 10⁹): the 14 rules (in random contexts), both readings (19,332 K-configurations, 53 overflows), the rule-only run (38,672 > R moments), the cycle (132 left-end visits) and the table all hold, and no C C0 < occurs. For the table, the tracked exponents are the 289 X^n C exponents at the starts of the 25 complete cycles after step 732: the 242 not involved in a collision follow his table exactly (each by its place at the start of the cycle), and the 47 caught in a collision follow his collision rule. On the abstract orbit (1.2·10⁶ macro steps), class B never drops below the top, and every v swept at an overflow from class A is ≥ 4.

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