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 / W7-4

`1RB0LD_1RC0RF_0LD0LE_1RF1LC_0LB1LE_0RA---`

W7-4Checkpoint ASkelet 1-like Class 1bbchallenge ↗Explorer

Where it stands

In progress: observation

Observe at table level done. The machine is an exact base-4 counter: W = 100 sea, digits D(m,p) = X(10)^mY (m even, phase = 2 bits at the region's ends), one sweep = one increment with shifts at 1->2 and 3->0, +1 W at the right end per sweep (R1/R2 700/700, exact step formula R3).

Read the full status

A mod-3 field invariant J keeps every merge clean (1,456/1,456 real fields, 1,986/1,986 glued sweeps). Overflows alternate the wall [10100][] and give births at the right end (300/300); the wall then eats the top digit through a finite remnant family (80/80 small cases return clean, none halts). The three starts enter the same language by step 20,600 and differ only in the far-left field. Exact sweep simulator = C core at 1e11 on all three (configuration and step count); no halt to 1e14 on 82, 464, 722 (82 to 1e15). Not a cryptid. Stage-1 GO signal; open: complete wall case table + closure check.

Observe

Deepen

Informal proof

Rocq

Overview

In one sentence

Exact base-4 counter: digits are 10-regions in a 100 sea; a mod-3 field law keeps merges clean; no halt to 1e15.

Status: Checkpoint Aobserving · updated 2026-10-14Not blocking · Next: proof.md. Answer Q1–Q3 whenever; a “no” redirects the work.
idle since Oct 14 20:36 (40 h ago) · status.json 2026-10-14
Class: Skelet 1-like Class 1ours: sheet Skelet 1-like Class 1 ≠ ours Base-4 counter on 10-regions in a 100 sea; overflow eats the left wall and spawns a digit at the right · high confidence
On the list: line 76 of BB6_holdouts_663.txt · historical 740 line 82 · observe.json rank #82
eqv ×1table ×3sim 1e15

Mechanism

How it works: 3 notes

Tape at every C-record: 0^inf <wall> W^a D W^f ... D W^c 11 C> 0^inf, with W = 100 and digits D(m,p) = X (10)^m Y (m even, X in {10,11}, Y in {10,00}, phase p = 2x+y). One sweep adds 1 to this base-4 counter from the right; phases 1->2 and 3->0 shift the digit one W left; the right field gains 1 W.
Every interior field keeps J = f + 2pL + floor(pR/2) - floor(pL/2) = 0 (mod 3), so a dying field always merges its two digits into one D(m+m'+2) and never goes negative. Digits are born at the right end on overflows and merge as they drift left: 10 digits at 1e14.
Overflow: [10100] W^a -> [] W^a and [] W^a -> [10100] W^(a-2) (+ a birth). When the far-left field runs out, the wall eats the top digit through a finite remnant family. The three starts enter the same language by step 20,600, differing only in the far-left field; an exact sweep simulator matches the C core at 1e11 on all three and reaches 1e14 with no halt (82: 1e15).

Figures for Checkpoint A

Fig 1 · Four counter sweeps, one carryQ1
Rows are steps. Count the trips from the right edge; compare how far left each one turns.

Fig 2 · Digit worldlines from blank to 3e9Q2
Each white line is one digit. Follow lines from the right edge leftward; watch where two lines meet.

Fig 3 · Left wall eating the top digitQ3
Watch the dense 1010 block at the far left shrink while the 8-cell digit to its right drifts left.

Checkpoint A · 3 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 you see four trips from the right edge, with the second one turning much further left than the others (it carries into the 8-cell digit)?
Q2
check Fig 2 do new white lines start at the right edge, drift left and slow down, and sometimes meet and continue as one line?
Q3
check Fig 3 does the dense block at the far left get shorter in steps while everything to its right keeps its stripes?

Discord message · draft, not posted

ready to paste

Is anyone working on 1RB0LD_1RC0RF_0LD0LE_1RF1LC_0LB1LE_0RA--- (Skelet 1-like Class 1)? Its other starts 1RB0RD_0LC0LF_1RD1LB_0RE---_1RA0LC_0LA1LF and 1RB1LE_0RC---_1RD0LA_1RE0RB_0LA0LF_0LD1LF are on the list too. It looks like a clean base-4 counter: digits are 10-regions in a 100 background, an overflow eats the left wall and spawns a new digit on the right, no glider in sight to 1e14. We'd like to try a closed-invariant proof for all three unless someone already has one.

More figures (1)Fig 4: Default view, first 10,000 steps

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

rule	from ⟶ to	cases	steps	checked
R1 increment (p = 0, 1, 2)	L W^a D(m,p) W^c 11 C> 0^∞ ⟶ L W^(a-s) D(m,p+1) W^(c+1+s) 11 C> 0^∞, s = 1 if p = 1 else 0	m even; a >= s	8c+11 (p = 0, 2); 8c+5m+23 (p = 1)	✓700/700
R2 carry (p = 3)	L W^a D(m',q) W^f D(m,3) W^c 11 C> 0^∞ ⟶ R1 applied to D(m',q) with W^f as its right field, D(m,3) -> D(m,0) shifted 1 W left; right field c+2	repeats leftward through every digit at phase 3	8(c+f) + (5m+12) + stop(q, m'), stop = 11 or 5m'+23	✓700/700
J invariant and merges	interior field W^f between D(.,pL) and D(.,pR) with f + 2pL + floor(pR/2) - floor(pL/2) = 0 (mod 3) ⟶ J stays 0 under R1/R2; a field reaching 0 is followed by D(m,2x+0)D(m',0+y) = D(m+m'+2, 2x+y), never by a negative field	fields 0..18, glued digits, all phases	—	✓1986/1986
O1/O2 overflow	0^∞ [10100 \| empty] W^a (all digits at phase 3) W^c 11 C> 0^∞ ⟶ [10100] W^a -> [] W^a, right W^(c+2); [] W^a -> [10100] W^(a-2), right W^(c+1) D(0,0) (birth) or W^(c+3)	a >= 4; every digit shifts 1 W left; birth or no birth both stay in the language	—	✓300/300
Wall eats the top digit	[] W^1 D(m,0) ..., [] W^2 ..., [] W^3 ..., [10100] W^0..3 ... ⟶ remnant chain 11(10)^k{10,00} -> 1(10)^k{10,00} -> (10)^k{10,00} -> ... -> 110100 -> [] W^f (next field)	80 small-field families (wall x a in 0..4 x m in 0..6 x 2 field sizes): all return to a clean wall, none halts	—	✓80/80

Compressed historythe tape as overflow outputs: 0^∞ <wall> W^a D ... D W^c 11 C> 0^∞ (82, exact sweep-level simulator) at 25 moments: where the rules are read off

overflow outputs: 0^∞ <wall> W^a D ... D W^c 11 C> 0^∞ (82, exact sweep-level simulator)

step	`wall`	`a (far-left field)`	`digits`	`top digits`	`right end`
25,780	[1110]	3	1	D0.0	W^85
59,542	[]	85	2	D0.0 D0.0	W^73
155,923	[]	73	3	D2.0 D0.0 D0.0	W^96
375,678	[]	69	3	D2.0 D0.0 D0.0	W^289
927,748	[]	61	3	D2.0 D2.0 D0.0	W^289
3,105,598	[10100]	54	4	D2.0 D2.0 D0.0 D0.0	W^769
8,007,849	[10100]	50	3	D6.0 D2.0 D0.0	D0.0
18,063,033	[]	33	4	D6.0 D2.0 D2.0 D0.0	W^384
57,930,182	[10100]	22	5	D6.0 D2.0 D2.0 D0.0 ...	W^3073
136,320,257	[10100]	18	5	D6.0 D2.0 D2.0 D2.0 ...	D0.0
437,187,099	[]	9	6	D6.0 D2.0 D2.0 D2.0 ...	W^6144
1,309,352,950	[]	5	6	D6.0 D2.0 D2.0 D2.0 ...	W^18433
2,882,170,778	[1101010]	24	6	D2.0 D6.0 D2.0 D0.0 ...	W^12289
6,675,937,712	[]	9	6	D2.0 D6.0 D2.0 D4.0 ...	W^18433
15,392,730,394	[10100]	2	7	D2.0 D6.0 D2.0 D4.0 ...	W^49153
35,297,299,805	[1101010]	780	6	D6.0 D2.0 D4.0 D0.0 ...	D0.0
75,936,579,781	[10100]	758	7	D6.0 D2.0 D4.0 D4.0 ...	D0.0
187,647,088,069	[]	741	8	D6.0 D2.0 D4.0 D4.0 ...	W^98304
412,334,439,524	[]	737	8	D6.0 D2.0 D4.0 D4.0 ...	W^294913
975,100,850,146	[]	729	8	D6.0 D2.0 D4.0 D4.0 ...	W^294913
3.22·10¹²	[10100]	722	9	D6.0 D2.0 D4.0 D4.0 ...	W^786433
8.34·10¹²	[10100]	718	8	D6.0 D2.0 D4.0 D4.0 ...	D0.0
1.87·10¹³	[]	701	9	D6.0 D2.0 D4.0 D4.0 ...	W^393216
6.03·10¹³	[10100]	690	10	D6.0 D2.0 D4.0 D4.0 ...	W^3145729
9.52·10¹³	[]	689	10	D6.0 D2.0 D4.0 D4.0 ...	W^4718593

walllast []

not plottable

a (far-left field)last 689

digitslast 10

top digitslast D6.0 D2.0 D4.0 D4.0 ...

not plottable

right endlast W^4718593

not plottable

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

	0	1
A	1RB	0LD
B	1RC	0RF
C	0LD	0LE
D	1RF	1LC
E	0LB	1LE
F	0RA	---

file: Sk1Machines.v:8
module: Sk1Counter / Sk1CounterMixed + TM17
machine: 1LB1LE_1RC1LB_1LA0RD_1LC0RB_0LF---_0RD1LA (11 transitions apart)
diff: different table; same architecture (digits with take/give/carry over a periodic word W, segRLs wall and one-digit lemmas)
note: mxdys's Sk1Counter matches our sweep rules (one digit step = segRLs with take/give/carry; W traversal = wall lemma). Its endgame does not: TM17 runs an accelerated simulation until a glider (translated cycle); ours grows forever (fields 3*2^k, 10 digits at 1e14), so the endgame must be a closed invariant (as in our #30), not a glider check.

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

Finish stage 1: write the wall/remnant case table as affine rules and run an exhaustive closure check of the candidate language L (J-valid fields, even digits, wall grammar). Then proof.md: one closed-language argument for L plus three entry lemmas (82, 464, 722).

▲The wall grammar is only seen to 1e14: the remnant prefixes (11, 1, empty, 10100, 1011) and collision chains need a complete, proved table.
▲Formal size: the Sk1Counter-style lemmas exist upstream, but the closed-set argument over arbitrary digit lists is new work (#30 was 1,726 lines).
▲Owner risk: the class is mxdys's (Sk1Machines.v); ask in #bb6 before stage 2.

Stats & provenance10¹⁵ steps simulated · 896,775 cells · the status in full · files

simulated: 10¹⁵ steps
tape: 896,775 cells · 298,934 nonzeros
growth: direct C core: span 67k at 1e9, 897k at 1e11 (82); exact sweep-level simulator: no halt to 1e14 on 82, 464 and 722, and to 1e15 on 82 (11 digits, right field 1.5e7 W)
status now: Observe at table level done. The machine is an exact base-4 counter: W = 100 sea, digits D(m,p) = X(10)^mY (m even, phase = 2 bits at the region's ends), one sweep = one increment with shifts at 1->2 and 3->0, +1 W at the right end per sweep (R1/R2 700/700, exact step formula R3). A mod-3 field invariant J keeps every merge clean (1,456/1,456 real fields, 1,986/1,986 glued sweeps). Overflows alternate the wall [10100]<->[] and give births at the right end (300/300); the wall then eats the top digit through a finite remnant family (80/80 small cases return clean, none halts). The three starts enter the same language by step 20,600 and differ only in the far-left field. Exact sweep simulator = C core at 1e11 on all three (configuration and step count); no halt to 1e14 on 82, 464, 722 (82 to 1e15). Not a cryptid. Stage-1 GO signal; open: complete wall case table + closure check. (status.json, 2026-10-14)
observer's note: Stage-1 go signal: the interior counter is exact and closed (R1/R2, J mod 3, clean merges); overflow and wall rules are finite and affine as far as seen; no halt to 1e14 on any start. Remaining: complete the wall/remnant case table and check closure.
files: observe.json · notes.md · status.json

Proof & checks

No proof work yet.

Files

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

name	size	changed
notes.md ↓	9.1 KB	2026-10-14 20:36
status.json ↓	1.9 KB	2026-10-14 20:36
observe.json ↓	12 KB	2026-10-14 20:36
img/	4 items	2026-10-14 20:33
scripts/	17 items	2026-10-14 20:33
work/	23 items	2026-10-14 20:32

status.json in full

{
 "tm": "1RB0LD_1RC0RF_0LD0LE_1RF1LC_0LB1LE_0RA---",
 "label": "W7-4",
 "status": "CHECKPOINT_A",
 "stage": "observe",
 "updated": "2026-10-14",
 "confidence": "high",
 "holdout_line_740": 82,
 "reason": "Observe at table level done. The machine is an exact base-4 counter: W = 100 sea, digits D(m,p) = X(10)^mY (m even, phase = 2 bits at the region's ends), one sweep = one increment with shifts at 1->2 and 3->0, +1 W at the right end per sweep (R1/R2 700/700, exact step formula R3). A mod-3 field invariant J keeps every merge clean (1,456/1,456 real fields, 1,986/1,986 glued sweeps). Overflows alternate the wall [10100]<->[] and give births at the right end (300/300); the wall then eats the top digit through a finite remnant family (80/80 small cases return clean, none halts). The three starts enter the same language by step 20,600 and differ only in the far-left field. Exact sweep simulator = C core at 1e11 on all three (configuration and step count); no halt to 1e14 on 82, 464, 722 (82 to 1e15). Not a cryptid. Stage-1 GO signal; open: complete wall case table + closure check.",
 "siblings": [
  "1RB0RD_0LC0LF_1RD1LB_0RE---_1RA0LC_0LA1LF",
  "1RB1LE_0RC---_1RD0LA_1RE0RB_0LA0LF_0LD1LF"
 ],
 "sibling_note": "Same table from B (464) and D (722); starts C, E, F reduce to D, B, A after one step. Same counter and invariant; only the far-left field differs at entry (82: [] W^1, 464: [10100] W^9, 722: [10100] W^11), so one closed-language proof plus three entry lemmas covers all three lines.",
 "upstream": "No upstream proof of any start (solved_index: no; Astra equivalence sweeps negative). Nearest framework: verify/Sk1Machines.v (mxdys, Sk1 Class 1): same digit-counter shape, but its TM17 endgame is a glider check, which does not apply here.",
 "next_goal": "Stage 1 completion (2 h): write the wall/remnant case table as affine rules and run an exhaustive closure check of the candidate language L on small parameters."
}

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