BB(6) hunt
Machines / W7-1

1RB1RC_1LC1LE_1RD0RA_1LB0RA_0LD1LF_1LD---

W7-1ParkedSkelet 1-like Class 1bbchallenge ↗Explorer

Where it stands

Parked at the informal proof

proof.md revision 2 (after the skeptic review of revision 1). Fixed: both major gaps (PLUS-MERGE-1 now handled by a general merged-state lemma C3, a two-mode climb automaton C5 and both reflection branches C6; far-end 0+ rules FAR-0-PLUS-EVEN/ODD added and J3 relaxed) and all minor gaps (scaled budget f*2^u, SP smaller copy, 15 rules, (o1) wording, C1 statement, Reduction wording, (o5) count).

Read the full status

Open, fatal: O1, no inductive invariant. J has five one-step exits and halting members (2 + 1 # 2 halts after 186 steps). New: the far end decides halting by a race whose outcome depends on history-dependent counter parities; 24 of 300 perturbations of line 75's 1e13 configuration leave the rule set between 1e14 and 1e85 steps, 22 of them at the far end (3 reach the halting + 0 +). The four real orbits meet no outside case to 1e100 (check_proof.py section I) and 1e150 (work/rev2/far.py). Cryptid-protocol stop; decision.json filed.

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

Binary counter on budget fields (10)^f 1; parities are the digits; dead fields re-pair; no halt to 2.37e14.

Status
Parkedinformal proof · updated 2026-10-14Not blocking · Stuck at the informal proof stage. Answer Q1–Q3 whenever; a “no” redirects the work.
idle since Oct 16 10:32 (2 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 Skelet 1-like: binary counter whose digits are field parities, with re-pairing bounces · high confidence
On the list
line 70 of BB6_holdouts_663.txt · historical 740 line 75 · observe.json rank #75
eqv ×1table ×4sim 1e15
Your calls on file 2
next
Waiting on Dennis (decision.json). If halt-search: run work/rev2/fastmap.py-style exact map for the four starts as far as 2 h allows, extend it to the far-end exits (gap-4 walls) if one is reached, and report any + 0 + as a halting-kill candidate.
decision.json · answered 2026-10-16: halt-search
W7-1 (lines 75/597/265/179): park it as cryptid-like, or fund a bounded 2 h halting search with the exact fast map toward 10^1000 steps? Decisions →

Mechanism

How it works: 3 notes
  • At every D:R event the tape is a list of fields [f]=(10)^f 1 joined by separators | (00), + (11) or # (000); the last field L is the growing end.
  • Each half-cycle the head walks left over even fields to the first odd field (or a + or #), takes 1 from the field just left of it and adds 3 to L: the field parities are the digits of a binary counter (ruler sequence).
  • A field that reaches 0 becomes a # separator; the next carry into it is a uniform re-pairing bounce (+2 to the field right of it, +1 to the rest, all separators +, new L = 1). A carry past the far end is the same bounce for the whole tape. Exact simulator: no halt to 2.367e14; the 4 starts share every event and differ only in the first field.

Figures for Checkpoint A

Fig 1 · The field counter, 128 half-cyclesQ1

One row per half-cycle; columns are the 14 fields. Follow one column: when does it change colour?

The field counter, 128 half-cycles
customStart mid-run: step 300,021,233Rows one 3 px row per half-cycleWindow cells 1..14, 1 px = 0.083 cellsColors odd field even field field that loses 1 this half-cycle last field L (+3 each row) | separator + separator
Start: token list of line 75 at a D:R event · Rows: (D:R to next D:R), 128 half-cycles · Window: a 'cell' here is one field f_i, 12 px wide; not tape cells
Fig 2 · Death and re-pairing, constructedQ2

Watch the third field (0): its gap widens, its left neighbour shrinks once, then one long V.

Death and re-pairing, constructed
bbchallenge-defaultStart constructed tape (below)Rows every step, 722 stepsWindow cells -84..15, 1 px = 1 cellColors 1 0 head moving R/L
Start: 0∞ (10)7 1 00 (10)6 1 00 1 00 (10)5 1 00 (10)4 1 00 11 D> 0∞ · Rows: 7|6|0|5|4 -> 7|6#5|7 -> .. -> 7|5+5+17|1 -> 7|5+3|16|7
More figures (2)Fig 3–4: Default view, first 10,000 steps · Seven half-cycles, constructed fields
Fig 3 · Default view, first 10,000 steps

The site's picture: striped (10) fields; the far-left resets of the first 10^4 steps settle into right-end growth.

Default view, first 10,000 steps
bbchallenge-defaultStart blankRows every step; 10,000 steps squeezed into 500 rowsWindow cells -200..199, 1 px = 1 cellColors 1 0 head moving R/L
Rows: site canvas
Fig 4 · Seven half-cycles, constructed fields

Each V is one half-cycle: the head turns just past the first odd field; the right edge grows.

Seven half-cycles, constructed fields
bbchallenge-defaultStart constructed tape (below)Rows every step, 1,040 stepsWindow cells -94..15, 1 px = 1 cellColors 1 0 head moving R/L
Start: 0∞ (10)9 1 00 (10)6 1 00 (10)5 1 00 (10)8 1 00 (10)4 1 00 11 D> 0∞ · Rows: 7 half-cycles: 9|6|5|8|4 -> 8|5|3|5|25
Rules (9/9 validated)exact tape rewrites the proof will formalize, each re-checked by simulation
rulefrom ⟶ tocasesstepschecked
ODD
.. f_d | f_j(odd) | e .. | L (all fields right of f_j even)
⟶ .. (f_d - 1) | f_j | e .. | (L + 3)
f_d >= 1 (1 -> 0 included); separator left of f_d is | or +6S + 12n + 12 (S, n = sum, count of f_j..L)✓665/665
PLUS
.. f + e_j | e .. | L (e = even)
⟶ .. (f - 2) | e_j | e .. | (L + 3)
f >= 36S + 12n + 10✓300/300
death
a | 0 | b(odd) | e ..
⟶ a # b | e .. (L + 3)
—6S + 12n + 12✓150/150
death-merge
a + 0 | b(odd) | e ..
⟶ (a + b + 1) | e .. (L + 3)
—6S + 12n + 12✓150/150
hash-odd
a # e | .. | L
⟶ (a - 1) # e | .. | (L + 3)
—6S + 12n + 18✓150/150
hash-bounce (re-pairing + birth)
a # b(odd) | e_1 | .. | e_m
⟶ a + (b+2) + (e_1+1) + .. + (e_m+1) | 1
—6S + 6n + 28✓150/150
overflow-even (far end)
e_1 | .. | e_m (all even)
⟶ 1 + (e_1+1) + .. + (e_m+1) | 1
—6S + 6n + 28✓150/150
overflow-odd (far end)
o | e_2 | .. | e_m
⟶ (o+2) + (e_2+1) + .. + (e_m+1) | 1
—6S + 6n + 28✓150/150
ODD-across-plus
d + j(odd) | e ..
⟶ (d - 1) | (j - 1) | e .. (L + 3)
d >= 2 (d = 1 at the far end: 1 + j -> 0 | j-1)6S + 12n + 8✓150/150
Compressed historythe tape as 0∞ [f_1] s_1 [f_2] ... s_{k-1} [f_k] 00 11 D> 0∞, [f] = (10)f 1, s in {| = 00, + = 11-join, # = 000} at 7 moments: where the rules are read off
0∞ [f_1] s_1 [f_2] ... s_{k-1} [f_k] 00 11 D> 0∞, [f] = (10)f 1, s in {| = 00, + = 11-join, # = 000}
stepfields kfar-end prefix + first fieldL = f_kmax fieldcells
1,000,003,379132516,63916,63981,673
10,000,057,453161 + 2051,50851,508266,748
100,000,835,151191 + 1 + 1673,819132,074908,321
1·1012191 + 10231,499443,9412,884,505
1·1013208174,2832,072,8768,834,812
1·1014241 + 1 + 55,027,2665,027,26626,899,366
2.36·1014241 + 0 | 28,737,5318,737,53139,300,840
fields klast 24
24131e92.4e14log xstep 1000003379: fields k = 13step 10000057453: fields k = 16step 100000835151: fields k = 19step 1000005709393: fields k = 19step 10000006342829: fields k = 20step 100000020965165: fields k = 24step 236695882593413: fields k = 24
far-end prefix + first fieldlast 1 + 0 | 2
2581e91e13log xstep 1000003379: far-end prefix + first field = 25step 10000006342829: far-end prefix + first field = 8
L = f_klast 8,737,531
8.7e616,6391e92.4e14log xstep 1000003379: L = f_k = 16639step 10000057453: L = f_k = 51508step 100000835151: L = f_k = 73819step 1000005709393: L = f_k = 231499step 10000006342829: L = f_k = 174283step 100000020965165: L = f_k = 5027266step 236695882593413: L = f_k = 8737531
max fieldlast 8,737,531
8.7e616,6391e92.4e14log xstep 1000003379: max field = 16639step 10000057453: max field = 51508step 100000835151: max field = 132074step 1000005709393: max field = 443941step 10000006342829: max field = 2072876step 100000020965165: max field = 5027266step 236695882593413: max field = 8737531
cellslast 39,300,840
3.9e781,6731e92.4e14log xstep 1000003379: cells = 81673step 10000057453: cells = 266748step 100000835151: cells = 908321step 1000005709393: cells = 2884505step 10000006342829: cells = 8834812step 100000020965165: cells = 26899366step 236695882593413: cells = 39300840
Template comparison1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---.v: partly applies · the nearest solved proof, what carries over, and the transitions that differ
01
A1RB1RC
B1LC1LE
C1RD0RA
D1LB0RA
E0LD1LF
F1LD---
file
machines/1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---/1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---.v ⚠ not at pin
module
—
machine
1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB--- (9 transitions apart)
diff
#3: explicit digit blocks s(d) on (10)^p (01)^q pairs; here the digits are field parities, 3 separator kinds (| + #), far-end prefixes, births at every bounce
note
Our kill #3 (Skelet 1-like Class 2): same architecture (one macro rule per decrement, merges, re-pairing overflow, per-step invariant J). Upstream Sk1Machines.v / Sk1like_TC_v*.v (mxdys) use other digit words: not templates.
Proof strategy & riskshow the formal proof will go · 3 risks to watch

Prove a token-level invariant INV (allowed local patterns, budgets of the fields next to # and +, far-end prefix set) closed under the 9 validated rules plus the far-end table; nonhalting follows. One argument for the table; 179/265/597 are #24-style deltas (own base segment into the same family, first field as a parameter).

  • ▲The global invariant is open: 255 of 4,000 random tiny token lists halt, so INV must exclude bad local patterns for all field values.
  • ▲Far-end prefix set looks small (about 10 shapes in 35 x 12 hand-built deaths) but is not shown closed; line 75's natural far-end death is due just after 2.4e14.
  • ▲The case table (9 rules plus far-end variants) is larger than #3's; the formal stage may exceed 1 agent-day.
Stats & provenance2.4·1014 steps simulated · 39,300,840 cells · the status in full · files
simulated
2.4·1014 steps
tape
39,300,840 cells
growth
span 82k at 1e9, 267k at 1e10, 2.9M at 1e12, 8.8M at 1e13, 39M at 2.4e14 (exact accelerated simulator); direct C runs to 1e10 on all 4 strings
status now
proof.md revision 2 (after the skeptic review of revision 1). Fixed: both major gaps (PLUS-MERGE-1 now handled by a general merged-state lemma C3, a two-mode climb automaton C5 and both reflection branches C6; far-end 0+ rules FAR-0-PLUS-EVEN/ODD added and J3 relaxed) and all minor gaps (scaled budget f*2^u, SP smaller copy, 15 rules, (o1) wording, C1 statement, Reduction wording, (o5) count). Open, fatal: O1, no inductive invariant. J has five one-step exits and halting members (2 + 1 # 2 halts after 186 steps). New: the far end decides halting by a race whose outcome depends on history-dependent counter parities; 24 of 300 perturbations of line 75's 1e13 configuration leave the rule set between 1e14 and 1e85 steps, 22 of them at the far end (3 reach the halting + 0 +). The four real orbits meet no outside case to 1e100 (check_proof.py section I) and 1e150 (work/rev2/far.py). Cryptid-protocol stop; decision.json filed. (status.json, 2026-10-14)
observer's note
Mechanism found and validated; not a cryptid stop (affine events, parity = binary-counter digit). Stage 1 continues: invariant / closure for proof.md.
files
observe.json · notes.md · proof.md · status.json

Proof & checks

What is still open (status.json):

  • open lemma: O1: an inductive J* => J on the orbit from K(c). It needs budget clauses B1-B4 in counter terms (section 6.3) and a far-end clause certifying the safe order in every far-end window (section 6.4), which perturbation evidence shows is not a threshold condition.

Files

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

namesizechanged
notes.md ↓12 KB2026-10-14 22:29
proof.md ↓42 KB2026-10-14 22:30
status.json ↓2.8 KB2026-10-14 22:29
observe.json ↓9.9 KB2026-10-14 20:43
decision.json ↓2.5 KB2026-10-16 10:32
data/31 items2026-10-14 22:32
img/4 items2026-10-14 20:41
work/20 items2026-10-14 22:25
check_proof.py ↓49 KB2026-10-14 22:28
status.json in full
{
 "tm": "1RB1RC_1LC1LE_1RD0RA_1LB0RA_0LD1LF_1LD---",
 "label": "W7-1",
 "status": "STUCK",
 "stage": "informal_proof",
 "updated": "2026-10-14",
 "confidence": "high on the proved parts (15 rules, counter calculus C1-C6 with the climb automaton, openings, SP, LE); open lemma O1 is a far-end race that looks pseudo-random",
 "holdout_line_740": 75,
 "reason": "proof.md revision 2 (after the skeptic review of revision 1). Fixed: both major gaps (PLUS-MERGE-1 now handled by a general merged-state lemma C3, a two-mode climb automaton C5 and both reflection branches C6; far-end 0+ rules FAR-0-PLUS-EVEN/ODD added and J3 relaxed) and all minor gaps (scaled budget f*2^u, SP smaller copy, 15 rules, (o1) wording, C1 statement, Reduction wording, (o5) count). Open, fatal: O1, no inductive invariant. J has five one-step exits and halting members (2 + 1 # 2 halts after 186 steps). New: the far end decides halting by a race whose outcome depends on history-dependent counter parities; 24 of 300 perturbations of line 75's 1e13 configuration leave the rule set between 1e14 and 1e85 steps, 22 of them at the far end (3 reach the halting + 0 +). The four real orbits meet no outside case to 1e100 (check_proof.py section I) and 1e150 (work/rev2/far.py). Cryptid-protocol stop; decision.json filed.",
 "siblings": [
  "1RB0LD_1RC1RE_1LA0LD_1LB1LC_0RA1RF_1RA---",
  "1RB0RE_1LC0RE_1LA1LD_0LB1LF_1RC1RA_1LB---",
  "1RB1RE_1LC0LD_1RA0LD_1LA1LB_0RC1RF_1RC---"
 ],
 "sibling_note": "Same table from other starts: 179 = start D (mirrored), 265 = start C, 597 = start B (mirrored); no folders created for them. At 1e10 all four have the same token list except the first field (75: 20, 597: 24, 265: 46, 179: 44); 75 and 265 share every event to 2.367e14.",
 "upstream": "No upstream proof of this table (Astra equivalence inventory 2026-10-14: none). Class file Sk1Machines.v (ccz181078/mxdys) does not contain it.",
 "next": "Waiting on Dennis (decision.json). If halt-search: run work/rev2/fastmap.py-style exact map for the four starts as far as 2 h allows, extend it to the far-end exits (gap-4 walls) if one is reached, and report any + 0 + as a halting-kill candidate.",
 "proof": "proof.md (revision 2, STUCK: O1); check_proof.py (PASS, sections A-I); data/check_proof.out; work/rev2/ (fast map, perturbation and far-end evidence); data/abstract_runs.md",
 "open_lemma": "O1: an inductive J* => J on the orbit from K(c). It needs budget clauses B1-B4 in counter terms (section 6.3) and a far-end clause certifying the safe order in every far-end window (section 6.4), which perturbation evidence shows is not a threshold condition.",
 "cryptid_flag": "far-end race (proof.md section 6.4): pseudo-random parity bits decide each far-end window",
 "decision": "decision.json (halt-search recommended: bounded exact fast-map run of the four starts toward 1e1000)"
}
observe.json contract (tools/README-card.md):
1 contract warning
  • template file not in the pinned tree: machines/1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---/1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---.v