1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF

Status: KILLED_NONHALT (check_kill PASS, independently re-verified, packaged in submission/, 2026-10-13; Discord draft not posted). Earlier: CHECKPOINT_B, proof.md complete, skeptic round 1 passed Label: W5-8 (740 list line 214) Class guess (agent / Dennis): sheet "Bouncer + Chaotic Edge". Ours: a bouncer whose right edge is a 4-particle system with a closed double-cycle law. The edge is not chaotic. / Dennis: (open) Spreadsheet notes / Discord thread: no claim. It is on mxdys's UBRRBA_TODO (data/discord/2026-08-24_mxdys_ubrrba_86.txt, line 86), a list of holdouts that are easy to accelerate. The sheet gives only the class. Viewer: https://bbchallenge.org/1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF

Observation

Table: A0 1RB, A1 1LD; B0 0RC, B1 1RC; C0 1LA, C1 1RE; D0 halt, D1 1LE; E0 1RF, E1 0RC; F0 0RB, F1 0LF. It halts only if A reads 1 with a 0 to its left (A1 -> 1LD, then D reads 0).

• A bouncer. Every round trip goes from the left end to the right end and back. lo moves exactly -2 per trip, and hi about +2.05. The span grows like 1.07 sqrt(steps): 34,041 cells at 1e9 and 107,321 at 1e10 (26,506 trips).
• Left end. A fixed gadget G (44 cells; corrected in proof.md: 43, the 44th is the head cell). At the first left record of every trip the tape starts with 0^inf <F G, where G = 0^2 1^2 0 1^4 0 1^2 0 1^6 0 1^2 0 1^5 0^2 1^2 0 1^5 0 1^2 0^2. Each trip has two left records, about 151 steps apart.
• The sea. Everything right of G is a sea of 1s, with a few gaps (particles) in it.
• The right pass rewrites C> 11 -> 10 C>.
• The left pass undoes it with a moving 3-cell composite, 10 11 C> 0 -> 11 C> 0 11 (or 10 B> 000 -> B> 000 11 on the other trip phase; corrected in proof.md: this needs a 0 on the left, 0 10 B> 000 -> 0 B> 000 11), 12 steps per pair.
• So at left records the sea is 1^(2k); at right records it is (10)^k.
• Particles. Seen at left records, measured from hi, there are four.
• The wall W (0) and the edge E (0110 0110) stay fixed relative to hi (they move +2 per trip in absolute terms).
• The fast particle P1 (0110) moves 8 cells left of hi per 12 trips.
• Two slow particles, Q (0^6) and Q' (0110 1111 0^6), move 4 cells per 12 trips.
• Each particle cycles through 12 shapes with period 12 trips. At the phase-0 trip of a run the tape is exactly K(n,a,b,c,d) = 0^inf <F G 1^n 0 1^a 0110 1^b 0^6 1^c 0110 1111 0^6 1^d 0110 0110 111 0^inf (written with explicit exponents: 1^n 0 1^a 0 1^2 0 1^b 0^6 1^c 0 1^2 0 1^4 0^6 1^d 0 1^2 0^2 1^2 0 1^3).
• Collisions. When P1 reaches W, about 138 or 147 trips of rearrangement follow, of two kinds that alternate (Fig 2). Each kind restarts the steady pattern with the parameters shifted linearly.
• Pictures (img/):
• default_site.png: the site view.
• double_cycle_E0.png: diagram.py records:L --frame right, from the exact tape at step 153,126,993 (work/E0.cfg).
• edge_overview_1e10.png: our C recorder (scripts/rsim.c) plus diagram.py's PNG encoder, one row per 12 trips to 1e10.
• default_1e5.png.

Candidate rules (all validated by simulation from constructed tapes; scripts/)

The step formulas are exact (an exact least-squares fit over all instances, residual 0).

Double cycle. Let Even(n,x) = K(n, x, (x+76)/2, 35, 18) with x = 4 mod 8, x >= 52 and n odd.

Even(n,x) --S^((x-4)/8)-->  K(., 4, x+36, 35, (x+32)/2)
          --TE-->           K(., x-50, 82, (x+134)/2, 18)        = Odd
          --S^((x-52)/8)--> K(., 2, (x+112)/2, (x+134)/2, (x-16)/2)
          --TO-->           Even(n+12x+808, x+32)

This takes 3x+201 round trips. It was validated for every x in 52..252, for 16 random x up to 5,620 (n random odd), and against all 16 even-run starts of the real run to 1e10 (x = 212, 244, ..., 692). Data: work/run_starts_K.tsv.

The general two-parameter map is (x,y) -> (3x/4 + y/2 + 13, x/4 + y/2 + 35). It keeps the line x - 2y = -76 and attracts nearby points to it. Both families, start A (x = 212 + 32j) and start E (x = 220 + 32j), lie on that line.

Opening. From blank, the first left record of trip 3,209 (step 153,126,993) is exactly Even(12863, 212). The earlier even-run starts lie off the line (u = x - 2y = -96, -88, -84, ...) and follow other residues, so the law starts here.

Siblings (same table, canon checked). - 740 line 418 = this table from C, mirrored. Run from C it reaches Even(12857, 212) at step 153,013,640, shadowing A's run with n 6 smaller. - 740 line 636 = from E, not mirrored. It reaches Even(13299, 220) at step 163,638,058 (its own x = 220 + 32j family). - Starts B and F fall into the C run after 1-2 steps.

Cryptid check (ground rule 6). Not a cryptid. The cycle map is affine, all parities are fixed (n odd, x = 4 mod 8), and no branch depends on the digits of a growing number. A non-halting proof is in sight: S, TE and TO are exact runs that cannot halt, and Even(x) -> Even(x+32) repeats forever.

Template. The nearest proved table by transitions is 1RB0LA_1LC1RD_0RB0LC_1LA1RE_1LF0RD_---1LE (distance 3, RWL_mod_v5.v, a decider certificate with nothing to reuse). The architecture template is TranslatedBellv5.v TM1: - ES_v3 es' proves block macro rules with 4-6 variables, ind repeats them, follow chains them, and progress_nonhalt_cond ends the proof. - Bouncer_v2.v TM1 shows es' n doing a whole bouncer BigStep. - Bouncer_v3.v's multistep_c' (nested small counters) is how to run a long opening; our 153M steps is 11x the largest stepn in busycoq. - ES_v3 finds shift rules with a carried context of up to T cells. The R2a composite needs a 3-cell context (<E 111). try_sr tries contexts of growing length, so it should find it, but that is untested.

Checkpoint A (Dennis)

(open)

Informal proof

2026-10-13: proof.md complete, status OPEN (Checkpoint B pending, non-blocking). check_proof.py checks every claim. - The observe-stage rules are proved for their whole domains by a symbolic executor (scripts/symexec.py) using only R1 and R2b; R2a is not needed. - Corrections: R2b needs a 0 left of the crossed copies (0 10 B> 000 -> 0 B> 000 11); G has 43 cells; trips 3, 6, 9, 12 of S turn at the first particle, so not every trip reaches the right end. - New rules for the opening: T6 K(n,6,b,c,d) -> K(n+592,b+c-91,d+62,35,18) and T8 K(n,8,b,35,d) -> K(n+540,b-74,86,d+47,18). With them the opening is 4,097,897 direct steps plus 20 macro steps (proof.md 5), not 153M direct steps. - Lemma plan for Rocq: proof.md 8 (half-length family Kr, Ev N X; main risk is whether es_v3 finds R2b). 2026-10-13, skeptic round 1: sound, 4 minor gaps, all fixed; status CHECKPOINT_B. - proof.md Appendices A and B: TE and TO trip by trip (from scripts/phases.py); check COL re-proves every row. - The d split of S is an executor artefact (rotation y (v y)^X = (y v)^X y avoids it). - proof.md before section 9 is lint-clean (0 errors, 0 warnings): the starting point for submission/proof.md. - check_proof.py 196/196 PASS (seeds 1, 2 default; seed 1 --full).

Formalization log

2026-10-13, round 1: check_kill PASS (exit 0) on 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF.v (361 lines, sha256 beef54a5...cf48): compile 6.5 s native, coqchk pass 45.1 s, 0 assumptions. Not yet independently re-verified; no submission package yet. - proof.md §8 went through as planned: S, TE, TO, T6, T8 are one es' each (no case split; es' finds the shift rules itself), S_iter by induction, DC by four follows, the 20 opening rows by follow, progress_nonhalt_simple on (N, X). - Only change to the plan: the 4,097,897-step opening is cut into six direct runs at left records (LR W1..W5), because coqchk re-checks a single 4.1M-step VM cast by lazy conversion and ran out of memory under the 8 GB cap. Details: rocq/log.md.

Outcome

Never halts: check_kill PASS on the .v (round 1). Pending: independent re-verification and packaging (submission/).

Files

• check_proof.py (proof.md 9); scripts/symexec.py (symbolic executor), scripts/krun.c (batch C runner, built to work/krun), scripts/phases.py (writes work/phases_*.txt; the TE and TO tables are proof.md Appendices A and B).
• scripts/: kcheck.c (run a constructed tape, print the tape at given left-record counts); parseK.py; kval.py; val_all.py (S/TE/TO validation and step fits); lawcheck.py (double cycle); trans_probe.py; rsim.c (right-edge recorder, one row per trip); dump.c (full tape at given trips); render2.py; tm.py.
• work/: E0.cfg, run_starts_K.tsv, val_.txt, _probe.txt.

Kill

2026-10-13: KILLED_NONHALT, independently re-verified and packaged. - Audit (independent agent): check_kill --json PASS, exit 0 (2026-10-13T12:20:42Z; 17/17 sub-checks, compile 6.7 s native, coqchk -norec pass 44.9 s, busycoq 0940bb9 = pin); string byte-exact at 740 line 214; .v read end to end (361 lines, sha256 beef54a5...cf48), no axioms/sections/modules/Opaque/Extract, Ltac ES_v3.es_v3_pre ::= unfold Kr, G. is a tactic hook only; house-style header OK; Print Assumptions nonhalt closed. - Fresh check_kill for the package (2026-10-13T12:23:55Z): PASS, exit 0, compile 6.6 s native, coqchk pass 44.9 s, 0 assumptions. The .v is unchanged (same sha256), so no new compile was needed. - submission/: the .v (verbatim copy), proof.md (public write-up: header with template and .v map, sections 0-7 as in the working proof.md minus check names and process notes, a new section 8 describing the finished Rocq proof, Appendices A and B verbatim; writeup_lint 0 errors, 0 warnings), check_kill.txt (fresh run, local paths replaced by placeholders), README.md, discord.md (1,634 characters without the link; not posted; fill in , search #bb6 first; mxdys's UBRRBA to-do list is not a claim). - Siblings 740 lines 418 / 636 (same table from C mirrored / from E) are not formalized; they need only their own openings plus Perm/flip (proof.md 7.3).