1RB1RE_1LC0RC_0RA0LD_1LB1LE_0RC1LF_---1RA
Status: SKIPPED (2026-10-14). The halting port from RWLAccHaltv6.v is refuted at the halting event itself. This machine runs exactly like its twin tm161 until tm161 halts. At that step tm161's F reads a 1 on the right and halts, but this machine's F reads the 1 that A has just written on the left, so it runs on. The same happens for line 276 and its twin tm158. No delta proof.md exists.
Label: P-145/276 (strategy direction 1, twin ports). 740 line 145, byte for byte; the partner is line 276 (machines/1RB1LA_0LB1LC_1RD0LD_0LA0RE_1RC1RF_0LD---/). Class: Chaotic Bell Class 4, the same family as W6-5 (line 333, CRYPTID_CANDIDATE).
Checks: scripts/twin_check.py gives SUMMARY PASS (10 checks, about 4 s; output in scripts/twin_check.out). It reads the native RWLAcc dumps in logs/. To rebuild the dump driver, run scripts/build_prehalt.sh OUTDIR; it compiles against a copy of Astra's extracted RWLAcc62_BigUint module.
Line 145 against tm161
145 = 1RB1RE_1LC0RC_0RA0LD_1LB1LE_0RC1LF_---1RA
tm161 = 1RB1RE_1LC0RC_0RA0LD_1LB1LE_0RC1RF_0LA--- (RWLAccHaltv6.v, halts_at_trans ... (F,1))
- Same state names, same start A, no mirror (check R145).
- Only E1, F0 and F1 differ. F is entered only by E1 in both machines.
- Upstream's proof is
solve_halt' 48 20000 true 2%N (10^8)%N. That is RWLAcc62_BigUint evaluation, whose soundness brings Uint63 primitives beyond our baseline.
The detour through F (check M145)
Let E read 1 at cell p. Both machines write 1 there and step into F.
| Machine | F reads | Result |
|---|---|---|
| tm161 | t[p+1] | 0: back to A at p, after 2 steps. 1: halt |
| 145 | t[p-1] | 1: back to A at p, after 2 steps. 0: halt |
When both continue, they reach the same configuration (t[p] = 1, A at p) after the same number of steps. Every other transition is shared.
How E is entered (check K145)
E is entered by exactly two transitions, and each fixes one neighbour:
- A1 = 1RE, from the left. Afterwards t[p-1] = 1, so 145 never halts at this E.
- D1 = 1LE, from the right. Afterwards t[p+1] = 1, so tm161 halts here whenever E reads 1.
So every halting event of 145 is also a halting event of tm161. The two runs are therefore equal, step for step outside F, up to tm161's halting step. (At 1e8 steps both configurations are identical; check L145.)
At that step, 145 halts too only if tm161's last E was entered by D1 and t[p-1] = 0.
tm161's actual halting event (check H161)
Upstream's call is solve_halt' 48 20000 true 2 1e8. Re-run natively (Astra's extracted RWLAcc62_BigUint, scripts/prehalt_main.ml), it halts at F1 after 733,223 accelerated iterations, which matches upstream. The driver dumps the last configuration before the halt (logs/prehalt_tm161.txt). Its counts are around 10^33, so the halting step is far beyond direct simulation.
The window around the head, run concretely, halts after 201 steps:
step 199 A reads 1 at cell 21 (A1 = 1RE)
step 200 E reads 1 at cell 22 (entered by A1)
step 201 F reads 1 at cell 23 -> tm161 halts
The last E was entered by A1. So 145's F reads t[21] = 1, the 1 that A wrote at step 199, and 145 runs on: E keeps moving right over the 1s.
The twin's halting event is of the kind 145 always survives. The runs split exactly at tm161's halting step, and 145 does not halt there.
After the split (check X)
- The same native call on 145 gave no verdict within the 900 s wall cap (
logs/rwl_big_145.txt); tm161 halts in 128 s. - After 740,000 iterations, 145 has not halted. Its configuration still carries 15 of tm161's 16 pre-halt counts above 10^30, up to 1 (
logs/rwl_145_740000_iterations.txt). So it is just past the split.
Line 276 against tm158 (the partner)
276 = 1RB1LA_0LB1LC_1RD0LD_0LA0RE_1RC1RF_0LD---
tm158 = 1RB0RA_1RC0LC_0LD0RA_1LB1LE_0LC0LF_1RD--- (RWLAccHaltv6.v, (F,1), same solve_halt' call)
From blank, both machines carry the same tape up to a translation: tm158's cell p is 276's cell p+2. The states correspond as follows:
| tm158 | 276 | Note |
|---|---|---|
| B | C | sync state |
| C | D | sync state |
| A, when entered by C1 | E | |
| D, E | A |
The identical cells under this map are B0/C0, B1/C1, C0/D0, C1/D1, A0/E0 and D1/A1. Four guarded detours make up the rest:
| Detour | 276 | tm158 | Guard | Both end with |
|---|---|---|---|---|
| EA1 | E1 F0 D1 E0 | A1 A0 | t[p+1] = 0 | t[p] = 0, t[p+1] = 1, then C / B at p+2 |
| DA0 | D0 A0 B0 B1 | C0 D0 | none | t[p-1] = 1, then C / B at p-2 |
| EA0 | A0 B1 C1 | E0 | none | D / C at q-1 |
| AE1 | A1 A0 B1 C1 | E1 F0 D0 B1 | t[q-1] = 0 | t[q-1] = 0, t[q] = 1, then D / C at q-2 |
Check R276 tests every radius-7 context from a sync pair. Each one either merges at the image of tm158's next sync configuration (59,392 contexts) or ends in one of two split events:
- S1 (2,048 contexts). tm158 runs D1, E1, F1 over three 1s moving left and halts. 276 is in A at the same cells, on the same tape, and sweeps left over those 1s (A1 = 1LA).
- S2 (4,096 contexts). 276 runs D1, E1, F1 (E reads 1 with a 1 on its right) and halts. tm158 is in A there and sweeps right (A1 = 0RA).
Check L276 confirms the lockstep from blank to 3e5 steps of tm158 (149,674 sync configurations, 0 misses).
tm158's halting event (checks H158 and X)
- tm158's native run halts at F1 after 732,886 iterations (
logs/prehalt_tm158.txt). - Its window halts after 198 steps through D1, E1, F1 at cells -22..-24. That is an S1 event.
- Replayed from the sync point 30 steps earlier, 276 matches all 15 sync configurations. It then visits those three cells in A and runs on.
- An earlier S2 event would have made 276 halt. Instead, 276's native run passes 1,500,000 iterations without halting, with counts up to about 10^72; tm158's largest count at its halt is about 10^33.
So 276 also survives its twin's halting event.
Why the port cannot be rescued
Upstream's proofs certify only that each twin halts. Both twin runs end exactly where our machines split off, so nothing in them constrains what the holdouts do afterwards. A proof for 145 or 276 is a new problem:
- halting: reach a later halt from the split configuration (counts around 10^33 to 10^72 already);
- nonhalting: an invariant for a Chaotic Bell Class 4 machine. W6-5, the third member of this family, parked as a cryptid candidate (layer law x4/3 with a mod-3 branch).
Formalization route
None for the port. No module of RWLAccHaltv6.v applies: its lemma for tm161 or tm158 proves the twin halts and says nothing past that step. Even for a later halt of 145 or 276, the gate needs the standard RWLAcc62 checker under vm_compute, not RWLAcc62_BigUint, because BigUint soundness lists Uint63 primitives outside the baseline. Astra's tm1193 calibration passed the unchanged gate this way. No Perm or Flip is needed for 145 (identity relation).
Next (not funded)
The only open lead is a longer accelerated run past the split, which is direction 3 (halting pipeline). Run the 900 s-capped native RWLAcc on 145 and 276 for longer, and with other widths. Count a result only if the standard RWLAcc62 call reproduces it.