BB(6) hunt
Machines / W7-2

1RB1LB_1RC0LA_1RD0RE_1LA0LB_1RF---_1RB1LD

W7-2In progressSkelet 1-like Class 1bbchallenge ↗Explorer

Where it stands

In progress: informal proof

proof.md (start-parametric): INV = {N(Y): Y >= 22} u {Q(W): W >= 14}; Lemma N: N(Y) -->+ N(2^18 Y + 32859022); Lemma Q: Q(W) -->+ Q(2^18 W + 34431880); both proved by symbolic runs with empty side-condition logs, no residue condition. Start A (175): blank -->* N(508932094) (= qsim M(508932080) + 14). Start D (489): blank -->* D(X0, 10456559309013950571, 939468133961604901), Lemma D: D(X, Y2, Y1) -->+ D(2^20 X + 349479900, Y2 - 120, Y1 - 24) applied 39144505581733537 times, then the Y1-exhaustion run D(2^20 z + 349479900, 5759218639205926131, 13) -->+ Q(2^33 z + 23036877419765819664) for every z.

Observe
Deepen
Informal proof
Rocq
space-time diagram, first 10,000 steps from blank
The first 10,000 steps from a blank tape. Time runs down; white is 1.
About this picture

The standard picture (bbchallenge.org's Default view): each row is the whole tape at one step, time runs downward, and the head's path draws the pattern.

bbchallenge-defaultStart blankRows steps 0 → 10,000, top to bottomWindow cells −200..199, left to rightColors 1 0 or unvisited

Overview

In one sentence

After about 4.1e18 steps line 175 repeats one exact cycle: big run X -> 2^36 X + 9575900996480.

Status
In progressinformal proof · updated 2026-10-14Not blocking · Proof.md written; next: the Rocq proof. Answer Q1–Q3 whenever; a “no” redirects the work.
idle since Oct 14 21:45 (39 h ago) · status.json 2026-10-14
Informal proof
proof.mdconditional; see Proof for what is still open
Class
Skelet 1-like Class 1ours: sheet Skelet 1-like Class 1 ≠ ours exponential counter with an exact macro cycle M(X) -> M(2^36 X + c) (175); 489 is a deeper tower regime · high confidence
On the list
line 160 of BB6_holdouts_663.txt · historical 740 line 175 · observe.json rank #175
eqv ×2table ×2sim 1e15
Your calls on file 2
next
Formalize: two cycle lemmas (15 segments each, Diff-rule families + 7 shift rules), Lemma D with its iteration, and the opening runs (657,961 and 8.9M + 339,452 engine moves); a trace-replaying tactic or reflective checker is the realistic route. Checkpoint B review of proof.md first (non-blocking).
2026-10-14 · 2026-10-14-superseded
Line 489 (same table, start D) is in a two-far-field tower regime that 175's cycle proof does not cover: park 489, or fund one 2 h stage for its exhaustion events?

Mechanism

How it works: 3 notes
  • Runs of 4-cell words; a marker crosses a run one word per left-end visit and turns each word into two, (0100)^a 1^2 (0001)^(b+1) -> (0100)^(a+2) 1^2 (0001)^b (20/20), so transfers are x -> 2x + c; nothing ever halves. Halting needs B> 0 1 1 (E is entered only from C1, C only from B0).
  • From qsim record 21 (step 4,111,147,719,584,449,981) the record sequence is periodic with period 42: M(X) = 0^inf 1 1011^X 10111110 1110^26 <A 01010100010000010001000100001 0^inf goes to M(2^36 X + 9575900996480), every other field a fixed constant, 56/56 periods exact. All 42 segments of the period re-run by plain simulation from constructed configurations with small random X (same residue mod 64): 165/165; their fitted maps compose to exactly 2^36 X + 9575900996480. X stays fixed mod 2^36, so the 3 parity-flagged qsim rules always end on the same parity.
  • Line 489 (same table, start D, mirrored) is not in the cycle: two far fields Y1 = 9.4e17, Y2 = 1.05e19 are eaten linearly, D(Y1,Y2,X) -> D(Y1-48, Y2-240, 2^40 X + 377451701380050) per 40 records; Y1 runs out after 1.96e16 periods, at tower depth, with an unknown outcome.

Figures for Checkpoint A

Fig 1 · Line 175, first 10,000 steps

The site's own view: a counter grows leftward from the start.

Line 175, first 10,000 steps
bbchallenge-defaultStart blankRows every step (10,000 steps squeezed into 500 px as on the site)Window cells -200..199, 1 px = 1 cellsColors 1 0 head moving R/L
Fig 2 · 175: the 42-record cycleQ1

One row per qsim rule application; bar width is log2 of the run length. Compare rows 21, 63, 105.

175: the 42-record cycle
customStart blankRows one row per qsim rule applicationWindow whole tape; run of length n drawn 1+1.5*log2(n+1) px wideColors run of a 3-ones word run of a 1-one word separator text head blank
Rows: records 0..139, block size 8 · Window: (log scale, not cells) · Colors: white: 0111 rotations; grey: 0001 rotations
Fig 3 · One segment of the cycle, X = 52Q2

Rows are left/right records from the constructed start; the run is crossed again and again, each pass doubling it.

One segment of the cycle, X = 52
bbchallenge-defaultStart constructed: 0∞ 11 (0111)52 <B 101000100000100010001000101001 0∞Rows left/right records for 2,482,418 stepsWindow cells -1677..0, 1 px = 1 cellsColors 1 0 head moving R/L
Rows: ends at 0^inf 1 1011^385 <A 01^2 0100^29 0001^3 0^4 1 0^inf · Window: right edge fixed
More figures (2)Fig 4–5: Line 489, right records · 489: two huge far fields
Fig 4 · Line 489, right records

Mirror image of 175's picture; the long far-end list sits on the left.

Line 489, right records
bbchallenge-defaultStart blankRows right records for 300,000 stepsWindow cells 0..689, 1 px = 1 cellsColors 1 0 head moving R/L
Window: left edge fixed
Fig 5 · 489: two huge far fields

Same drawing as Fig 2, mirrored; from row 50 two long grey far fields stay while the head side grows.

489: two huge far fields
customStart blankRows one row per qsim rule applicationWindow whole tape; run of length n drawn 1+log2(n+1) px wideColors run of a 3-ones word run of a 1-one word separator text head blank
Rows: (records 0..199, block size 8), drawn mirrored · Window: (log scale, not cells)
Rules (5/6 validated)exact tape rewrites the proof will formalize, each re-checked by simulation
rulefrom ⟶ tocasesstepschecked
visit (doubling transfer)
0∞ <B 101 (0100)a 12 (0001)b+1 (010)2 (0100)99 1 (0010)14 03 1 0∞
⟶ 0∞ <B 101 (0100)a+2 12 (0001)b (010)2 (0100)99 1 (0010)14 03 1 0∞
a >= 1, b >= 0 (1e9 run: 75 visits in a row)about 16a + const✓20/20
segment 20 (x4)
0∞ 11 (0111)Z <B 101000100000100010001000101001 0∞
⟶ 0∞ 11011 (1011)4Z+176 <A 01010100 (0100)28 00010001000100001 0∞
Z = 52 mod 64 tested (cycle value)2,482,418 at Z = 52✓4/4
all 42 cycle segments
record k of the period, big field Z
⟶ record k+1, big field a_k Z + b_k (a_k in {1,2,4})
Z with the cycle's residue mod 64; 2-4 random Z per segment—✓165/165
cycle M (175)
0∞ 1 (1011)X 10111110 (1110)26 <A 01010100010000010001000100001 0∞
⟶ 0∞ 1 (1011)68719476736X+9575900996480 10111110 (1110)26 <A 01010100010000010001000100001 0∞
X = 0 mod 16 suffices on the observed orbit (X0 = 508932080 = 48 mod 64, then 0 mod 64)about (10)21.7 per period at X ~ (10)10✓56/56
489 period (D regime)
0∞ 100001000 (1000)y 10010010 (0010)z 0010010010100010001000100000100010001010 B> (1101)x 11011 0∞
⟶ 0∞ 100001000 (1000)y-48 10010010 (0010)z-240 0010010010100010001000100000100010001010 B> (1101)1099511627776x+377451701380050 11011 0∞
observed with y = 9.4e17, z = 1.05e19; not base-validated (needs 3-field segment checks)—–untested
489 visit (mirror)
0∞ (100)2 (0001)59 001 (0010)364 05 (0001)295 06 (0001)a+1 1 (0010)b 101 C> 0∞
⟶ 0∞ (100)2 (0001)59 001 (0010)364 05 (0001)295 06 (0001)a 1 (0010)b+2 101 C> 0∞
a >= 0, b >= 1—✓20/20
Compressed historythe tape as 0∞ 1 (1011)X 10111110 (1110)26 <A 01010100010000010001000100001 0∞ at 12 moments: where the rules are read off
0∞ 1 (1011)X 10111110 (1110)26 <A 01010100010000010001000100001 0∞
stepXdigits of X
4.11·1018508,932,0809
1.93·10403.49·101920
9.14·10612.4·103031
4.31·10831.65·104142
2.03·101051.13·105253
9.63·101267.79·106263
4.54·101485.35·107374
2.14·101703.68·108485
1.01·101922.53·109596
4.79·102131.73·10106107
2.26·102351.19·10117118
1.06·102578.21·10127128
Xlast 8.21·10127
8.2e1275.1e84.1e181.1e257log-logstep 4111147719584449981: X = 508932080step 1.9e40: X = 34973555807665087360step 9.1e61: X = 2403364454700038670890828653440step 4.3e83: X = 1.7e41step 2e105: X = 1.1e52step 9.6e126: X = 7.8e62step 4.5e148: X = 5.4e73step 2.1e170: X = 3.7e84step 1e192: X = 2.5e95step 4.8e213: X = 1.7e106step 2.3e235: X = 1.2e117step 1.1e257: X = 8.2e127
digits of Xlast 128
12894.1e181.1e257log xstep 4111147719584449981: digits of X = 9step 1.9e40: digits of X = 20step 9.1e61: digits of X = 31step 4.3e83: digits of X = 42step 2e105: digits of X = 53step 9.6e126: digits of X = 63step 4.5e148: digits of X = 74step 2.1e170: digits of X = 85step 1e192: digits of X = 96step 4.8e213: digits of X = 107step 2.3e235: digits of X = 118step 1.1e257: digits of X = 128
Template comparisontemplate: partly applies · the nearest solved proof, what carries over, and the transitions that differ
01
A1RB1LB
B1RC0LA
C1RD0RE
D1LA0LB
E1RF---
F1RB1LD
file
machines/1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---/
module
—
machine
1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB--- (8 transitions apart)
diff
—
note
Our kill #3 (Skelet 1-like Class 2): one macro lemma per segment + progress_nonhalt, Individual62. Here the invariant is just 'exists m, c = M(16m)' with the 42-segment chain as one lemma. Sk1Machines.v (Sk1CounterMixed/Sk1Auto) does not fit the cycle; Sk1Auto's checked run is an option for the 4.1e18-step base segment.
Proof strategy & riskshow the formal proof will go · 3 risks to watch

175 only: proof.md for the cycle lemma M(X) -->+ M(2^36 X + 9575900996480) on X = 0 mod 16 (42 segment lemmas from about 12 sweep shapes), then the base segment c0 -->* M(508932080) (21 qsim records, about 4.1e18 steps) from the same sweep lemmas with concrete numbers. 489 is a separate decision.

  • ▲The base segment (4.1e18 steps, 21 records with their own skeletons) needs its own lemma instances; not yet base-validated segment by segment.
  • ▲Some cycle segments may need a residue mod 8 or 16 of their own field; the proof must carry the exact class (mod-4 rerun pending).
  • ▲489 may need a full digit-system theory (tower depth); it is not covered by the 175 proof.
Stats & provenance1010 steps simulated · 127,078 cells · the status in full · files
simulated
1010 steps
tape
127,078 cells · 37,602 nonzeros
growth
qsim: 10^3424 steps, 10^1712 nonzeros in 120 s; cycle multiplies X by 2^36
status now
proof.md (start-parametric): INV = {N(Y): Y >= 22} u {Q(W): W >= 14}; Lemma N: N(Y) -->+ N(2^18 Y + 32859022); Lemma Q: Q(W) -->+ Q(2^18 W + 34431880); both proved by symbolic runs with empty side-condition logs, no residue condition. Start A (175): blank -->* N(508932094) (= qsim M(508932080) + 14). Start D (489): blank -->* D(X0, 10456559309013950571, 939468133961604901), Lemma D: D(X, Y2, Y1) -->+ D(2^20 X + 349479900, Y2 - 120, Y1 - 24) applied 39144505581733537 times, then the Y1-exhaustion run D(2^20 z + 349479900, 5759218639205926131, 13) -->+ Q(2^33 z + 23036877419765819664) for every z. (status.json, 2026-10-14)
observer's note
175: exact macro cycle found and base-validated; go to proof.md. 489: different regime, filed as a decision.
files
observe.json · notes.md · proof.md · status.json

Proof & checks

○ Checkpoint B: no note from Dennis found

  • proof.md L9: - Stage: informal_proof (2026-10-14). Status: OPEN (Checkpoint B material; not formalized).

Files

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

namesizechanged
notes.md ↓9.0 KB2026-10-14 21:42
proof.md ↓19 KB2026-10-14 21:45
status.json ↓1.8 KB2026-10-14 21:42
observe.json ↓13 KB2026-10-14 20:23
decisions/1 item2026-10-14 21:42
img/6 items2026-10-14 20:18
scripts/9 items2026-10-14 21:13
work/18 items2026-10-14 21:38
check_proof.py ↓17 KB2026-10-14 21:38
status.json in full
{
 "tm": "1RB1LB_1RC0LA_1RD0RE_1LA0LB_1RF---_1RB1LD",
 "label": "W7-2",
 "status": "OPEN",
 "stage": "informal_proof",
 "updated": "2026-10-14",
 "confidence": "high",
 "confidence_note": "both starts covered at the informal level by checked symbolic runs (check_proof.py ALL OK); soundness rests on scripts/engine.py, validated by section B, not yet by an independent implementation or Rocq",
 "holdout_line_740": 175,
 "reason": "proof.md (start-parametric): INV = {N(Y): Y >= 22} u {Q(W): W >= 14}; Lemma N: N(Y) -->+ N(2^18 Y + 32859022); Lemma Q: Q(W) -->+ Q(2^18 W + 34431880); both proved by symbolic runs with empty side-condition logs, no residue condition. Start A (175): blank -->* N(508932094) (= qsim M(508932080) + 14). Start D (489): blank -->* D(X0, 10456559309013950571, 939468133961604901), Lemma D: D(X, Y2, Y1) -->+ D(2^20 X + 349479900, Y2 - 120, Y1 - 24) applied 39144505581733537 times, then the Y1-exhaustion run D(2^20 z + 349479900, 5759218639205926131, 13) -->+ Q(2^33 z + 23036877419765819664) for every z.",
 "siblings": [
  "1RB0RC_1LC1RC_1LD0RB_1LA0LE_1LF---_1LC1RA"
 ],
 "sibling_note": "489 = this table from start D (mirrored, renamed); canon(489,A) = canon(175,D). proof.md covers 489 too (start D enters cycle Q). Starts B, C, E, F are not on the 740 list; start F is upstream Eqv_v2.v TM595 tm (halting-equivalent to 175, unproved).",
 "upstream": "No upstream proof of any start; Eqv_v2.v TM595 links start F to 175 only.",
 "next": "Formalize: two cycle lemmas (15 segments each, Diff-rule families + 7 shift rules), Lemma D with its iteration, and the opening runs (657,961 and 8.9M + 339,452 engine moves); a trace-replaying tactic or reflective checker is the realistic route. Checkpoint B review of proof.md first (non-blocking).",
 "proof": "proof.md",
 "check": "check_proof.py (ALL OK, work/check_proof_all.txt)"
}
observe.json contract (tools/README-card.md):
2 contract warnings
  • diagrams[1].window: not "cells A..B, 1 px = k cells"
  • diagrams[4].window: not "cells A..B, 1 px = k cells"