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

`1RB0RD_0LC0RA_1LA1LC_1RE0LF_0RA1RF_1LB---`

W7-5local proof 32Claimed by someone elseSkelet 1-like Class 1bbchallenge ↗Explorer

How it was proved

How we proved it never halts

Exact base-4 counter on fixed digit words in a 100 sea; both starts follow one rule set; no halt to 1e16.

#32local proof number

530lines of Rocq

8 sto compile

–automatic checks

Claimed by someone else

We proved this machine locally, but our proof was still unsubmitted when we found it already covered upstream.

Submit completed proofs early. A local proof does not secure an upstream claim.

Upstream proof ↗ · Recorded timeline

What the timing evidence establishes

This describes upstream credit, not who first discovered the mathematics. The records do not establish adoption of our proof, first public push time, or whether an earlier submission would have secured credit.

Overview

In one sentence

Exact base-4 counter on fixed digit words in a 100 sea; both starts follow one rule set; no halt to 1e16.

Upstream: The blank-start machine never halts: PR_Sk1Class1.v.TM1 ↗. We also have a local proof. This upstream addition is separate from our merged submissions; adoption credit is not established.
Rocq proof: check_kill PASS · first Oct 14 23:08
530 lines · 24 KB .v · compile 7.6 s · coqchk pass · 0 axioms · PASS Oct 14 23:08
Class: Skelet 1-like Class 1ours: sheet Skelet 1-like Class 1 ≠ ours Base-4 counter: fixed 4-phase digit words in a 100 sea; births at the right end, a zero-field cluster at the left wall · high confidence
On the list: not on BB6_holdouts_663.txt (line 274 of the previous list) · historical 740 line 274 · observe.json rank #274
eqv ×1sim 1e15

Your calls on file 1

2026-10-14 · 2026-10-14-superseded: W7-5 (lines 274, 514) turned out to be a clean base-4 counter that needs neither W7-4's J law nor its wall table: start its stage 1 now, or keep waiting for W7-4's stage 1?

Mechanism

What to check here: the pictures show the mechanism that the rule table describes.

How it works: 3 notes

At every D-record the tape is 0^inf [1100] P(p1) s^f1 ... P(pk) s^R 100 D> 0^inf, s = 100, digit words P0 = 11001100, P1 = 110000, P2 = 1001100, P3 = 10000. One sweep adds 1 from the right: 3s wrap to 0 (moving 2 cells left), the first lower digit steps up in place. Fields follow from positions; R grows 6 per 4 sweeps.
Fields shrink 2 per cycle of their left digit and die; a digit whose field is 0 is pushed one word right instead of overlapping, so the oldest digits form a zero-field cluster at the left and keep counting. Overflows alternate the wall 1100 / none; every other one gives birth to a new digit P3 at the right end.
Lines 274 and 514 (start F, mirrored) enter the same language by step 108 / 792 and differ only in one field (+4). Exact sweep simulator (rules + step formula) = C core at 1e11 on both; no halt to 1e16 on either.

Figures for Checkpoint A

Fig 1 · Five counter sweeps, two carriesQ1
Each zigzag from the right edge is one sweep. Compare how far left each one turns before going back.

Fig 2 · Digit worldlines from blank to 1e9Q2
Each white line is one digit. Find where new lines start at the right edge; follow them left.

Fig 3 · Births at the right edge
Rows are new rightmost cells (4 per sweep). Look for dark lines starting at the right edge.

More figures (2)Fig 4–5: Default view, first 10,000 steps · Line 514, default view

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(p) s^R 100 D> (p = 0, 1, 2) ⟶ P(p+1) s^(R+2) 100 D> (R+1 for p = 1)	p = 0, 1, 2; the digit stays in place	8R + 32 (p = 0, 2) or 8R + 76 (p = 1)	✓215658/215658
R2 carry	P(q) s^f P(3)^j-chain s^R 100 D> (q < 3) ⟶ P(q+1) s^(f - [q=1]) P(0)^j-chain s^(R+1) 100 D>	each wrapped digit moves 2 cells left and its right field loses 1; q = 1 also costs its right field 1	8(R + fields crossed) + 52 per wrapping digit + 32 or 76 (stop digit q = 1) + 20 per push word	✓72019/72019
PUSH (zero field)	P(a) s⁰ P(b) with the field due to go to -1 ⟶ P(a') s⁰ P(b') with P(b') one word further right; its right field pays 1	cascades through runs of zero fields	+20 per pushed word	✓3156/3156
O1 overflow, wall leaves	0^∞ 1100 P(3)...P(3) s^R 100 D> ⟶ 0^∞ P(0)...P(0) s^(R+1) 100 D> (after pushes)	k digits, any fields	8(R + all fields) + 52k + 32 + 20 per push word	✓2858/2858
O2 overflow, wall + birth	0^∞ P(3)...P(3) s^R 100 D> (R >= 2k+2) ⟶ 0^∞ 1100 P(0)...P(0) s^R' P(3) s² 100 D> (every digit 2 more cells left)	k digits, any fields; R' = R + 1 - push words	10(R + all fields) + 50k + 101 + 20 per push word	✓2315/2315

Compressed historythe tape as overflow outputs: 0^∞ [wall] P(p1) s^f1 ... P(pk) s^R 100 D> 0^∞ (274, exact sweep simulator) at 23 moments: where the rules are read off

overflow outputs: 0^∞ [wall] P(p1) s^f1 ... P(pk) s^R 100 D> 0^∞ (274, exact sweep simulator)

step	`event`	`digits`	`wall`	`cluster digits`	`nonzero inner fields`	`R`
477	O2	2	1,100	1	3	2
2,529	O1	2	none	1	1	21
7,910	O2	3	1,100	2	41	2
39,426	O1	3	none	2	31	93
119,447	O2	4	1,100	2	20 187	2
611,635	O1	4	none	2	10 155	381
1,874,600	O2	5	1,100	3	122 763	2
9,688,076	O1	5	none	3	80 635	1,533
29,808,277	O2	6	1,100	3	37 507 3067	2
154,568,141	O1	6	none	4	374 2555	6,141
476,169,214	O2	7	1,100	4	203 2043 12283	2
2,471,212,970	O1	7	none	4	33 1531 10235	24,573
7,615,621,471	O2	8	1,100	5	881 8187 49147	2
39,531,956,819	O1	8	none	5	199 6139 40955	98,301
121,837,780,040	O2	9	1,100	6	3607 32763 196603	2
632,482,087,556	O1	9	none	6	877 24571 163835	393,213
1.94·10¹²	O2	10	1,100	7	14525 131067 786427	2
1.01·10¹³	O1	10	none	7	3603 98299 655355	1,572,861
3.11·10¹³	O2	11	1,100	8	58211 524283 3145723	2
1.61·10¹⁴	O1	11	none	8	14521 393211 2621435	6,291,453
4.99·10¹⁴	O2	12	1,100	9	232969 2097147 12582907	2
2.59·10¹⁵	O1	12	none	9	58207 1572859 10485755	25,165,821
7.98·10¹⁵	O2	13	1,100	10	932015 8388603 50331643	2

eventlast O2

not plottable

digitslast 13

walllast 1,100

cluster digitslast 10

nonzero inner fieldslast 932015 8388603 50331643

Rlast 2

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

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

file: Sk1Machines.v:8
module: Sk1Counter / Sk1CounterMixed
machine: —
diff: W = 100 here; digit words of 8/6/7/5 cells; wraps shift 2 cells; zero-field pushes; O2 extra pass
note: Same take/give/carry digit-counter shape with fixed-size digit words, but the 2-cell wrap shift needs a re-cut of the words, the Sk1 batch rule excludes zero-field pushes, and the O2 overflow adds a full extra pass. Closest own kills: #30/#7 counter route; W7-4 shares the sea and the wall/birth cycle but not the digit law.

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

One closed-language proof: sea-crossing lemmas, 4-phase digit lemmas (stop/wrap), a push lemma by induction over zero-field runs, the two overflow lemmas, and an invariant giving R >= 2k+2 at every O2; then entry lemmas for 274 (108 steps) and 514 (792 steps).

▲The push cascade and O2's extra pass need inductive segment lemmas; that is new formal work beyond Sk1CounterMixed.
▲The domain condition (room at O2) counts, so a pure regular-language certificate is unlikely without extra structure.
▲Scoop risk: Skelet 1-like Class 1 is mxdys's mined class (Sk1Machines.v TM1..TM105 list).

Stats & provenance10¹⁶ steps simulated · 642,934 cells · the status in full · files

simulated: 10¹⁶ steps
tape: 642,934 cells · 214,315 nonzeros
growth: direct C core: span 73,697 at 1e9 and 642,933 at 1e11 (274); exact sweep simulator: no halt to 1e16 on 274 and 514 (56.4 million sweeps, 13 digits, span 225,496,005); one new digit per two overflows
status now: Checkpoint B review: sound, 5 minor gaps, all fixed (proof.md section 11): S0 sentence corrected; O2 field law derived in 4.3 (gap rule g_1-1, g_2..g_(m-1), g_m-1, or g_1-2 if m=1); r' = rest of r + 2 covers RA2/RA3/L5e; 5.2 (D2) split into m>=2 / m=1; notes.md 514 counts corrected. proof.md (start-parametric, lines 274 and 514): 14 pass lemmas (S0, L1-L7, RA1-RA3, RE1-RE2) proved for all exponents by symbolic execution from six shift rules; the sweep is their composition, exact against the machine on 80k in-domain configurations; invariant B(k;f) with f_(k-1) >= (4^k-4)/3, epoch theorem B(k) -> B(k+1) in 2*4^k-3 sweeps with newborn field 3*4^k-5 (or -6) >= (4^(k+1)-4)/3; openings 274 blank -> B(3; 0,41) at step 7,910, 514 (start F mirrored, phi) -> B(2; 7) at step 792. check_proof.py: 82 checks, 0 failures, ~7 s. Not a kill until tools/check_kill.sh PASS. (status.json, 2026-10-14)
observer's note: Observe done: exact base-4 counter, rules validated (real 36.8k sweeps, 12k random, exhaustive small), sweep simulator = C core at 1e11 on both starts, no halt to 1e16. Stage 1 waits on the W7-5 stop rule (decision.json).
files: observe.json · notes.md · proof.md · status.json · 1RB0RD_0LC0RA_1LA1LC_1RE0LF_0RA1RF_1LB---.v

Proof & checks

Blank-start proof verified; the required independent audit is complete. Submission packaging remains.

Rocq proof · Independent audit · Gate and kernel-check receipt

Files

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

name	size	changed
notes.md ↓	13 KB	2026-10-14 22:38
proof.md ↓	27 KB	2026-10-14 22:37
status.json ↓	2.5 KB	2026-10-14 23:10
observe.json ↓	12 KB	2026-10-14 21:13
1RB0RD_0LC0RA_1LA1LC_1RE0LF_0RA1RF_1LB---.v ↓	24 KB	2026-10-14 23:03
decisions/	1 item	2026-10-14 22:09
img/	5 items	2026-10-14 21:02
proof_scripts/	3 items	2026-10-14 22:09
rocq/	7 items	2026-10-14 23:10
scripts/	11 items	2026-10-14 21:06
submission/	2 items	2026-10-14 23:07
work/	23 items	2026-10-14 21:08
check_proof.py ↓	35 KB	2026-10-14 22:35

status.json in full

{
 "tm": "1RB0RD_0LC0RA_1LA1LC_1RE0LF_0RA1RF_1LB---",
 "label": "W7-5",
 "status": "CHECKPOINT_B",
 "stage": "informal_proof",
 "updated": "2026-10-14",
 "confidence": "high",
 "holdout_line_740": 274,
 "reason": "Checkpoint B review: sound, 5 minor gaps, all fixed (proof.md section 11): S0 sentence corrected; O2 field law derived in 4.3 (gap rule g_1-1, g_2..g_(m-1), g_m-1, or g_1-2 if m=1); r' = rest of r + 2 covers RA2/RA3/L5e; 5.2 (D2) split into m>=2 / m=1; notes.md 514 counts corrected. proof.md (start-parametric, lines 274 and 514): 14 pass lemmas (S0, L1-L7, RA1-RA3, RE1-RE2) proved for all exponents by symbolic execution from six shift rules; the sweep is their composition, exact against the machine on 80k in-domain configurations; invariant B(k;f) with f_(k-1) >= (4^k-4)/3, epoch theorem B(k) -> B(k+1) in 2*4^k-3 sweeps with newborn field 3*4^k-5 (or -6) >= (4^(k+1)-4)/3; openings 274 blank -> B(3; 0,41) at step 7,910, 514 (start F mirrored, phi) -> B(2; 7) at step 792. check_proof.py: 82 checks, 0 failures, ~7 s. Not a kill until tools/check_kill.sh PASS.",
 "siblings": [
  "1RB---_0RC0LD_1RD1RC_1LB0LE_1LF0RA_0LD1LA"
 ],
 "sibling_note": "Line 514 is start F of the same table, mirrored. It enters the same language at step 792 (274 at step 108) and then follows the same rules with the same counter value; only one field differs (+4 words), and that offset moves into the next field whenever the cluster absorbs a digit. One closed-language proof plus two entry lemmas covers both lines.",
 "upstream": "No upstream proof of either start. verify/Sk1Machines.v (mxdys) Sk1Counter/Sk1CounterMixed applies only partly: same digit-counter shape, but wraps move a digit 2 cells (re-cut), consumption reaches through empty fields (outside its batch rule), and O2's E-pass/birth is a second kind of visit; proof.md 9.1.",
 "next_goal": "Formalize (proof.md section 9.2): shift rules + pass lemmas in Individual62 style, abstract sweep with domain option, epoch invariant by induction on t (lia/nia), openings by solve_init (274: 7,910 steps) and flip_halts/perm_halts + 792 steps (514).",
 "formal": {
  "file": "1RB0RD_0LC0RA_1LA1LC_1RE0LF_0RA1RF_1LB---.v",
  "sha256": "1dec277e5a7d867f...",
  "check_kill": [
   "PASS formalizer round 1 2026-10-14 23:03 (rocq/check_kill_r1.txt, coqchk pass)",
   "PASS orchestrator 2026-10-14 (rocq/check_kill_orchestrator.txt)"
  ],
  "pending": "independent audit agent, then status KILLED_NONHALT + submission bundle; line 514 needs its own delta file (rocq/log.md, Open)"
 }
}

Rendered 2026-10-16 13:29 by tools/machinepage.py from status.json, observe.json (the card), the kill files (tools/killreview.py) and the dashboard records · rebuild: python3 -B tools/card.py 1RB0RD_0LC0RA_1LA1LC_1RE0LF_0RA1RF_1LB--- (the kill review: python3 -B tools/killreview.py 1RB0RD_0LC0RA_1LA1LC_1RE0LF_0RA1RF_1LB---, which also renders a derived kill's same-machine pictures)