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 / #1

`1RB0LC_1LA0RE_0RD1LF_1LC1LB_0LD0RB_0LA---`

#1Claimed elsewhereStructural counter + counterbbchallenge ↗Explorer

Upstream result

Claimed elsewhere

The blank-start machine never halts: BLECv4.v.TM2 ↗. Recorded commit time: 2026-10-15T06:57:40Z. First public push time is not established.

Absent from the current 663 holdout list. Earlier local observations remain below.

Overview

In one sentence

Period-5 tape; a binary counter of drifting 3-cell digits feeds a left-edge bit counter that absorbs them

Upstream: The blank-start machine never halts: BLECv4.v.TM2 ↗. Recorded commit time: 2026-10-15T06:57:40Z. First public push time is not established.
Status: Externally Solvedinformal proof · updated 2026-10-10Parked · Stopped by Dennis 2026-10-10: cryptid candidate; Rocq rule reduction later, low priority. The 2 open questions are optional.
idle since Oct 10 12:49 · status.json 2026-10-10
Informal proof: proof.mdconditional; see Proof for what is still open
Class: Structural counter + counterours: sheet Structural counter + counter ≠ ours Two coupled binary counters: drifting-defect digit counter (right) + edge bit counter (left) · med confidence
On the list: not on BB6_holdouts_663.txt (line 79 of the previous list) · historical 740 line 79
#1eqv ×1sim 1e15

Your calls on file 3

parked: Stopped by Dennis 2026-10-10: cryptid candidate; Rocq rule reduction later, low priority.
next: Dennis: stop (keep as cryptid-like, write an AntiHydra-style rule reduction) or continue (search for X: a quantitative u-vs-Delta invariant plus a leading-marker episode analysis; see proof.md 3.4 and 5.1).
decision.json · answered 2026-10-10: stop: Stop proof work on #1 and file it as a cryptid candidate (rules written out, Rocq rule reduction later), or spend another stage searching for the missing invariant clause X? Decisions →

Mechanism

How it works: 3 notes

Period-5 tape 10110. Right counter: little-endian digits 110=1 / 100=0 in the stripes; each sweep adds 1 with carry.
A carried digit moves 5 cells left (digit k drifts 1 block per 2^k sweeps); overflow adds two 0-digits at the right end.
Left counter: big-endian bits 10=1 / 00=0, +1 per 2 sweeps; absorbing the lowest digit halves it (phases X/Y follow).

Figures for Checkpoint A

Fig 1 · Hub map: one row per right sweepQ1 Q2
Each row is the tape at the start of a right sweep. Follow one orange/blue track down the rows.

Fig 2 · Same rows as Fig 1, plain coloursQ1
The same rows and window as Fig 1, nothing recoloured: compare its small stripe breaks with Fig 1's tracks.

Checkpoint A · 2 open

check: does the figure show what I claim? A “no” stops proof work built on a wrong reading. decision: your call.

Q1
check Fig 1 do the orange/blue tracks read as one binary counter whose digits drift left and are absorbed by the left counter? Fig 2 is the same rows, uncoloured.
Q2
check Fig 1 in the left band, do the bits change every few rows, like a second counter rather than a fixed wall?

Discord message 1 · draft, not posted

Structural counter + counter, Counter Class 4 · ready to paste · source

Is anyone working on any of these Structural counter + counter / Counter Class 4 holdouts, or has anyone tried them and got stuck? We found no sheet notes, threads or claims, and none are on mxdys's UBRRBA list or dyuan01's longitudinal list.

1. `1RB0LC_1LA0RE_0RD1LF_1LC1LB_0LD0RB_0LA---`, `1RB0LC_1LA0RE_0RD0LA_1RE1RA_0LD1RF_0RB---`, `1RB1RC_0LA1RF_1RD0LE_1LC0RB_0RA0LC_0RD---` (identical trajectories to 1e9). Period-5 background `10110` carrying a binary counter whose digits are 3-cell defects (`110` = 1, `100` = 0). Digits drift left on carries, and a bit counter at the left edge absorbs them.
2. `1RB---_1LC1RE_1LD0LC_1LE1LC_1RF0RE_1RA0RB`. Period-5 tape cut into segments by phase-shift walls. Each wall moves 3/2 times as often as the one to its left, so segment lengths run 12, 18, 27, 41, 61, 92, 138, 206 blocks.
3. `1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF` and its twin `1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB`. Run-length counter whose epochs double in length. Each epoch starts at `0^inf <A 0 1^3 0^2 1^2 0^2 1^(2k) 0^2 1^(2k+1) 0^P 1 0^Q 1 0^inf` with P+Q = 2k and P irregular. No halt in 1e11 steps; in a macro simulation every even P closes the epoch for k <= 13.

What we checked: direct simulation (1e9 steps for groups 1 and 2, 1e11 for group 3), plus the local rules above on random instances. No proofs yet. If nobody has them, we'll write Rocq proofs, starting with group 1.

More figures (3)Fig 3–5: Left/right records to 100M steps · Blaze, 100M steps · bbchallenge default view, first 10,000 steps

Fig 5 · bbchallenge default view, first 10,000 stepsviewer ↗
The site's view: a narrow bell growing from the blank tape.

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

rule	from ⟶ to	cases	steps	checked
R1 E-chain	E> (10110)ⁿ ⟶ (11010)ⁿ E>	—	17n	✓40/40
R2 F-chain	(11010)ⁿ <F ⟶ <F (10110)ⁿ	n>=1	9n	✓40/40
R3 set (no carry)	E> (10110)^a 100 ⟶ <F (10110)^a 110	a>=0	26a+7	✓35/35
R4 carry through j ones	E> (10110)^a [110 (10110)^b_i]_{i=1..j} 100 ⟶ <F (10110)^a-1 [100 (10110)^b_i]_{i<j} 100 (10110)^b_j+1 110	j>=1, a>=1, b_i>=0 (carried digits shift one block left)	26(a+sum b_i)+16j+7	✓125/125
R5 right overflow	E> (10110)^a [110 (10110)^b_i]_{i=1..j} 11 0^∞ ⟶ <F (10110)^a-1 [100 (10110)^b_i]_{i=1..j} 100 100 11 0^∞	j>=0, a>=1 (all digits 1: reset + two new 0-digits)	26(a+sum b_i)+16j+13	✓80/80
R6 hub macro (X and Y)	0^∞ 10 W σ E> 110 (10110)^g R ⟶ 0^∞ 10 (W+1) σ E> 110 inc(inc((10110)^g R))	g>=2; inc = R3/R4/R5 (g drops by 1); W+1 widens by one bit on overflow, left edge -2	—	✓160/160
R7 absorption, phase X	0^∞ 10 W w 101010 E> 110 (10110)¹ D_1 (10110)^G_1 R' ⟶ phase X if D_1=110 else Y; left bits W+1+w(1-d); right = inc^(2+(d xor w)) of (10110)^G_1+2 R'	4 cases (d,w) in {0,1}^2, 30/30 each; w = low bit of W, d = 1 iff D_1=110	—	✓120/120
R8 hub macro, separator regime	0^∞ 10 W1 s W2 σ E> 110 (10110)^g R ⟶ 0^∞ 10 W1 s (W2+1) σ E> 110 inc(inc((10110)^g R))	s in {0, 110}; W2 non-empty and not all ones; both σ (entry/exit of this regime still open)	—	✓96/96

Compressed historythe tape as 0^∞ 10 W σ E> 110 (10110)^g D_1 (10110)^G_1 ... D_k (10110)^G_k 11 0^∞ (σ = 101010 for X, 100010 for Y) at 31 moments: where the rules are read off

0^∞ 10 W σ E> 110 (10110)^g D_1 (10110)^G_1 ... D_k (10110)^G_k 11 0^∞ (σ = 101010 for X, 100010 for Y)

step	`phase (X/Y)`	`W left bits MSB-first (10=1, 00=0)`	`g`	`D digits LSB-first (110=1, 100=0)`	`G gaps after each digit`	`lo`	`hi`
3,304	Y	0	1	100	2 0 0 0	-32	10
6,050	Y	0	1	10,000	2 1 0 0 0	-40	12
10,278	X	1	4	111	2 1 0	-46	13
15,768	X	1	4	110	3 1 0 0	-54	15
30,190	X	0	5	101	4 1 1 0	-66	18
39,622	X	1	7	100	3 2 0 0 0	-72	20
60,156	Y	110	1	101	7 4 1 1 0	-82	22
112,236	Y	10	10	110	5 3 1 0 0	-100	27
150,658	Y	1	1	100,000	11 5 2 1 0 0 0	-112	30
251,402	X	10	7	0	10 5 2 1 0 0 0	-132	35
386,450	Y	1,110	1	10,101	16 7 4 1 1 0	-150	39
631,060	Y	101	12	11,000	13 7 3 1 0 0 0	-176	46
1,023,498	X	111	22	1,110	12 6 3 1 0 0	-204	53
1,564,836	Y	1,111	1	101,000	26 13 6 3 1 0 0 0	-236	61
2,556,812	Y	111	31	1,100	16 8 4 2 0 0 0	-276	71
3,963,894	Y	11,110	1	1,011	36 18 9 4 2 1 0	-318	81
6,310,650	X	1,001	12	1,011,011	37 19 9 4 2 1 0	-372	94
8,307,182	X	100	48	1,110,110	24 12 5 3 1 0 0	-406	103
8,310,866	X	101	47	1,001,110	24 12 6 3 1 0 0	-406	103
8,314,032	X	110	46	1,101,110	25 12 6 3 1 0 0	-406	103
8,317,492	X	111	45	1,011,110	25 13 6 3 1 0 0	-406	103
8,320,596	X	1,000	44	1,111,110	26 13 6 3 1 0 0	-406	103
8,427,418	X	10,001	3	100,010,000	46 23 11 6 2 1 0 0 0	-408	104
8,428,868	X	10,010	2	110,010,000	47 23 11 6 2 1 0 0 0	-408	104
8,430,898	X	10,011	1	101,010,000	47 24 11 6 2 1 0 0 0	-408	104
8,437,790	X	1,011	47	1,110,000	25 12 6 2 1 0 0 0	-408	104
8,441,584	X	1,100	46	1,000	25 12 6 3 1 0 0 0	-408	104
9,999,794	Y	1,001	24	100,111	39 19 9 5 2 1 0	-432	109
15,848,708	Y	1,110	39	10,110,010	40 20 10 4 2 1 0 0	-502	127
25,116,996	Y	110,111	2	1,111,101	69 34 17 8 4 1 1 0	-582	147
39,809,272	X	10,001	68	1,010,110	48 23 12 5 3 1 0 0	-678	171

phase (X/Y)last X

not plottable

W left bits MSB-first (10=1, 00=0)last 10,001

glast 68

D digits LSB-first (110=1, 100=0)last 1,010,110

G gaps after each digitlast 48 23 12 5 3 1 0 0

not plottable

lolast -678

hilast 171

Template comparisonCounterCmp_v1.v TM1: does not apply · the nearest solved proof, what carries over, and the transitions that differ

	0	1
A	1RB	0LC
B	1LA	0RE
C	0RD	1LF
D	1LC	1LB
E	0LD	0RB
F	0LA	---

differs from the template

file: CounterCmp_v1.v:9
module: TM1
machine: 1RB0LD_1RC0RE_0LA0RC_1LB1LD_0LF1RE_---1LA (10 transitions apart)
diff: 10 of 12 transitions differ (A1 B0 C0 C1 D0 D1 E0 E1 F0 F1); CounterClass1 TM1: 9; BECv7 TMs: 11-12
note: Different mechanism (unary blocks at the 0^inf edge); its S1/Inc1 shape fails 0/5 here (3 halt). Only BECv7's digit-list layout (Inductive RD + bin_inc) carries over.

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

Encode the hub as (phase, W, separator, W2, g, digit list with gaps) using BECv7-style Inductive lists. Prove R1-R5 with es/ind, R6-R8 and absorption with follow/mid, init to the first hub, then nonhalt via multistep_nonhalt + progress_nonhalt_cond on a well-formed-hub invariant. Missing first: Y-phase absorption and separator entry/exit rules.

▲Separator regime (left part 10 W1 0|110 W2 ..., about 40% of hubs) is entered after Y-phase absorption; its entry/exit rules are not found yet.
▲The invariant must show g>=2 after every absorption and that digit gaps never collide (a spacing lemma on G_i).
▲Likely a 30-60 KB proof; the trio is correlated, so a stall here also stalls #21 and #22.

Stats & provenance10⁹ steps simulated · 2,457 cells · the status in full · files

simulated: 10⁹ steps
tape: 2,457 cells · 1,464 nonzeros
growth: ~t^0.33 (span 1148 at 1e8, 2457 at 1e9; lo -1964, hi 492)
status now: Stopped by Dennis 2026-10-10: cryptid candidate; Rocq rule reduction later, low priority. Fatal gap open: the absorption-safety lemma (old O2, now the configuration predicate Safe(w, 2g-1-d_1), proof.md 3.3) is not inductive, and no strengthening X is known. Safety depends on the left counter u avoiding a sparse set of unsafe values (abs0 undefined at segment 1^m / 1^(m-1)0; new marker within 2 of a leading marker at the 1/4, 1/2, 3/4 points) at t=0 absorptions after a leading-O birth (ABS0 at u = 2^m - 2). The real trajectory came within 2 sweeps of halting: at step 86,265, Dep(O111000;1;111100;9,4,2,0,0,0); the same configuration with word O111100 halts 18,861 steps later. Later margins are 7-13% of Delta, but u/Delta at ABS0 fills the band [1.6066, 2.0006], whose top edge maps onto the 3/4 unsafe point, so no band argument closes it. Cryptid protocol triggered (proof.md 5.3): heuristically probviously non-halting (about one birth per doubling of Delta, hit probability O(1/Delta)), but no structural reason. Needs Dennis's priority call: stop or continue. Also open (major): L and the ABS rules are checked, not derived as window-lemma chains. Closed this pass: O1 replaced by P_k (proved, 2.36M/3.05M exhaustive transitions), L precondition (right context starting 1,0; sharp), edge cases |w|=1 and '', spacing >= 3, H4 needs +2s for strips, h_1 = 161 at step 300,628,504. check_proof.py full SUMMARY PASS 36/36. (status.json, 2026-10-10)
observer's note: Mechanism found: two coupled binary counters, no Collatz-like branching. 8 rule families validated (696/696); separator-regime rules still open.
files: observe.json · notes.md · proof.md · status.json

Proof & checks

proof.md · the informal proof
check_proof.py · the numeric checks of proof.md

○ Checkpoint B: no note from Dennis found

notes.md L75: - Checkpoint questions are now yes/no questions about the figures. Moved off the card (strategy calls, not figure reading; settle them in proof.md / Checkpoint B):
proof.md L8: - AI assistance: written by Claude (Anthropic) under Dennis's direction. Checkpoint B pending, non-blocking. The review of 2026-10-10 is in §9.
proof.md L319: ## 8. Checkpoint B notes (Dennis)

Files

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

name	size	changed
notes.md ↓	17 KB	2026-10-10 12:49
proof.md ↓	31 KB	2026-10-10 07:08
status.json ↓	1.9 KB	2026-10-10 12:49
observe.json ↓	14 KB	2026-10-10 04:41
deepen.json ↓	6.9 KB	2026-10-10 04:29
decision.json ↓	4.2 KB	2026-10-10 12:49
img/	7 items	2026-10-10 01:54
scripts/	19 items	2026-10-10 06:52
check_proof.py ↓	24 KB	2026-10-10 07:03

status.json in full

{
 "tm": "1RB0LC_1LA0RE_0RD1LF_1LC1LB_0LD0RB_0LA---",
 "status": "CRYPTID_CANDIDATE",
 "stage": "informal_proof",
 "updated": "2026-10-10",
 "cryptid_flag": true,
 "reason": "Stopped by Dennis 2026-10-10: cryptid candidate; Rocq rule reduction later, low priority. Fatal gap open: the absorption-safety lemma (old O2, now the configuration predicate Safe(w, 2g-1-d_1), proof.md 3.3) is not inductive, and no strengthening X is known. Safety depends on the left counter u avoiding a sparse set of unsafe values (abs0 undefined at segment 1^m / 1^(m-1)0; new marker within 2 of a leading marker at the 1/4, 1/2, 3/4 points) at t=0 absorptions after a leading-O birth (ABS0 at u = 2^m - 2). The real trajectory came within 2 sweeps of halting: at step 86,265, Dep(O111000;1;111100;9,4,2,0,0,0); the same configuration with word O111100 halts 18,861 steps later. Later margins are 7-13% of Delta, but u/Delta at ABS0 fills the band [1.6066, 2.0006], whose top edge maps onto the 3/4 unsafe point, so no band argument closes it. Cryptid protocol triggered (proof.md 5.3): heuristically probviously non-halting (about one birth per doubling of Delta, hit probability O(1/Delta)), but no structural reason. Needs Dennis's priority call: stop or continue. Also open (major): L and the ABS rules are checked, not derived as window-lemma chains. Closed this pass: O1 replaced by P_k (proved, 2.36M/3.05M exhaustive transitions), L precondition (right context starting 1,0; sharp), edge cases |w|=1 and '', spacing >= 3, H4 needs +2s for strips, h_1 = 161 at step 300,628,504. check_proof.py full SUMMARY PASS 36/36.",
 "next": "Dennis: stop (keep as cryptid-like, write an AntiHydra-style rule reduction) or continue (search for X: a quantitative u-vs-Delta invariant plus a leading-marker episode analysis; see proof.md 3.4 and 5.1).",
 "parked": "Stopped by Dennis 2026-10-10: cryptid candidate; Rocq rule reduction later, low priority."
}

observe.json contract (tools/README-card.md):

1 contract warning

diagrams[0].style: custom; the first diagram should be a bbchallenge view unless a custom one is clearly more telling

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 1RB0LC_1LA0RE_0RD1LF_1LC1LB_0LD0RB_0LA---