Built . It shows the files as they were then (ages and “working now” follow your clock). tools/rebuild_pages.sh rebuilds the site within 5 minutes of a change; by hand: python3 -B tools/site.py.

Machines / W5-2

`1RB0RF_1RC1LB_1LD1RE_1LB0LD_1RF0RC_1RA---`

W5-2Cryptid candidateShift-overflow counterbbchallenge ↗Explorer

Where it stands

Cryptid candidate, parked at the observation

Observe done. The mechanism is understood: these are SOC_2_5_v1.v TM10's macro rules, every TM10 lemma except ROv3_0/ROv3_1 compiles for this string, and the rules were re-validated on the TM.

Read the full status

From blank every cycle is LOv, RC1_Ov_0, an R4 chain, RC4_Ov_0, giving an explicit map (L,x) -> (L',x') on the left-overflow configurations cfgL(L,0,2x+1). The run leaves this cycle only if every 1-bit of x is at an odd position. Then the chain empties and TM10's ROv3 (A reads 1) comes up, and with A1 = 0RF that can halt: the TM10-invariant configuration cfgL(8,0,17) halts at step 10,189,718, so TM10's P is not an invariant here. All 20,000 cycles computed (L to 172,193) stay normal, and the even-position 1-bits grow about 0.36 per cycle, so heuristically it never halts. But the condition is about the binary digits of an exponentially growing orbit, and no invariant is known: ground rule 6. The scout's near-port premise is wrong, because ROv3_0/ROv3_1 are false here, not just unproved.

Observe

Deepen

Informal proof

Rocq

Overview

In one sentence

TM10's two binary counters; it can halt only if a counter value x ever has every 1-bit at an odd position

Status: Cryptid candidateobserving · updated 2026-10-14Parked · Observe done. The 3 open questions are optional.
idle since Oct 14 16:43 (44 h ago) · status.json 2026-10-14
Class: Shift-overflow counterours: Shift-overflow counter (sheet) · ours adds: (SOC_2_5_v1 TM10 with A1 = 0RF); halting hinges on the bits of a counter value: cryptid-like · med confidence
On the list: line 371 of BB6_holdouts_663.txt · historical 740 line 409 · observe.json rank #409
eqv ×1sim 1e15

Your calls on file 3

priority call (answered): Cryptid-like: halting needs some cycle's x to have all 1-bits at odd positions. Park it, or fund one 2 h stage to formalize the reduction in Rocq ('no cycle empties the chain -> ~halts tm c0') and search for a digit invariant?
parked: Dennis 2026-10-14: park
2026-10-14 · park: W5-2 halts only if some cycle's x has all its 1-bits at odd positions: park it, or fund one 2 h stage?

Mechanism

How it works: 3 notes

SOC_2_5_v1.v TM10's macro rules (A1 = 0LB there, 0RF here): a left counter LC (digits 11/10) counts down, a right counter RC (digits 10000/00000) counts up, and overflows shift digits between them. Every TM10 lemma except ROv3_0/ROv3_1 compiles for this string.
From blank (cfgL(3,6,1) at step 35) every cycle is LOv at cfgL(L,0,2x+1), RC1_Ov_0, c >= 0 RC4_Ov_1, RC4_Ov_0. The chain eats x's 1-bits from the bottom and stops at the first one at an even position, which gives an explicit map (L,x) -> (L',x'). All 20,000 cycles computed (L to 172,193) are like this. The history table has one row per cycle (step column = cycle t).
If every 1-bit of x is at an odd position, the chain empties and the run leaves TM10's cycle into ROv3, where A reads 1. With 0RF that can halt (cfgL(8,0,17) halts at step 10,189,718). Even-position 1-bits grow ~0.36 per cycle (min 7 at cycle 13); chain lengths look random. No invariant is known, so ground rule 6 applies.

Figures for Checkpoint A

Fig 1 · bbchallenge default view, 10,000 steps
The site's view. Left: the slowly growing left counter. Right: the right counter's carry sweeps.

Fig 2 · Counter value x, one row per cycleQ1
Each row is x in binary, lowest bit at the right. Look for any row without orange.

Fig 3 · Where A1 = 0RF matters: a haltQ2
Row 0 is TM10's ROv3 situation. Watch the red A on a 1 head right; F (cyan) later reads 1.

More figures (2)Fig 4–5: Records to 10^10 steps · From blank: the only A1 step

Rules (10/10 validated)exact tape rewrites the proof will formalize, each re-checked by simulation

rule	from ⟶ to	cases	steps	checked
init	0^∞ A> 0^∞ ⟶ cfgL(3,6,1) = LC(3,6) <B 11 RC(1)	—	35	✓1/1
LC_Inc	LC(L,k+1) <B 11 RC(n) ⟶ LC(L,k) 10 C> RC(n)	k+1 < 2^L; LC(L,k) = 0^inf 1 + L digits of 2^L-1-k (11 = 1, 10 = 0), RC(n) = n LSB first (10000 = 1, 00000 = 0)	—	✓54/54
RC_Inc	LC(L,k) 10 C> RC(n) ⟶ LC(L,k) <B 11 RC(n+1)	—	—	✓60/60
LC_Ov	LC(L,0) <B 11 RC((2x+1)2ⁱ) ⟶ LC(L,2^L-1) 10 C> RC1(i,2ⁱ⁺¹-2,x)	n != 2^L (n = 2^L: corner case, 10/10, never reached from blank since n is odd)	—	✓83/83
RCj_Inc + LC_Inc	LC(L,k+1) 10 C> RCj(r,n+1,m) ⟶ LC(L,k) 10 C> RCj(r,n,m)	j = 1, 3, 4 (RCj = TM10's BinDec2 words with tails 10000, 0010000, 00010000)	—	✓181/181
RC1_Ov_0	LC(L,k) 10 C> RC1(2r,0,m) ⟶ LC(L+1+5r,(2k+1)2^5r-1) 10 C> RC4(i,2ⁱ⁺¹-2,m') if m = (2m'+1)2ⁱ, else C> RC(1)	m > 0 (47/47) and m = 0 (29/29); odd lenR: RC1_Ov_1/_1_0 77/77 (only after an exhaustion)	—	✓76/76
RC4_Ov_0	LC(L,k) 10 C> RC4(2r,0,m) ⟶ LC(L+2+5r,(2k+1)2^5r+1-1) 10 C> RC(2m+1)	ends every cycle	—	✓70/70
RC4_Ov_1	LC(L,k) 10 C> RC4(2r+1,0,m) ⟶ LC(L+5+5r,(2k+1)2^5r+4-1) 10 C> RC4(i,2ⁱ⁺¹-1,m') if m = (2m'+1)2ⁱ; m = 0: C> RC(0) (RC4_Ov_1_0 = exhaustion)	m > 0 (46/46), m = 0 (33/33)	—	✓79/79
cycle map F	cfgL(L,0,2x+1) ⟶ cfgL(L',0,2x'+1), x' = (2k_c+1)2^5q + (x >> s)	x has a 1-bit at an even position; the chain stops there (q = half its gap, s = bits consumed, k_c from the chain). Checked on the real TM at the next left record: chain length 0 (28), 1 (19), 2 (3), L' <= 21; F = macro-rule simulator on 783 orbit cycles	—	✓50/50
RC3 overflow, A1 = 0RF	LC(L,k) 10 C> RC3(2r,0,2m+1) ⟶ halt	TM10's ROv3_0 needs A1 = 0LB. Here A reads the 1 of the 1 00 10000 tail and moves right; with m odd, F later reads a 1. Other RC3 cases: 13 halts, 56 no TM10 result in 2e5 steps	30r+30 (r = 0: 30)	✓16/16

Compressed historythe tape as 0^∞ <B 1^2L+3 RC(2x+1) 0^∞ at 35 moments: where the rules are read off

0^∞ <B 1^2L+3 RC(2x+1) 0^∞

step	`L`	`1-bits of x`	`E (1-bits at even positions)`
1	3	2	1
2	6	4	2
3	14	6	3
4	37	25	11
5	40	23	13
6	48	19	8
8	84	21	10
10	95	23	11
13	124	18	7
16	163	39	19
20	190	37	15
25	235	30	18
30	265	29	15
40	345	31	17
50	435	69	31
75	650	92	51
100	815	82	46
150	1,215	133	65
200	1,640	172	95
300	2,355	240	140
400	3,190	305	167
500	4,010	378	202
750	6,015	554	284
1,000	8,245	749	394
1,500	12,405	1,080	551
2,000	16,920	1,432	705
3,000	25,530	2,197	1,084
4,000	33,625	2,886	1,417
5,000	42,020	3,601	1,769
7,500	63,420	5,483	2,791
10,000	85,235	7,355	3,725
12,500	106,850	9,032	4,638
15,000	129,520	10,788	5,523
17,500	150,875	12,599	6,415
20,000	172,160	14,392	7,299

Llast 172,160

1-bits of xlast 14,392

E (1-bits at even positions)last 7,299

Template comparisonSOC_2_5_v1.v TM10: partly applies · the nearest solved proof, what carries over, and the transitions that differ

	0	1
A	1RB	0RFtpl 0LB
B	1RC	1LB
C	1LD	1RE
D	1LB	0LD
E	1RF	0RC
F	1RA	---

differs from the template

file: SOC_2_5_v1.v:5186
module: TM10
machine: 1RB0LB_1RC1LB_1LD1RE_1LB0LD_1RF0RC_1RA--- (1 transition apart)
diff: A1: 0LB -> 0RF
note: Every TM10 lemma except ROv3_0/ROv3_1 compiles with this string (the scout's Iter.v, which admits those two). They are false here, not just unproved: TM10's invariant P contains halting configurations of this machine (cfgL(8,0,17) halts at step 10,189,718). A proof needs P plus an orbit-specific digit condition (the chain never empties), and that condition is the open part. No other upstream file proves this table from any start.

Proof strategy & riskshow the formal proof will go · 3 risks to watch

No non-halting proof is known. Rule 6: formalize the reduction (Rocq: 'no cycle empties the chain -> ~halts tm c0', from TM10's lemmas and F), then park unless a digit invariant turns up.

▲Non-halting depends on the binary digits of an exponentially growing orbit (all 1-bits at odd positions must never happen): cryptid-like.
▲The scout's Iter.v 'nonhalt' admits ROv3_0/ROv3_1, which are false for this machine; it is not evidence.
▲After an exhaustion the dynamics are unmodelled; halting is shown only from constructed starts, not from blank.

Stats & provenance3·10¹⁰ steps simulated · 228 cells · the status in full · files

simulated: 3·10¹⁰ steps
tape: 228 cells · 70 nonzeros
growth: exponential (two binary counters); A reads 1 only at step 10 through 3e10 steps; abstract orbit checked for 20,000 cycles (L to 172,193)
status now: Observe done. The mechanism is understood: these are SOC_2_5_v1.v TM10's macro rules, every TM10 lemma except ROv3_0/ROv3_1 compiles for this string, and the rules were re-validated on the TM. From blank every cycle is LOv, RC1_Ov_0, an R4 chain, RC4_Ov_0, giving an explicit map (L,x) -> (L',x') on the left-overflow configurations cfgL(L,0,2x+1). The run leaves this cycle only if every 1-bit of x is at an odd position. Then the chain empties and TM10's ROv3 (A reads 1) comes up, and with A1 = 0RF that can halt: the TM10-invariant configuration cfgL(8,0,17) halts at step 10,189,718, so TM10's P is not an invariant here. All 20,000 cycles computed (L to 172,193) stay normal, and the even-position 1-bits grow about 0.36 per cycle, so heuristically it never halts. But the condition is about the binary digits of an exponentially growing orbit, and no invariant is known: ground rule 6. The scout's near-port premise is wrong, because ROv3_0/ROv3_1 are false here, not just unproved. (status.json, 2026-10-14)
observer's note: Mechanism understood (TM10's macro rules, validated); non-halting needs the orbit of an explicit digit map never to put every 1-bit of x at an odd position. Heuristically never; no invariant known.
files: observe.json · notes.md · status.json

Proof & checks

No proof work yet.

Files

machines/<tm>/: 7 entries · raw notes, status, scripts, images

name	size	changed
notes.md ↓	8.7 KB	2026-10-13 01:45
status.json ↓	2.2 KB	2026-10-14 16:43
observe.json ↓	13 KB	2026-10-13 01:45
data/	5 items	2026-10-13 01:45
decisions/	1 item	2026-10-14 16:43
img/	5 items	2026-10-13 01:39
scripts/	10 items	2026-10-13 01:44

status.json in full

{
 "tm": "1RB0RF_1RC1LB_1LD1RE_1LB0LD_1RF0RC_1RA---",
 "label": "W5-2",
 "status": "CRYPTID_CANDIDATE",
 "stage": "observe",
 "updated": "2026-10-14",
 "confidence": "med",
 "reason": "Observe done. The mechanism is understood: these are SOC_2_5_v1.v TM10's macro rules, every TM10 lemma except ROv3_0/ROv3_1 compiles for this string, and the rules were re-validated on the TM. From blank every cycle is LOv, RC1_Ov_0, an R4 chain, RC4_Ov_0, giving an explicit map (L,x) -> (L',x') on the left-overflow configurations cfgL(L,0,2x+1). The run leaves this cycle only if every 1-bit of x is at an odd position. Then the chain empties and TM10's ROv3 (A reads 1) comes up, and with A1 = 0RF that can halt: the TM10-invariant configuration cfgL(8,0,17) halts at step 10,189,718, so TM10's P is not an invariant here. All 20,000 cycles computed (L to 172,193) stay normal, and the even-position 1-bits grow about 0.36 per cycle, so heuristically it never halts. But the condition is about the binary digits of an exponentially growing orbit, and no invariant is known: ground rule 6. The scout's near-port premise is wrong, because ROv3_0/ROv3_1 are false here, not just unproved.",
 "siblings": [],
 "sibling_note": "No other start or mirror of this table is on the 740 or 778 lists (starts B..F checked by canon), and it is a singleton in the 1590 equivalence file. Upstream proves A1-variants of the table (SOC_2_5_v1.v TM8/9/10/11/12/14/15/18/19, A1 in {1RD,1LB,0LB,1LE,0RE,1LA,0LE,1LC,0RC}), but none with A1 = 0RF.",
 "holdout_line_740": 409,
 "holdout_line_778": 436,
 "upstream": "Nearest proof: SOC_2_5_v1.v Module TM10 (1RB0LB_..., A1 = 0LB), a hand proof with cfgL/cfgR/cfgR1/cfgR3/cfgR4 and invariant P. Both orbits avoid R3 in 20,000 macro events, but TM10's proof covers R3 because TM10's ROv3 lemmas hold there. No claim in data/discord or data/sheet (sheet: Shift-overflow counter, no status).",
 "priority_call_answered": "Cryptid-like: halting needs some cycle's x to have all 1-bits at odd positions. Park it, or fund one 2 h stage to formalize the reduction in Rocq ('no cycle empties the chain -> ~halts tm c0') and search for a digit invariant?",
 "parked": "Dennis 2026-10-14: park"
}

Rendered 2026-10-16 13:29 by tools/machinepage.py from status.json, observe.json (the card) and the dashboard records · rebuild: python3 -B tools/card.py 1RB0RF_1RC1LB_1LD1RE_1LB0LD_1RF0RC_1RA---