1RB0RF_1LC0RD_1LA0LD_1LE0RA_0LB---_0LB1RB

Status: SKIPPED (2026-10-14). The CTLv1.v certificate port is refuted at the level of upstream's invariant, as for P-728. The machine and its twin run in lockstep, but upstream's certificate does not contain the condition that keeps them in lockstep. No delta proof.md exists.

Label: P-385 (strategy direction 1, twin ports). 740 line 385, byte for byte. Sheet class: Monotone list. Line 173 has the same table from another start.

Checks: scripts/twin_check.py gives SUMMARY PASS with --long (7 checks, including the 2e9-step run C; output scripts/twin_check.out). Build the native probes first with scripts/build.sh.

The relation

385   = 1RB0RF_1LC0RD_1LA0LD_1LE0RA_0LB---_0LB1RB
twin  = 1RB0RE_1LC0RD_1LA0LD_1LE0RA_0LB0LF_0RA---   (CTLv1.v nonhalt16856)
twin2 = 1RB0RE_1LC0RD_1LA0LD_1LE0RA_0LB1LF_1RC---   (CTLv1.v nonhalt18273)

Upstream proves both twins with the same call, solve_cert (CPS_LRU 1001 100000 100000 2 3200 2 2 0 0). That is a CTL62 decider certificate, not a hand proof.

• Same start A, no mirror. States A to D are identical except where A1 goes (385: F, twin: E).
• The twin's E is entered from two places: D0 (1LE) and A1 (0RE). 385 splits it:
• 385's E is the twin's E entered by D0;
• 385's F is the twin's E entered by A1.
• The twin's F is entered only by E1.
• On a 0, all three behave the same: E0 = F0 = twin E0 = 0LB.

The F branch: exact merge

Let F read 1 at cell p with t[p-1] = 0. Then both machines end with B at p+1, t[p-1] = 0, t[p] = 1, and every other cell unchanged (check M, all windows). Only cells p-1 and p are read.

With t[p-1] = 1 the twin halts. Upstream proves the twin never halts, so this case never occurs in the twin's run. The shortcut is therefore exact on every reachable configuration.

The E branch: the reconvergence condition

E is entered by D0. Say D reads 0 at cell p and writes 1, so E reads t[p-1]. - t[p-1] = 0: both run E0 0LB. No split. - t[p-1] = 1: 385 halts at its second step. The twin halts too if t[p-2] = 1. If t[p-2] = 0 it runs on (check X, 512 tapes, 12 steps, no halt).

So 385 is the twin with one extra halting route:

P: whenever D reads 0, the cell on its left is 0.

385 never halts if and only if the twin's run satisfies P. Two remarks narrow P down: - D0 entered by B1 (0RD) always has a 0 on its left, because B just wrote it. - So P only concerns C1 (0LD): C reads 1 at cell q, and t[q-1] = 0. P says t[q-2] = 0 as well.

P holds in simulation

• 1e6 steps (check L): after replacing each twin E1 F0 A0 by 385's F1, the (state, position, read) sequences are equal. That covers 43,782 F1 shortcuts and 152,318 D0 events, with no D0 seeing a 1.
• 2e8 steps of each machine in C (scripts/bin/d0ctx): no D0 sees a 1. That is 3.0e7 D0 events for 385 and 2.8e7 for the twin. About 1 in 7 is entered by C1, and 99.86% of those see 0 1 1 0 on the left (t[p-1..p-4], D at p).
• 2e9 steps of each machine (logs/d0ctx_2e9.log, check C): no D0 sees a 1, over 3.04e8 D0 events for 385 and 2.80e8 for the twin. The context counts scale with the run; no new context appears.

Upstream's invariant does not contain P

Upstream's certificate is the closed configuration set of busycoq's CTL saturation (CTL.v, module CTL with the CPS_LRU context): - the tape is cut into 2-cell blocks; - each side is a DFA state that remembers the 2 nearest blocks exactly, then an LRU list of at most 2 further block ids.

It was replayed natively with the extracted decider (scripts/bin/ctlx, check U):

Split-state probe (check S). The twin is run on a 7-state context in which the state entered by D0 is a copy G that halts on reading 1 (D0 -> 1LG, G = 0LB---). - Calibration: the twin padded with an unused 7th state is still proved. - The split twin is not proved. The same holds for twin2.

scripts/bin/ctltrace7 steps the saturation one CTL step at a time. The split twin fails at step 852 of 26,893 (the full twin closure):

left side (DFA state 8), in tape order:  ...(LRU: 10, 01) 00 01 | 01 <C
exact part: blocks 00 01 next to the block 01 that C enters
C1 0LD, D0 1LG, then G reads the right cell of block 01: a 1

So the closed set contains the configuration ... 0 1 0 1 <C. In it, C reads 1, D reads 0 with a 1 on its left, and the D0-entered state then reads that 1. This is exactly a P-violation. In the twin it is harmless (E1 0LF, F0 0RA, ...).

385 under the same call fails at the same pattern: C< reads block 0 1, D0, then E reads a 1 and halts. twin2's split fails the same way, at step 4,151.

In the real run this window never appears: at every C1-entered D0 the left context is 0, never 1 0. The CTL abstraction over-approximates, and its extra configurations include P-violations. The upstream argument therefore does not apply to 385 from any opening. Porting needs a strictly finer invariant, one that proves P.

Searches on 385 itself

Extracted CTL62 deciders on 385 directly (scripts/grid.py, two workers), logs/grid385.jsonl. The cap was 8 s per run (20 s for the first 327 CPS_LRU runs). The whole grid was capped at 50 minutes.

No configuration closes. The timeouts are mostly larger blocks (bsz 3 and up) with long histories. mxdys's own sweeps left this line a holdout, so this was a cheap check, not a promising route.

Formalization route

No port route exists. - Copying CTLv1.v's call, or importing nonhalt16856, gives a theorem about the twin. It would still need a proof of P, and P is equivalent to 385's own non-halting. - nonhalt16856 depends on CTL62 (PArray/Uint63), which the unchanged check_kill baseline rejects. Any CTL-format certificate would go through Astra's package instead. - No Perm or Flip is involved. The states are renamed only in the sense of the split (385's E and F both map to the twin's E). The start is A, and no new opening is needed.

A kill needs either of these: 1. A regular invariant for 385 itself that excludes 0 1 0 1 <C (more precisely, D0 with a 1 on its left) while covering the twin's orbit. It would use the CTL format (left NFA, right NFA, key set) and go through Astra's package (astra/autonomous-20261014/certificate-package/package.py). This is direction 5 (regular-language search), not a port. 2. A hand proof of the machine's "Monotone list" dynamics. That is new work.