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 / #16
1RB0LC_1RC0RA_1RD0RF_0LE---_1LB1LA_1LD1RA
Where it stands
Parked at the informal proof
Skeptic round 2 applied (2026-10-12): two fatal gaps remain, neither with a known repair. (1) Window family: long members of H*c4 reach window right ends (long P box: 1 at S=83, 60/1,079,332 at S=168, >=96 at S=339; long E in two steps).
Read the full status
The window start is derived (Clean formula, P0 = d0 + delta; exact on 60, check L1) and delta=0 is ruled by existing rules (59/60), and a new corner rule RightEndP2W (P=2 at a wall = RightEndP to P=0 + Absorb0; exact on 251/251 ruled random frames of 300, negative control, checks M1-M2) rules delta=1 for S even; the rest (delta=1 S odd, delta=2, delta=0 after Push1End with two walls) reaches a V1 right end with walls, whose restart writes (10)^p (101)^q 1 (101)^r, a tape form outside the grammar (check L3; transient in the one run followed, back in the grammar 1,675 steps later). (2) Short regime: the look-ahead Hs_4 is not inductive; wider boxes leak (E1w 110, P1w 12, Pt1 450; Et1/Eseg 0), and Reflect into a top (U24) is reached (check L7). Also open: Lemma T/G/C/CP fitted (CP sketch is only an equivalence with H1 at the successor), 'ak even at Push1' a census fact (not local parity). Fixed this round: box bounds stated and leak counts as lower bounds, U4/U13/U17/U24 relabelled 'refuted by box', V1 parity rewritten as an induction over the rules (conditional on H1), Hc4 total (J2b). Non-halting is very likely (every free run from a leak point runs on: 2e9-4e9 steps), but no inductive invariant is known.
Observe
Deepen
Informal proof
Rocq
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
Self-similar Jacobsthal transfer staircase + (010)-eating bouncer; middle phase not yet closed-form
- Status
- Parkedinformal proof · updated 2026-10-12Not blocking · Stuck at the informal proof stage. Answer Q1–Q3 whenever; a “no” redirects the work.idle since Oct 12 23:02 · status.json 2026-10-12
- Informal proof
- proof.mdconditional; see Proof for what is still open
- Class
- Chaotic Fractal Othersours: sheet Chaotic Fractal Others ≠ ours Fractal: Jacobsthal transfer staircase (right) + bouncer (left), chaotic segment list · med confidence
- On the list
- line 398 of
BB6_holdouts_663.txt· historical 740 line 440
Your calls on file 8
- parked
- Parked by Dennis 2026-10-12 (decision queue: go with recommendations: park).
- 2026-10-11 · corner_rules
- Fund one stage to rule #16's small-value corner events and pin the block-seed clause of H*, so that H* closes without a margin, before proof.md? (Dennis: go with recommendations (2026-10-11))
- 2026-10-12 · corner_rules_2
- Fund one more short stage to rule #16's last three corner sub-families and fix the H* clause for the RightEndP1 output, before proof.md? (Dennis: apply recommendations (2026-10-12))
- 2026-10-10 · hub_invariant
- Fund one stage to write #16's hub-level invariant out explicitly (parity, staircase, linear underflow relations, corner-event rules) and test its closure with the macro simulator, before proof.md? (auto-applied: Claude's recommendation, under Dennis's standing instruction 'do your recommendations and continuously orchestrate' (2026-10-10, while he was away). Override any time.)
- 2026-10-10 · macro_closure
- Fund one stage to close #16's macro-level invariant (the parity rules plus the underflow inequality and the exact staircase relation), checked on random instances, before proof.md? (auto-applied: Claude's recommendation, under Dennis's standing instruction 'do your recommendations and continuously orchestrate' (2026-10-10, while he was at lunch). Override any time.)
- 2026-10-10 · parity_round
- Fund one targeted deepen stage on #16's parity invariant (a parity census at every event, then a parity-aware DFA search) before any proof work? (Dennis: go with all recommendations (2026-10-10))
- 2026-10-12 · seed_clause
- Fund one stage to replace #16's seed clause by closed forms of the short (S) transitions, so that H*c2 becomes inductive, before proof.md? (Dennis: b (fund all five), 2026-10-12)
- 2026-10-12 · park
- #16's invariant still leaks in two places after five funded stages and two skeptic rounds: park it, or fund one more round aimed only at the two fatal gaps? (Dennis 2026-10-12: 'go with recommendations')
Mechanism
How it works: 3 notes
- Right phase: transfers (01)^(T+c) (011)^T -> (011)^(T+c) (01)^T (c = 3 if T even, 2 if odd), nested as domes.
- Left phase: a plain bouncer eats (010)^d, left edge +2 per bounce; one right sweep then starts the next right phase.
- Between them, a record-free middle phase rebuilds the left part; its segment sizes are irregular (the open part).
Figures for Checkpoint A
Blaze view to 1e8 steps. Compare the domes on the left with the domes on the right.
bbchallenge-blazeStart blankRows Blaze time blocks of 131,072 stepsWindow cells -6,064..8,159, 1 px = 17.8 cellsColors 0 1 a mix
Rows: (763 rows, each averaged), stretched to 500 px (1 px ~ 200,000 steps) · Window: each px shows one 16-cell block · Colors: pale orange: the fine 01/011/010 stripes average out over each pixel's cells and time block
One right phase from a built tape. Look to the right of each big dome.
bbchallenge-blazeStart constructed: 0∞ (10)24 (101)24 (01)1400 1 C> 0∞Rows Blaze time blocks of 8,192 stepsWindow cells -3,308..1,367, 1 px = 5.8 cellsColors 0 1 a mix
Rows: (513 rows, each averaged), steps 0..4,200,000, stretched to 500 px · Window: each px shows one 4-cell block; cell 0 = the start head cell · Colors: pale orange: the fine 01/011/010 stripes average out over each pixel's cells and time block
Edge records to 9.6M steps. Track which edge moves, row by row, and how far.
bbchallenge-defaultStart blankRows the start, then one per new leftmost or rightmost cellWindow cells -2,309..2,690, 1 px = 1 cellColors 1 0 head at a new left/right edge
Rows: 5,000 rows (row cap hit), steps 0..9,618,857 only; not evenly spaced in time · Colors: zoomed out, the 1-cell stripes blur to greys (lighter = more 1s)
More figures (1)Fig 4: bbchallenge Default view, first 10,000 steps
For orientation: the start of the run as bbchallenge.org shows it.
bbchallenge-defaultStart blankRows 10,000 steps squeezed into 500 px rowsWindow cells -200..199, 1 px = 1 cellColors 1 0 or never visited head after a right/left move
Rows: 1 px row = 20 steps; the site blends steps 20y+9 and 20y+10
Rules (8/8 validated)exact tape rewrites the proof will formalize, each re-checked by simulation
| rule | from ⟶ to | cases | steps | checked |
|---|---|---|---|---|
| Transfer_even | l (01)x+T+3 (011)T 1 C> 0∞ ⟶ l (01)x (011)T+3 (01)T 1 C> 0∞ | T even, x>=0; l = 0^inf (10)^p (101)^q or 0^inf (10)^p (011)^a | 4T^2+35T+21 | ✓56/56 |
| Transfer_odd | l (01)x+T+2 (011)T 1 C> 0∞ ⟶ l (01)x (011)T+2 (01)T 1 C> 0∞ | T odd, x>=0; same l as Transfer_even | 4T^2+27T+9 | ✓56/56 |
| Conv | l (01)x+S_k 1 C> 0∞ ⟶ l (01)x (011)S_k 1 C> 0∞ | S_0=0, S_(k+1)=2S_k+3 (S_k even) or +2 (odd): 0,3,8,19,40,83,168,339,...; = Transfer iterated | — | ✓12/12 |
| Bounce_C | 0∞ <C (01)a (001101)b (01)c (001)d+2 0∞ ⟶ 0∞ <C (01)a+2 (001101)b (01)c+2 (001)d 0∞ | also holds with middle (001101)^b (01)^e (001101)^f (20/20) | 6a+20b+6c+16 | ✓56/56 |
| Bounce_A | 0∞ <A (10)a (011010)b (10)c (010)d+2 0∞ ⟶ 0∞ <A (10)a+2 (011010)b (10)c+2 (010)d 0∞ | same phase as Bounce_C, seen at the A-record; d even ends in hub (d=0) | — | ✓36/36 |
| BounceEnd_odd | 0∞ <A (10)a (011010)b (10)c 010 0∞ ⟶ 0∞ <A (10)a+2 (011010)b (10)c+1 0∞ | d odd: last half-bounce lands in the hub | — | ✓12/12 |
| Sweep1 | 0∞ <A (10)a+1 (011010)b (10)c 0∞ ⟶ 0∞ (10)a (101)2b+1 (01)c 1 C> 0∞ | b,c>=1: hub -> right phase start (Conv on (01)^c) | — | ✓36/36 |
| Sweep2 | 0∞ <A (10)a+1 (011010)b (10)c+1 (011010)d (10)e 0∞ ⟶ 0∞ (10)a (101)2b+1 (01)c (011)2d (01)e+1 1 C> 0∞ | 5-segment hub; (011)^(2d) acts as a wall for Conv on (01)^(e+1) | — | ✓36/36 |
Compressed historythe tape as 0∞ (10)p (101)q (01)x (011)T 1 C> 0∞ at 22 moments: where the rules are read off
0∞ (10)p (101)q (01)x (011)T 1 C> 0∞
| step | p | q | x | T |
|---|---|---|---|---|
| 14,526,001 | 1,348 | 77 | 1,420 | 0 |
| 14,526,022 | 1,348 | 77 | 1,417 | 3 |
| 14,526,169 | 1,348 | 77 | 1,412 | 8 |
| 14,526,894 | 1,348 | 77 | 1,401 | 19 |
| 14,529,753 | 1,348 | 77 | 1,380 | 40 |
| 14,541,326 | 1,348 | 77 | 1,337 | 83 |
| 14,586,457 | 1,348 | 77 | 1,252 | 168 |
| 14,765,710 | 1,348 | 77 | 1,081 | 339 |
| 15,474,265 | 1,348 | 77 | 740 | 680 |
| 18,295,950 | 1,348 | 77 | 57 | 1,363 |
| 479,669,602 | 4,142 | 3,895 | 5,780 | 0 |
| 479,669,623 | 4,142 | 3,895 | 5,777 | 3 |
| 479,669,770 | 4,142 | 3,895 | 5,772 | 8 |
| 479,670,495 | 4,142 | 3,895 | 5,761 | 19 |
| 479,673,354 | 4,142 | 3,895 | 5,740 | 40 |
| 479,684,927 | 4,142 | 3,895 | 5,697 | 83 |
| 479,730,058 | 4,142 | 3,895 | 5,612 | 168 |
| 479,909,311 | 4,142 | 3,895 | 5,441 | 339 |
| 480,617,866 | 4,142 | 3,895 | 5,100 | 680 |
| 483,439,551 | 4,142 | 3,895 | 4,417 | 1,363 |
| 494,677,386 | 4,142 | 3,895 | 3,052 | 2,728 |
| 539,548,607 | 4,142 | 3,895 | 321 | 5,459 |
plast 4,142qlast 3,895xlast 321Tlast 5,459Template comparisonFractalType7v4.v TM20: partly applies · the nearest solved proof, what carries over, and the transitions that differ
| 0 | 1 | |
|---|---|---|
| A | 1RB | 0LC |
| B | 1RC | 0RA |
| C | 1RD | 0RF |
| D | 0LE | --- |
| E | 1LB | 1LA |
| F | 1LD | 1RA |
differs from the template
- file
FractalType7v4.v:6- module
TM20- machine
1RB0LF_1RC0RA_0RD0RB_1LE0RF_1LB0LE_1LE---(8 transitions apart)- diff
7/11 defined transitions differ (TM20 with D<->F): A1 C0 C1 D0 E1 F0 F1; same A0 B0 B1 E0. All 19 FractalMisc modules: >=8- note
- Rules/shapes do not carry over: TM20 Inc from S1 0/8, FractalMisc TM1 Inc1 0/8 on this machine. Reusable: architecture (P-call recursion, inductive Good invariant with inequalities, chunked native_compute init).
Proof strategy & riskshow the formal proof will go · 3 risks to watch
FractalType7v4 architecture: es/ind lemmas for Transfer (T even/odd) and Bounce, Conv by induction on k, Sweep by chain steps. Then an inductive Good invariant on the segment list with inequality bounds (no exact values) + progress_nonhalt, like Inv_step. First: close the middle (underflow) phase as rules; init via chunked multistep_c + native_compute.
- ▲Middle (underflow) phase has no closed form: result splits on parities of p, q, b; 63/63 probes reach the left edge, rule table unknown
- ▲Segment list grows (3->5 segments by 1e9); the inequalities a Good invariant needs are not known yet
- ▲No template within 7 transitions: new-mechanism proof, likely 20-40 KB
Stats & provenance109 steps simulated · 47,345 cells · the status in full · files
- simulated
- 109 steps
- tape
- 47,345 cells · 21,900 nonzeros
- growth
- span ~t^0.48 (5,086 cells at 1e7, 47,345 at 1e9); right-phase record counts are Jacobsthal numbers (85, 1365, 5461)
- status now
- Skeptic round 2 applied (2026-10-12): two fatal gaps remain, neither with a known repair. (1) Window family: long members of H*c4 reach window right ends (long P box: 1 at S=83, 60/1,079,332 at S=168, >=96 at S=339; long E in two steps). The window start is derived (Clean formula, P0 = d0 + delta; exact on 60, check L1) and delta=0 is ruled by existing rules (59/60), and a new corner rule RightEndP2W (P=2 at a wall = RightEndP to P=0 + Absorb0; exact on 251/251 ruled random frames of 300, negative control, checks M1-M2) rules delta=1 for S even; the rest (delta=1 S odd, delta=2, delta=0 after Push1End with two walls) reaches a V1 right end with walls, whose restart writes (10)^p (101)^q 1 (101)^r, a tape form outside the grammar (check L3; transient in the one run followed, back in the grammar 1,675 steps later). (2) Short regime: the look-ahead Hs_4 is not inductive; wider boxes leak (E1w 110, P1w 12, Pt1 450; Et1/Eseg 0), and Reflect into a top (U24) is reached (check L7). Also open: Lemma T/G/C/CP fitted (CP sketch is only an equivalence with H1 at the successor), 'ak even at Push1' a census fact (not local parity). Fixed this round: box bounds stated and leak counts as lower bounds, U4/U13/U17/U24 relabelled 'refuted by box', V1 parity rewritten as an induction over the rules (conditional on H1), Hc4 total (J2b). Non-halting is very likely (every free run from a leak point runs on: 2e9-4e9 steps), but no inductive invariant is known. (status.json, 2026-10-12)
- observer's note
- Not a cryptid: parity splits are deterministic (T alternates along the staircase); 300 random hub configs x 5e7 steps: 0 halts
- 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
- check_proof_full.txt · its output
What is still open (status.json):
- open lemma: Exists H with K0 in H such that every R in H has a fully ruled traversal whose next right end is in H. Needs (a) rules for RightEndP with P = 3 at a wall, the V1 right end with walls (and the glued-wall left word (10)^p (101)^q 1 (101)^r it creates), and Reflect into a top/level/window; (b) explicit inductive clauses for the short regime (Ec1, El1, Et0, Et1, Pc1, Pt0, Pt1, P-even kinds, Eseg) replacing the look-ahead Hs_4; (c) an invariant that admits the window right ends or excludes the family at every level (it grows: S=83, 168, 339).
Files
machines/<tm>/: 16 entries · raw notes, status, scripts, images
| name | size | changed |
|---|---|---|
| notes.md ↓ | 81 KB | 2026-10-12 14:28 |
| proof.md ↓ | 61 KB | 2026-10-12 14:35 |
| status.json ↓ | 2.2 KB | 2026-10-12 23:02 |
| observe.json ↓ | 11 KB | 2026-10-10 04:41 |
| deepen.json ↓ | 31 KB | 2026-10-12 12:17 |
| decisions/ | 7 items | 2026-10-12 23:02 |
| img/ | 5 items | 2026-10-10 01:05 |
| scripts/ | 230 items | 2026-10-12 14:25 |
| check_proof.py ↓ | 46 KB | 2026-10-12 14:21 |
| check_proof_full.txt ↓ | 9.4 KB | 2026-10-12 14:35 |
| qsim.jsonl ↓ | 97 KB | 2026-10-10 00:27 |
| rulefit.json ↓ | 49 KB | 2026-10-10 00:35 |
| rulefit.txt ↓ | 3.0 KB | 2026-10-10 00:35 |
| sim_1e9.jsonl ↓ | 155 B | 2026-10-10 00:27 |
| sim_1e9.time ↓ | 42 B | 2026-10-10 00:27 |
| validation.log ↓ | 1.5 KB | 2026-10-10 01:06 |
status.json in full
{
"tm": "1RB0LC_1RC0RA_1RD0RF_0LE---_1LB1LA_1LD1RA",
"status": "STUCK",
"stage": "informal_proof",
"updated": "2026-10-12",
"reason": "Skeptic round 2 applied (2026-10-12): two fatal gaps remain, neither with a known repair. (1) Window family: long members of H*c4 reach window right ends (long P box: 1 at S=83, 60/1,079,332 at S=168, >=96 at S=339; long E in two steps). The window start is derived (Clean formula, P0 = d0 + delta; exact on 60, check L1) and delta=0 is ruled by existing rules (59/60), and a new corner rule RightEndP2W (P=2 at a wall = RightEndP to P=0 + Absorb0; exact on 251/251 ruled random frames of 300, negative control, checks M1-M2) rules delta=1 for S even; the rest (delta=1 S odd, delta=2, delta=0 after Push1End with two walls) reaches a V1 right end with walls, whose restart writes (10)^p (101)^q 1 (101)^r, a tape form outside the grammar (check L3; transient in the one run followed, back in the grammar 1,675 steps later). (2) Short regime: the look-ahead Hs_4 is not inductive; wider boxes leak (E1w 110, P1w 12, Pt1 450; Et1/Eseg 0), and Reflect into a top (U24) is reached (check L7). Also open: Lemma T/G/C/CP fitted (CP sketch is only an equivalence with H1 at the successor), 'ak even at Push1' a census fact (not local parity). Fixed this round: box bounds stated and leak counts as lower bounds, U4/U13/U17/U24 relabelled 'refuted by box', V1 parity rewritten as an induction over the rules (conditional on H1), Hc4 total (J2b). Non-halting is very likely (every free run from a leak point runs on: 2e9-4e9 steps), but no inductive invariant is known.",
"confidence": "med",
"open_lemma": "Exists H with K0 in H such that every R in H has a fully ruled traversal whose next right end is in H. Needs (a) rules for RightEndP with P = 3 at a wall, the V1 right end with walls (and the glued-wall left word (10)^p (101)^q 1 (101)^r it creates), and Reflect into a top/level/window; (b) explicit inductive clauses for the short regime (Ec1, El1, Et0, Et1, Pc1, Pt0, Pt1, P-even kinds, Eseg) replacing the look-ahead Hs_4; (c) an invariant that admits the window right ends or excludes the family at every level (it grows: S=83, 168, 339).",
"parked": "Parked by Dennis 2026-10-12 (decision queue: go with recommendations: park)."
}