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-6

`1RB0LA_1RC---_0LD1RD_0RA0RE_0RF1RC_1LF0LA`

W7-6Cryptid candidateTranslated Counterbbchallenge ↗Explorer

Where it stands

Cryptid candidate, parked at the observation

Stage 1 (W7-6) stopped by its stop rule. The counting phase is exact: at every C right record the word is a base-4 counter on pairs of 1-runs (23=0, 22=1, 33=2, 32=3, top digit 3) and each record adds 1 (10,416/10,416 random transitions, w = 2..40); it cannot halt while counting.

Read the full status

Halting is possible only at phase events: overflow -> A erases the trail -> nested rebuild -> the new counter collides with markers / the old remnant. Synthetic scans show a collision halts only for an exact (value, gap) pair (w=3: V=49, gap 28 halts at 6,290 steps). The real orbit survived every event to 2.1e7; the current 23-pair counter (V = 61,170,343,443,693 at step 100,000,903, irregular high digits) overflows after ~9.2e12 increments, about 4.6e15 steps, trail ~1.8e13. Whether that transition halts is an exact big-number coincidence question: cryptid-like lottery, not settled. No nonhalting work (taken class, M-Abozaid SOTCv2.v).

Observe

Deepen

Informal proof

Rocq

Overview

In one sentence

Exact base-4 counter while counting; halts only at overflow/collision events hinging on exact coincidences.

Status: Cryptid candidatewave7-stage1 · updated 2026-10-14Parked · Stage 1 (W7-6) stopped by its stop rule. The 2 open questions are optional.
idle since Oct 16 10:32 (2 h ago) · status.json 2026-10-14
Class: Translated Counterours: sheet Translated Counter ≠ ours Translated base-4 counter with overflow, trail erase and nested rebuild (phase cycle) · med confidence
On the list: line 29 of BB6_holdouts_663.txt · historical 740 line 33 · observe.json rank #33
eqv ×1sim 1e13

Your calls on file 1

decision.json · answered 2026-10-16: park: Park line 33 as a cryptid-like translated counter, or fund one 2 h stage to build the exact phase model and decide the transition at ~4.6e15 steps? Decisions →

Mechanism

How it works: 7 notes

Counting phase: a ~4w+3-cell counter moves right over blank tape and leaves a trail 1^N behind; each tick the head sweeps the whole counter left and back.
At every C right record the word is 0^inf L 1^N 0^2 s_1 0 s_2 0 ... s_2w 0 1 C> 0^inf with s_i in {1^2, 1^3}; pairs are base-4 digits MSB first: 23=0, 22=1, 33=2, 32=3; '4 3' = digit 0 with a pending carry.
Rule R1 (exact, 10,416/10,416 random record transitions, w = 2..40): each C right record shows value V+1. The top digit is always 3, so a w-pair counter runs at most 4^(w-1) increments.
Overflow (all digits 3 + carry): A sweeps left erasing the trail (A1 = 0LA); separators 0 1^2 0 become single-1 markers; a small counter is rebuilt at the left end and counts through the gap.
Collision: when the counter front reaches a marker or the old counter's remnant, it either absorbs it (counter grows) or halts. Synthetic scans: the outcome depends on the exact (value, gap) pair, e.g. w=3, V=49, gap 28 halts at step 6,290.
History: phase 1 (8 pairs) overflowed at 3.73e6; nested rebuilds 3.7e6-2.1e7 (gaps 0^(2*4^k-2)); the current phase is a 23-pair counter (V = 61,170,343,443,693 at step 100,000,903) that overflows after ~9.2e12 more increments, ~4.6e15 steps, trail ~1.8e13.
Family: lines 472, 569, 690 are distinct tables (not starts of 33's table) with the same architecture by end tapes (1^5408013, 1^4591407, 1^10536 0 1^2 0 1^5410013 at 1e9); qsim 0 rules on all four.

Figures for Checkpoint A

Fig 1 · Phases to 2.2e7: count, erase, rebuildQ1
White wedges are counting phases; the near-flat lines are A erasing the trail after an overflow.

Fig 2 · Two counter ticks, w = 4 pairs
Each tick the head crosses the whole counter; compare the digit blocks before and after each sweep.

Fig 3 · A collision that haltsQ2
The counter absorbs the marker, overflows, rebuilds and halts: halting needs this exact value/gap coincidence.

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

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

rule	from ⟶ to	cases	steps	checked
R1 record increment	0^∞ L 1^N 0² enc_w(V) 1 C> 0^∞ ⟶ next C right record: enc_w(V+1) (carry shown as '4 3')	V < 4^w - 1; top digit 3	~20 (low pair) or one full sweep, ~502 per increment at w=23	✓10416/10416
R2 digit code	pair (s1,s2) of 1-runs ⟶ 23->0, 22->1, 33->2, 32->3	w = 2..40	—	✓10416/10416
R3 trail growth	N ⟶ N + ~2 per increment (79,689 over 39,847 increments)	w = 23, measured, not exact	—	✓1/1
R4 collision outcome	enc_w(V) 1 C> 0^g 1 0^∞ ⟶ absorb (counter grows) or HALT, depending on exact (V, g)	w=3: 3 halting cells of 8 x 48 (one orbit); w=2: V=15 halts for most g	—	✓432/432

Compressed historythe tape as 0^∞ 1³ 0 1² 0 1⁵ 0 1¹³²² 0 1² 0 1^N 0² enc23(V) 1 C> 0^∞ at 2 moments: where the rules are read off

0^∞ 1³ 0 1² 0 1⁵ 0 1¹³²² 0 1² 0 1^N 0² enc23(V) 1 C> 0^∞

step	`N`	`V`
100,000,903	399,782	6.11·10¹³
119,999,033	479,471	6.11·10¹³

Nlast 479,471

Vlast 6.11·10¹³

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

	0	1
A	1RB	0LA
B	1RC	---
C	0LD	1RD
D	0RA	0RE
E	0RF	1RC
F	1LF	0LA

file: SOTCv2.v:8
module: TM1
machine: 1RB---_0RC1LF_1LC1LD_1RE0RA_0RD1RF_0LD0LF (11 transitions apart)
diff: different table (nearest SOTC/BTC proof >= 5 transitions away)
note: M-Abozaid's token/sweep lemmas fit the counting phase (R1); nothing upstream covers overflow -> erase -> nested rebuild -> collision, where this machine can halt.

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

No nonhalting proof attempted (taken class; needs a new decision). HALT route only: an exact phase-level model (R1 closed form + run-length transitions) to decide the transition after the 23-pair counter overflows (~4.6e15 steps).

▲Collision outcomes hinge on exact coincidences of large irregular numbers (the 23-pair start value has irregular digits): cryptid-like lottery.
▲A HALT at ~4.6e15+ needs a checked runner with a formal increment lemma (W5-5-style base-4 digit lemmas).
▲Translated Counter is M-Abozaid's class (SOTCv2.v); nonhalting work needs a separate call.

Stats & provenance10⁹ steps simulated · 3,954,386 cells · the status in full · files

simulated: 10⁹ steps
tape: 3,954,386 cells · 3,954,346 nonzeros
growth: trail ~2 cells per increment, ~4.0e5 cells per 1e8 steps (linear within a phase)
status now: Stage 1 (W7-6) stopped by its stop rule. The counting phase is exact: at every C right record the word is a base-4 counter on pairs of 1-runs (23=0, 22=1, 33=2, 32=3, top digit 3) and each record adds 1 (10,416/10,416 random transitions, w = 2..40); it cannot halt while counting. Halting is possible only at phase events: overflow -> A erases the trail -> nested rebuild -> the new counter collides with markers / the old remnant. Synthetic scans show a collision halts only for an exact (value, gap) pair (w=3: V=49, gap 28 halts at 6,290 steps). The real orbit survived every event to 2.1e7; the current 23-pair counter (V = 61,170,343,443,693 at step 100,000,903, irregular high digits) overflows after ~9.2e12 increments, about 4.6e15 steps, trail ~1.8e13. Whether that transition halts is an exact big-number coincidence question: cryptid-like lottery, not settled. No nonhalting work (taken class, M-Abozaid SOTCv2.v). (status.json, 2026-10-14)
observer's note: Stage 1 stop rule: counting is exact (R1), but halting happens only at overflow/collision events whose outcome depends on exact coincidences of large irregular numbers.
files: observe.json · notes.md · status.json

Proof & checks

No proof work yet.

Files

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

name	size	changed
notes.md ↓	6.3 KB	2026-10-14 22:51
status.json ↓	3.2 KB	2026-10-14 22:50
observe.json ↓	7.7 KB	2026-10-14 22:50
decision.json ↓	2.1 KB	2026-10-16 10:32
img/	7 items	2026-10-14 22:50
scripts/	9 items	2026-10-14 22:47
work/	12 items	2026-10-14 22:47

status.json in full

{
 "tm": "1RB0LA_1RC---_0LD1RD_0RA0RE_0RF1RC_1LF0LA",
 "label": "W7-6",
 "status": "CRYPTID_CANDIDATE",
 "stage": "wave7-stage1",
 "updated": "2026-10-14",
 "confidence": "med",
 "reason": "Stage 1 (W7-6) stopped by its stop rule. The counting phase is exact: at every C right record the word is a base-4 counter on pairs of 1-runs (23=0, 22=1, 33=2, 32=3, top digit 3) and each record adds 1 (10,416/10,416 random transitions, w = 2..40); it cannot halt while counting. Halting is possible only at phase events: overflow -> A erases the trail -> nested rebuild -> the new counter collides with markers / the old remnant. Synthetic scans show a collision halts only for an exact (value, gap) pair (w=3: V=49, gap 28 halts at 6,290 steps). The real orbit survived every event to 2.1e7; the current 23-pair counter (V = 61,170,343,443,693 at step 100,000,903, irregular high digits) overflows after ~9.2e12 increments, about 4.6e15 steps, trail ~1.8e13. Whether that transition halts is an exact big-number coincidence question: cryptid-like lottery, not settled. No nonhalting work (taken class, M-Abozaid SOTCv2.v).",
 "siblings": [
  {
   "line": 472,
   "tm": "1RB0LA_1RC---_0LD1RD_1RA0RE_0RF1RC_1LF0LA",
   "note": "distinct table (D0 1RA vs 0RA); same architecture by end tape (1^5408013 + ~30-cell counter at 1e9); qsim 0 rules; not modelled"
  },
  {
   "line": 569,
   "tm": "1RB0RD_1RC---_0LA1RA_0RE1RC_1LE0LF_0RC0LF",
   "note": "distinct table; same architecture by end tape (1^4591407 at 1e9); qsim 0 rules; not modelled"
  },
  {
   "line": 690,
   "tm": "1RB0LA_1RC---_0LD1RD_0RB0RE_0RF0LD_1LF0LA",
   "note": "distinct table (D0 0RB, E1 0LD); end tape 1^10536 0 1^2 0 1^5410013 at 1e9; qsim 0 rules; not modelled"
  }
 ],
 "family_note": "The four W7-6 lines are four different tables (canon over all starts, renaming + mirror), not starts of one table; no start-parametric argument applies. Line 33's table has no other start on the 740 list.",
 "template": "SOTCv2.v TM1 (M-Abozaid): applies partly (sweep/token lemmas fit the counting phase); nothing upstream covers overflow -> erase -> nested rebuild -> collision.",
 "checks": {
  "byte_exact_740": "line 33",
  "claims": "none before ours (claims.tsv); sheet: 'Has to halt in the counting phase'; no proof file names any of the 4 lines",
  "ledger": "query 33: parked 10-13 (halting-hunt, retry_if exact model with a margin); qsim/margin scouts negative",
  "qsim": "0 rules on 33/472/569/690 at 200,000 loops (work/qsim_*.jsonl)",
  "sim": "no halt to 1e9 on all four lines (work/sim1e9_*.jsonl)",
  "increment_rule": "scripts/validate_increment.py: 10,416/10,416 record transitions",
  "collision_scan": "scripts/collide_scan.py, scripts/overflow_scan.py, scripts/halt_orbit.py"
 },
 "next_goal": "If funded (2 h): exact phase-level simulator = R1 closed form (exact trail growth and step cost per increment, fitted then validated on random words) + run-length simulation of overflow/erase/nested rebuild/collision, validated against direct simulation to 2.2e7 (3 phase events); then run it through the overflow of the 23-pair counter (~4.6e15 steps) and report HALT (with step count, the C2-552/W5-5 checked-runner route) or the next phase's parameters."
}

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

1 contract warning

mechanism: 7 bullets (max 3; the card folds them under the summary)

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 1RB0LA_1RC---_0LD1RD_0RA0RE_0RF1RC_1LF0LA