1RB1RA_1LC1RE_---0LD_1LE1LD_0RA0LF_1LF0LB

Status: CRYPTID_CANDIDATE (confidence med: mechanism exact, no non-halting argument) Class guess (agent / Dennis): Bouncer + Chaotic Edge; exact mirror twin of #5 1RB1RA_0LC0RF_1LD1LC_1RE1LB_---0RA_1RF0RD / ? Spreadsheet notes / Discord thread: - On the 778 list, line 427, byte-exact (tools/holdouts.py contains). - Results row 901 says "Bouncer + Chaotic Edge" and Level 0 row 153 says "Chaos + bouncer". Neither row has a status, notes or claim. - Discord: the machine appears only on mxdys's 2026-08-24 UBRRBA_TODO list (data/discord/2026-08-24_mxdys_ubrrba_86.txt, line 81). That list is fair game. - No byte-exact or equivalent proof exists in verify/. Viewer: https://bbchallenge.org/1RB1RA_1LC1RE_---0LD_1LE1LD_0RA0LF_1LF0LB

Observation

• The twin is #5, exactly. σ(mirror(#5)) equals #26's transition table cell for cell, where mirror swaps L and R and σ renames the states A,B,C,D,E,F to D,E,A,B,C,F (work/ check, printed True). The two machines differ only in the start state: #26 starts in σ(C), not σ(A). That is why holdouts.py solved (equivalence with fixed start A) does not pair them.
• Same trajectory. Bounce k is the k-th new left record of #26 and the k-th new right record of #5.
• For every k ≥ 2, #26 is at 0^inf <E 1^n w 0^inf at step t, and #5 is at 0^inf rev(w) 1^(n+1) B> 0^inf at step t + 2k exactly.
• This held at all 102,240 bounces k = 2..102,241, i.e. to 1e10 steps (work/lockstep.c, work/lockstep_1e10.txt). Bounce 1 is the only difference: there #26 is in D, a start transient.
• So #5's block is one cell longer. The extra cell costs 2 steps per trip (walk there and back), which is the 2k.
• Twin scan. I ran all 778 holdouts to 1e8 steps (work/twinscan_778_1e8.txt) with the targeting detector's tolerances (width within 0.3% + 3, nonzeros within 0.5% + 3). Only #5 matches: 10,414 cells, 10,027 nonzeros for both. The next nearest is about 3% off.
• At 1e9: no halt; span 32,607 (lo −32,263, hi 343), 31,699 nonzeros, block 1^30,399 on the left, edge w = 2,206 cells on the right. At 1e10: no halt; 102,241 bounces.
• Per-bounce stats (work/sweeps.c, work/sweeps_1e9.txt, 32,262 bounces to 1e9):
• Erosion is 0.0577 block cells per bounce on average. The maximum is 11 in one bounce (bounce 13,759); window maxima are 27 per 8, 46 per 32, 79 per 128 and 204 per 1,024 bounces.
• The maximum dive depth is 889 cells.
• The block was 1 cell at bounces 2–7 and 2 cells at 8–11 and 15–17. It has been ≥ 29 cells since bounce 31 and ≥ 33 since bounce 41.
• These are #5's numbers shifted one bounce (#5 has the extra first record).
• Tools:
• qsim found block size 2 and 0 prover rules (200k loops, step 2.45M; work/qsim.jsonl).
• compress track found 300 skeletons in 300 snapshots, so there is no stable skeleton for w (work/compress_track.txt).
• I skipped rulefit: the edge has no affine exponent structure, and on #5 all 16 fitted rules died.
• Diagrams (img/, script img/src/figs.py):
• default_site.png (+ viewer.html)
• twin_vs_5_mirrored.png is the key figure: #26 next to #5 mirrored, with the differing cells in red. Only the wall cell differs, from bounce 2 on.
• edge_every4e5_1e9.png
• closeup_bounces54-57.png (Explore colours)

Candidate rules

Notation is wiki directed-head; x and y are arbitrary words. Each rule is the mirror image of a #5 rule under σ: #5's C (the diver) is #26's A, and #5's A (the walker toward the wall) is #26's D. I validated every rule with tools/sim.py on 60 random instances (random x, y, k, n, j), all 60/60 (work/validate_rules.py, work/validate_rules.json).

• Case split.
• A reading 0 sees one of the right contexts 00, 010 or 011, so T, Ca and Fo cover it completely.
• D reading 0 with no 00 on its left sees one of 1110, 11010, 10110 or 101010 (E1, E2, P1, P2), or the wall (bounce).
• Between rules, A walks right over 1s and D walks left over 1s.
• B, C, E and F occur only inside rules.
• Halting door. It is the only route to the halting transition C0: D0 → E1 → F0^j → F1 → B0 → C0.
• Invariant: the cells from the leftmost 1 to head−1 never contain 00.
• I checked it at every step from the blank tape to 1e9 with work/inv00.c: 0 violations.
• Its sanity variants fail as they should: the region widened by 1 cell gives 23,551 violations in 1e6 steps, and widened by 2 gives 84,719.
• A brute-force Python rescan (work/inv00_brute.py) agrees exactly on 3e4 steps: 0 / 1,664 / 6,078.
• It is the mirror of #5's no-00 invariant, which has a local proof (#5 notes).
• Consequence: #26 halts only via 0^inf 1 1 0 <D or 0^inf 1 0 1 0 <D, that is, only if the edge eats the block down to 2 cells (j ≤ 1 by the invariant).
• Twin map (see Observation): checked 102,240/102,240. Why it holds for all time:
• the tables are identical under σ∘mirror;
• the configurations agree at bounce 2 (with block n+1 for #5);
• the block length only changes the walk time, as long as the rules never reach the wall end of the block. That is #5's wall-model condition n ≥ e+3; here n ≥ 33 and e ≤ 15 after bounce 40.

Cryptid check (ground rule 6)

• 26's edge is the same object as #5's edge: the same word, mirrored, at every bounce. So every result in #5's research/erosion.md applies verbatim:

• no deterministic erosion bound;
• potential and regular-language certificates fail by 5–12×;
• the edge has about 0.63 bits/cell of entropy and is not substitutive.
• Dennis flagged #5 as CRYPTID_CANDIDATE on 2026-10-10 on that basis.
• Verdict: CRYPTID_CANDIDATE, stopped before proof work.
• Side result, inferred, not computed separately here: #5's exact wall-model run found no halt in its first 1e8 bounces (about 9.6e15 steps). The run never had a block below 33 after bounce 40. #26's block is one cell shorter and still far from 2, so #26 does not halt in its first ~1e8 bounces either.

Template check

• verify/Bouncer_v3.v TM1 (1LB1RA_0RA0RC_---1RD_1RE1RB_1LF0LE_0RD0LE):
• It needs an eventually periodic side: RC i pumps the exponents 363+128i and 1+3i.
• One BigStep is 128 bounces, checked by vsideRLs_es_spec + native_check_eq. The block side uses sideRLs_wall.

• 26's block side would fit that wall lemma, but its edge side is aperiodic, so no RC i exists. Does not apply.

• InfiniteRect_v1.v (eventually periodic boundary-token sequences) and LongNv1.v (explicit segRLs_n exponent patterns) assume the same regularity. Do not apply.

Checkpoint A (Dennis)

(pending; non-blocking questions on the card; decision.json asks park vs shared rule reduction)

Informal proof

Not started: cryptid candidate.

Formalization log

—

Outcome

CRYPTID_CANDIDATE (2026-10-10), shared with twin #5. If an erosion bound is ever proved for #5, it transfers through σ∘mirror plus the bounce-2 correspondence. That would give 2 kills from one proof.

Decision (2026-10-10, auto-applied)

Question: #26 is #5 mirrored with renamed states (same edge at every bounce): park it with #5 as one cryptid candidate, or fund the shared Rocq rule reduction now? Answer: park_with_5 (Park with #5 as one cryptid candidate). 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. Parked 2026-10-10 with #5 (auto-applied recommendation): exact mirror twin of #5, same cryptid call.

Rule reduction (2026-10-12)

This is not a kill. Status stays CRYPTID_CANDIDATE. The proof is shared with #5, Part 5 of machines/1RB1RA_0LC0RF_1LD1LC_1RE1LB_---0RA_1RF0RD/rocq/rule_reduction.v. It compiles in 1.9 s against unmodified busycoq, with no Admitted or Axiom, and its assumptions are functional_extensionality_dep only (baseline). - Proved: the twin's local rules, directly on tm26 with es: the walks (A right, D left), the bounce 0^inf 1^n <D y -> 0^inf 1^(n+1) A> y, T, Ca, Fo, E1, E2, P1 and P2, exactly as in the table above. - Proved: the transfer. - perm_twin : Perm tm26 (flip tm5) sigma, with sigma = A->C, B->D, C->E, D->A, E->B, F->F. So #26 from blank is #5's table, mirrored, started in C on the blank tape. - Through busycoq's perm_nonhalt, flip_halts and flip_involutive, #5's invariant and door analysis carry over. - Stated as open: erosion_open (C;; tape0) for #5's table, a Definition that is not proved. It says the edge never eats the block down to 2 cells. - Proved: - reduction_twin : erosion_open c0_twin -> ~ halts tm26 c0 - nonhalt_twin_iff_erosion_open : ~ halts tm26 c0 <-> erosion_open c0_twin - See #5's notes, "Rule reduction (2026-10-12)", for the invariant (including the extra D clause) and what remains open. - Also proved for the twin in #5's rocq/reduction.v (2026-10-12): reduction_twin : EdgeNeverEats a0_twin -> ~ halts tm26 c0 and reduction_twin_iff, on the 7-rule system, closed under the global context (no funext). See #5's notes, "Rocq rule reduction (2026-10-12)".