1RB1RA_1RC1LB_1LD0RA_1LB0LE_1LF1LD_---0LD

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 in simulation, but upstream's certificate covers configurations from which this machine halts. No delta proof.md exists.

Label: P-697 (strategy direction 1, twin ports). 740 line 697, byte for byte. Class: Cubic Mess.

Checks: scripts/twin_check.py gives SUMMARY PASS (7 checks, about 1 s; output scripts/twin_check.out; --long adds the 1e10-step run). Build the native probes first with scripts/build.sh.

The relation

697  = 1RB1RA_1RC1LB_1LD0RA_1LB0LE_1LF1LD_---0LD
twin = 1RB1RA_1RC1LB_1LD0RA_1RB0LE_1LF1LD_---0LD   (FARv3.v nonhalt58)

• Same state names, same start A, no mirror, no renaming.
• The tables differ in one entry, D0: both write 1 and go to B; 697 moves left, the twin moves right.
• Upstream proves the twin with solve_cert (RWL_mod_FAR 2000 1000 1 3200 2 4 1 0), a decider certificate (CTL62), not a hand proof. The same file is in the pinned vendor copy.

How D is entered (check E)

D is entered only from the right, by three transitions:

So D reads 0 with a 0 on its right only directly after F1, i.e. in the window E0 F1 D0.

When D0 has a 1 on its right: exact merge (check M)

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

697:  D0          (1 step)
twin: D0 B1 B1    (3 steps)
both end with B at p-1, t[p] = t[p+1] = 1, every other cell unchanged

Only cells p and p+1 are read, so this holds for every tape. This is the equivalence lens's "DD0 detour".

When D0 has a 0 on its right: the runs split (check X)

After D0 the machines sit at different cells: 697 has B at p-1, the twin has B at p+1 reading 0, then C at p+2. So the port needs, for every reachable configuration:

P: whenever D reads 0, the cell on its right is 1 (equivalently: F1 is never followed by D0).

Given P, 697's run is the twin's run with every D0 B1 B1 replaced by D0.

P holds in simulation

• 1e6 steps (check L): after replacing each twin detour, the (state, position, read) sequences are equal. No D0 sees a 0 on its right in either machine.
• 1e10 steps of 697 in C (logs/d0ctx_697_1e10.log): 2,170 D0 events, none with a 0 on the right. All but one have right context 1 0 1 0 and come from E1.
• D0 is rare (466 events in the first 1e8 steps): it fires when the D/E pass reaches the left end, 0^inf <D (10)^m ....

Upstream's invariant does not contain P (check U)

Upstream's certificate is the closed event set of busycoq's FAR saturation (CTL.v, module FAR): - the right side is an RWL_mod automaton with block size 1, mnc 2, mod 4, len1 1, len2 0, so a state remembers only the nearest run: [id x min(n,2) % (n mod 4)] (block ids: 1 = id 0, 0 = id 1); - the left side is a stack handled by return summaries.

The native replay of nonhalt58's exact call (scripts/fartrace.ml on the extracted decider) closes with 256 events (logs/far_twin_events.txt, one line per event with its parent). It contains:

pre3L 1|C>[0x2%2]                     left end, C facing right, a 1 on its left, right side [0x2%2]
ret3  1|C>[0x2%2] -> D<[1x1%1]        ... returns to the left end in D with a 0 on its right
retL  D<[1x1%1]                       D at the left end reads 0, right neighbour 0: a P-violation

Its DFA transitions (dfa [0x1%1] -1-> [], [0x2%2] -1-> [0x1%1], [0x2%3] -1-> [0x2%2], [0x2%0] -1-> [0x2%3], [0x2%1] -1-> [0x2%0], [0x2%2] -1-> [0x2%1]) make [0x2%2] match every 1^(4k+2) 0^inf. So the invariant covers, for every k >= 0:

0^inf 1 C> 1^(4k+2) 0^inf

From these configurations both machines reach a P-violation, and then 697 halts while the twin does not:

For c = 2, 697's run is:

step  0   0^inf 1 C> 1^2 0^inf
step 10   0^inf <D 0 1 0 1 0 1 0^inf        (P-violation: D reads 0, right neighbour 0)
step 11   0^inf <B 1 0 1 0 1 0 1 0^inf      (697: D0 1LB; the twin goes right instead)
step 40   0^inf 1^4 0 1^5 <D 1 0^inf
step 50   0^inf <E 0 1 0^2 1 0 1 0 1 0 1 0^inf
step 51   0^inf <F 1 0 1 0^2 ...            F reads 0: halt

In busycoq's soundness proof (CTL.v, PR n), every pre3L (w,(q,r)) event certifies that the machine runs n steps from (const s0 << w, r', q, R) for every r' matched by r. So nonhalt58's closed set certifies the twin's non-halting from all of 0^inf 1 C> 1^(4k+2) 0^inf. Read as an invariant for 697, the same set would certify the same for 697, which halts there. The twin's closed set is not closed for 697. The same call on 697 fails exactly there: FAIL at retL F<[0x1%1] (F at the left end, the common FF0 halt).

The upstream argument therefore does not carry over from any opening of 697. Porting needs a strictly finer invariant, one that excludes these configurations.

FAR cannot prove P even for the twin (check S, grids)

Split-state probe (bin/far7, busycoq's deciders on a 7-state context): - twin + unused 7th state, upstream parameters: true (calibration); - twin with F1 -> 0LG, G = ---0LE (G is D that halts on 0, so the machine halts exactly at a P-violation): false with upstream's parameters, and false on all 1,764 configurations of the grid below (logs/grid_splittwin.jsonl).

Direct searches on 697 itself (extracted CTL62 deciders, scripts/grid.py):

Counts: logs/grid_summary.json (raw rows logs/grid*.jsonl).

Formalization route

No port route exists. - Copying FARv3.v's call (or importing nonhalt58) gives a theorem about the twin. It would still need P, and upstream's invariant contains configurations that violate P and from which 697 halts. P is a new nonhalting-strength invariant of 697. - nonhalt58 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 697 itself that excludes the left-end family 0^inf 1 C> 1^(4k+2) ... (more generally, E reaching an isolated 1 with a 0 on both sides), in a gate-passing format (Astra's NFA package, direction 5). The FAR and plain CTL grids above found none at these sizes. 2. A hand proof of P for 697 (an alignment/parity statement about the (10)^m (01)^n region the D/E pass leaves behind) plus a gate-passing proof of the twin. Both are new work; Cubic Mess dynamics make this a family-sized project, not a port.

Indv6.v near-twins

Indv6.v (hlin decider, solve_hlin_nonhalt, T = 1e6) proves two machines one transition away from 697: tm99 ..._1LF1LD_---1RD (F1 differs) and tm326 ..._1LF1RE_---0LD (E1 differs). Neither is a lockstep twin: each changes a transition that fires regularly in 697 (E1 6,614 times and F1 64 times in the first 1e6 steps), so they give no port.

hlin with Indv6's exact configuration (logs/hlin697.txt, extracted decider): true on both near-twins (0.11 s and 0.30 s, calibration), no result on 697 within 150 s.