1RB1LF_1LC0RD_---1LA_0LA0RE_1LA1RA_1LB0LD

Status: SKIPPED (2026-10-14). The FARv3.v certificate port is refuted at the level of upstream's invariant. 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-728 (strategy direction 1, twin ports). 740 line 728, byte for byte. Class: Bell-like.

Checks: scripts/twin_check.py --long gives SUMMARY PASS (7 checks, about 4 minutes; output scripts/twin_check.out). Build the native probes first with scripts/build.sh.

The relation

728  = 1RB1LF_1LC0RD_---1LA_0LA0RE_1LA1RA_1LB0LD
twin = 1RB1LF_1LC0RD_---1LA_1LE0RE_1LA1RA_1LB0LD   (FARv3.v nonhalt216)

• Same state names, same start A, no mirror, no renaming.
• The tables differ in one entry, D0: 728 writes 0 and goes left to A, the twin writes 1 and goes left to E.
• Upstream proves the twin with solve_cert (RWL_mod_FAR 60000 30000 2 3200 2 2 3 0), a decider certificate (CTL62), not a hand proof.

When D0 sees a 0 on its left: exact merge

Let D read 0 at cell p, with t[p-1] = 0. Then:

728:  D0 A0 B0 C1   (4 steps)
twin: D0 E0         (2 steps)
both end with A at p-2, t[p-1] = t[p] = 1, every other cell unchanged

Only cells p-1 and p are read, so this holds for every tape (check M). This is the equivalence lens's "DD0 detour, 2 vs 4 steps".

When D0 sees a 1 on its left: a new halting route

With t[p-1] = 1 the machines split at the second step (728: A1, twin: E1).

728 can then halt where the twin cannot. If t[p-4..p-1] = 0 0 0 1:

728:  D0 A1 F0 B0, then C reads 0: halt (5th step)
twin: D0 E1 A1 F1 D0 E0 A0 B1 D1 E0 A0 B1 D1 ...  (12 steps inside p-4..p, no halt)

(Check X, all 128 surrounding tapes.) So the port needs this condition for every reachable configuration:

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

Given P, 728's run is the twin's run with every D0 E0 pair replaced by D0 A0 B0 C1, and upstream's theorem would carry over. Without P, the halting events differ.

P holds in simulation

• 1e6 steps (check L): after replacing each detour, the (state, position, read) sequences of the two machines are equal. No D0 sees a 1.
• 2e9 steps of each machine in C (check C, logs/d0ctx_2e9.log): no D0 sees a 1. That is 2.0e8 D0 events in 728 and 2.5e8 in the twin; 99.9% come from F1 with left context t[p-1..p-4] = 0 1 1 0.
• The hub tapes coincide: both reach 0^inf <D 0 1^3 0 1^c S with the same c and S at the same head position. The rulefit rules match after the shift c = a+3 (728) and c = a+2 (twin), for example both send c = 3m to 4m+7 with the same suffix.

Most D0 events come from the leftward pass over the (0011)^m region, which rewrites each 0011 into 1101. There the 4-periodic layout puts a 0 left of D. The rest sit at region boundaries. P is an alignment statement about this region.

Upstream's invariant does not contain P

Upstream's certificate is the closed event set of busycoq's FAR saturation (CTL.v, module FAR): - the right side is RWL_mod words over 2-cell blocks; - the left side is a stack handled by return summaries.

It was replayed natively, event by event (scripts/fartrace.ml on the extracted decider). With nonhalt216's exact parameters it closes with 10,461 events (check U).

scripts/pcheck.py lists every block transition that the closure conditions evaluate (39 transitions) and simulates each one at the cell level. In the closed set, E entering a block from the right after D0 (state E<) reads the blocks 10 and 11: 12 frame/pop pairs, for example:

frame B>[0x1%1,2x1%1,1x1%1] returns E<[1x2%0,0x1%1,1x1%1], then pops block 10   (ids: 11=0, 10=1, 01=2)

D< reading 01 also includes D0 followed by E1 inside the block. So upstream's invariant admits P-violations. In the twin they are harmless: E1 1RA, A1 1LF, F1 0LD, and no halt.

The same call on 728 fails:

FAIL at retL C<[...]   <- retL F<[...]

In words: in 728's abstraction, A reads a 1 at the left end of the tape, then F and C read blank cells. That is the shape of a P-violation next to blank cells in 728 (D0 A1 F0 B0 C0). The twin's abstraction excludes it, because there a P-violation runs E1 A1 F1 instead.

The upstream argument therefore does not carry over from any opening. Porting needs a strictly finer invariant, one that proves P.

Searches for a finer invariant (all negative)

On 728 itself, with the extracted CTL62 deciders (20 s cap):

Counts: logs/grid728_summary.json (raw rows logs/grid728*.jsonl).

The twin itself closes under only 2 of 900 RWL_mod_FAR configurations (bsz 2, mod 2, len1 3, mnc 2 or 3). Neither closed set implies P.

Split-state probe (check S). The same deciders run on a 7-state context. There, the state entered by D0 is a copy that halts on reading 1: - Calibration: the twin padded with an unused state is still proved. - The twin with D0 -> 1LG, G = 1LA--- is not proved. So FAR cannot prove P even for the twin. - 728 with D0 -> 0LG, G = 1RB--- is not proved.

The whole FAR grid above on both split machines (2 × 1,458 calls, logs/far7_grid.jsonl): 0 true, all false.

Formalization route

No port route exists. - Copying FARv3.v's call (or importing nonhalt216) gives a theorem about the twin. It would still need a proof of P, and P is a new nonhalting-strength invariant of 728: violating it can halt. - nonhalt216 depends on CTL62 (PArray/Uint63), which the unchanged check_kill baseline rejects. - No Perm or Flip is involved: the relation is the identity.

A kill needs either of these: 1. A regular invariant for 728 itself that tracks the (0011)^m alignment, in the CTL format (left NFA, right NFA, key set). Route it through Astra's package (astra/autonomous-20261014/certificate-package/package.py, blank startup checked in Coq). This is direction 5 (regular-language search), not a port. 2. A hand proof of P plus a gate-passing proof of the twin. Both are new work.