/machines/1RB0RA_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/proof.md · raw

1RB0RA_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---: informal non-halting proof (incomplete: one lemma open)

Summary. The sweep boundary is S(w) = 0^inf 11 D> <w> 0^inf, as in the parent. The parent's tokens and passes carry over, with two changes: 1. At an L, this machine sends +1 to the rest but adds no pass. 2. There is a one-cell stray token S = 1, a drain suspended with 0 passes.

Call a boundary word w = L^n t good, G(w), if the n increments sent by its own leading L's turn t into a word with no stray. Then: - the sweep of a good word is defined and leaves at most one stray (Lemma C); - the next word is good exactly when the current sweep would leave no stray if it were given n' extra passes, where n' is the next word's L-run. That is one inequality, θ(x) ≤ n', for a threshold θ of an S-free word x (Lemma D).

What is missing is an invariant that implies this inequality at every sweep and is preserved by the sweep. On the first 3,000 sweeps of the abstract orbit (and at the 278 boundaries from blank to 1e9) the inequality holds with 2θ ≤ 0.962 n' at worst. But none of the candidates tried so far is preserved by the sweep for all words: not the bare inequality, not its factor-2 version, not that plus the orbit's value bound (with or without a lower bound on N), and not the V*-based J4 of §3.3.5.

1. Families and notation

2. Rule table

1RB0RA_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---      (parent with A1 = 0RA instead of 0RF)

S(w) = 0^inf 11 D> <w> 0^inf        L = 110, 0 = 000, 1 = 100, S = 1 (one cell)
start: 0^inf A> 0^inf  -(5)->  S(1)                                   (A0 B0 C1 D0 D0; A1 never fires)
sweep: S(w) -+-> S(w')  if R(hx,0,w,w')     (w' starts one cell further left; then re-parse canonically)
domain: G(w) (section 3.3.3); G(1) holds; closure under the sweep is OPEN (section 3.3.5)

Inc (one h pass):
  I1  Inc(1::r, 0::r') <- Inc(r,r')        I3  Inc(L::r, L::r') <- Inc(r,r')
  I2  Inc(0::r, 1::r)                      I4  Inc([], [1])
  IS  Inc(S::r, r')    <- R(h1,1,r,r')                                 NEW (mutual with R)

R (k >= 0):                                        parent                     Rocq (TwinSpec.v)
  X1  R(hx,k,   L::r, L::r') <- Inc(r,r1), R(hx,k,r1,r')    R(hx,k+1,r1,r')  CHANGED  RIncs_hx_ld
  X2  R(hx,k,   0::r, L::r') <- R(hx,k+1,r,r')                                       RIncs_hx_d0
  X3  R(hx,k,   1::r, L::r') <- R(h1,k,r,r')                                         RIncs_hx_d1
  C1  R(h1,k+1, L::r, L::r') <- Inc(r,r1), R(hx,k,r1,r')    R(hx,k+1,r1,r')  CHANGED  RIncs_h1_ld
  C2  R(h1,k+1, 1::r, L::r') <- R(h1,k,r,r')                                         RIncs_h1_d1
  C3  R(h1,2k+1,0::r, 0::r') <- R(h1,k,r,r')                                         RIncs_h1_d0_0
  C4  R(h1,2k+2,0::r, 1::r') <- R(h1,k,r,r')                                         RIncs_h1_d0_1
  R0  R(h1,0,[],[1])     R1  R(h1,2k+1,[],0::r') <- R(h1,k,[],r')    R2  R(h1,2k+2,[],1::r') <- R(h1,k,[],r')
  Z   R(h1,0, r, S::r)   for every r                        Z0, Z1 only       NEW      RIncs_z
  EQ  R(tp,k, r, r')     <- toRC r = toRC r0, R(tp,k,r0,r')  none             NEW (p3) RIncs_eq
      end identities: toRC [S;1] = toRC [L] (s1_eq), toRC (S::0^j) = toRC [1] (s0_eq)
  (no clause: hx on [] or on S::r; h1 with k >= 1 on S::r; EQ only re-reads, it reaches nothing new on a tape)

per-token transduction (one pass in; the passes it sends right, assuming each comes back as <C):
            L               0             1                S0          S1          SL
  h      [h]  L        []  1         [h]  0           [] 0 S      [] L S      [h,h'] L
  h'     [h,h'] L      [h',h] L      []  L S
         parent: (L,h') and (SL,h) give [h,h',h];  TM7: (L,h') gives [h',h]

machine level, j = number of digits of X before its first 0 digit:
  eater enters L:  1 D> 110 <X>  -(6j+9)->   0 111 D> <X+1>     parent: -(6j+13)-> 1 111 D> <X+1>
  drain enters L:  B> 1 110 <X>  -(6j+8)->   0 111 D> <X+1>     parent: -(6j+12)-> 1 111 D> <X+1>
  then, when the eater's pass returns:  0 11 <C -(3)-> <C 110    (the parent bounces one more h pass here)
  wall:  0^inf 1 <C <w'>  -(3)->  0^inf 11 D> <w'>                 (C1, D0, D0; unchanged)

In words: - Where A1 fires. As in the parent, A1 fires once for each L entered, on the middle cell of the 110. - A1 = 0RA writes 0 there and steps onto the last cell (a 0) in state A. - A0 = 1RB writes a 1 there and starts the same h pass over the rest as the parent's F0 = 0RB. - On return, C reads that 1, where the parent's C read a 0. So C1 = 0LD, D0, D0 restarts the eater one cell left of the parent's position, with 0 111 behind it. - When the eater's pass returns, 0 11 <C closes up to <C 110 directly. - Net effect: the L sends +1 to the rest but adds no pass. - Eater (hx, k). It eats L's (each one is +1 on the rest; k unchanged) and 0's (each one adds a pass). It stops at the first 1 and drains from there. - Drain (h1, k). A 1 absorbs a pass and becomes L. A 0 halves the count and keeps one bit of it. An L restarts the eater with k-1 and sends +1 to the rest. At the right end the count is written in bijective binary. - With 0 passes left, the drain stops wherever it is (Z) and leaves the stray in front of the untouched rest. - In the parent this could happen only at a last digit, which is why its Z0/Z1 identities sufficed. - Next sweep. The eater's n leading L's send n +1 passes to the tail u S v. Each one that carries through u resumes the suspended drain on v by one pass (IS). G (§3.3.3) says that these n passes always finish that drain.

Worked example (the start of the run from blank; §7 checks every boundary to 1e9): - S(L1). - Parent: X1 gives k = 1 and +1 makes 1 into 01; X2 gives k = 2; X3 drains 2 passes at the right end (R2). Result S(LLL11) at step 91. - Here: X1 keeps k = 0; X2 gives k = 1; X3 drains 1 pass (R1). Result S(LLL01) at step 69. - S(LLL01) gives S(L^4 S01) at step 146. The 3 +1s turn 01 into 101. The eater then hits the 1 with k = 0, and Z leaves the stray in front of 01. - S(L^4 S01) gives S(L^5 SL1) at step 259. The 4 +1s turn S01 into 0S1 (IS, C3, Z), then 1S1, then 0L1 (IS, C2, R0), then 1L1. The eater stops at the 1 with k = 0, and Z gives S L1. - S(L^5 SL1) gives S(L^9 S001) at step 600. - The first +1 hits SL (IS, then C1). That starts a nested eater with k = 0 on Inc(1) = 01, so this +1 pass alone turns SL1 into LLL01. - The other four +1s give LLL011. - The eater then eats LLL, doing 3 more +1s (011 becomes 1001), and Z leaves S001.

3. The argument

3.1 Every clause is an exact pass-level run (spec_both): Rocq-checked

Claim, as in the parent: - Inc(r,r') implies sideRLs [h] <r> <r'>; - R(hx,k,r,r') implies sideRLs ([h'] ++ h^k) <r> <r'>; - R(h1,k,r,r') implies sideRLs (h^k) (1 <r>) <r'>.

The proof is by mutual induction on Inc and R (Scheme ... Combined Scheme Inc_RIncs_mut). Case by case: - I1–I4, X2, X3, C2–C4, R0–R2. None of these runs fires A1, the only transition where this machine differs from the parent and TM7. So the scripts are the parent's (= TM7's), unchanged. - X1. seg_hx_ld k: segRLs (h' ++ h^k) (h ++ h' ++ h^k) ld ld. The parent has h^(1+k) on the right. It is followed by sideRLs_trans with the Inc premise (+1) and the R premise ([h'] ++ h^k on r1). - C1. seg_h1_ld k: segRLs (h^1 ++ h^k) (h ++ h' ++ h^k) w1ld ld, with the same change. - IS. toRC (S::r) = [1] *> toRC r, so the premise sideRLs ([] ++ h^1) ([1] *> toRC r) (toRC r') is the goal, by conversion. - Z. It uses zero passes, so it holds by sideRLseq_O, because toRC (S::r) = [1] *> toRC r holds by definition. - EQ (RIncs_eq, pass 3). rewrite with toRC r = toRC r0 turns the goal into the induction hypothesis. - End identities. s1_eq: toRC [S;1] = toRC [L] and s0_eq j: toRC (S::0^j) = toRC [1] are the parent's z1_eq/z0_eq, by const_unfold. With them, Example sweep_LS01: R(hx,0, LS01, LLLL01) compiles. That is the word for which the 16 clauses alone have no derivation (§3.3.3).

This compiles (scripts/TwinSpec.v, 3.7 s), with closed Print Assumptions for Inc_spec, RIncs_spec, BigStep, init and sweep_LS01. On the real machine every derivation also checks out directly (§7).

3.2 Sweep (BigStep): Rocq-checked

S(w) = 0^inf 1 · 1 D> <w> -+-> 0^inf 1 <C <w'> -(3)-> S(w'), by sideRLs_1 and then the wall rule. This is the parent's proof verbatim; it compiles.

The canonical re-parse that follows is a tape identity: S(w') = S(w'') whenever <w'> 0^inf = <w''> 0^inf.

3.3 The domain

3.3.1 Semantic reading, Lemma A and Lemma U

R and Inc are pass compositions (§1), so E_k = Inc^k ∘ E_0 and D_k(r) = Inc^k(S r) as tapes. The clauses then read as follows: - Inc(S 1 r) = L S r, Inc(S 0 r) = 0 S r, Inc(S L r) = L E_0(Inc r) and Inc(S) = 0 1. So a +1 pass moves the stray right by one token, or absorbs it at an L by starting a nested eater. - E_k(L r) = L E_k(Inc r), E_k(0 r) = L E_{k+1}(r) and E_k(1 r) = L D_k(r). - There is no clause for E_k([]), E_k(S..) or D_{k+1}(S..). These are the three failure modes. In the two stray cases, unless an L follows the stray, the machine leaves the token form.

Lemma A (one more pass is +1 on the result): R(tp,k,r,r') /\ Inc(r',r'') -> R(tp,k+1,r,r''). - Proof by induction on R, exactly as the parent's RIncs_Inc. - X1 and C1 use the IH at k+1. C3 and C4 swap (carry). R0 -> R1, R1 -> R2, R2 -> R1. - The new case Z: Inc(S::r, r'') can only be IS, whose premise is R(h1,1,r,r''). (There is no re-parse constructor for Inc, so this inversion stays valid.) - The new case EQ: the IH on R(tp,k,r0,r') gives R(tp,k+1,r0,r''), and EQ with the same tape identity gives R(tp,k+1,r,r''). - If the given derivation does not use EQ, neither does the one built, and neither does any Inc derivation it consumes.

Lemma U (uniqueness, pass 3). Convention: at k = 0 on [], every derivation built in this proof uses R0, never Z. (Z on [] would give [S], the same tape as R0's [1] by s0_eq 0, so nothing is lost.) Under this convention, Inc and the EQ-free R are partial functions: every instance Inc(r,·) or R(tp,k,r,·) has at most one derivation, whatever the input, strays included. - Proof by mutual induction on derivations, inverting the second one. Every clause is fixed by (tp, k, first token): - Inc: L gives I3, 0 gives I2, 1 gives I1, [] gives I4, and S gives IS. - hx: L gives X1, 0 gives X2, 1 gives X3. - h1 with k = 0: Z, or R0 on [] (the convention). - h1 with k ≥ 1: L gives C1, 1 gives C2, 0 gives C3 or C4 by the parity of k, and [] gives R1 or R2 by parity. - The Inc premise of X1/C1 and the R premise of IS are unique by the IH. So the next premise's input is the same word in both derivations. - Lemmas A and B respect the convention. Lemma A turns R0 into R1 with premise R0. Its Z case reuses the premise of the given IS. Its other cases recurse. Lemma B uses R0 on []. - So Lemma A's output is the output of R(tp,k+1,r,·), syntactically. - This is what the shorthand E_k, D_k, the chain in §3.3.3 and the threshold θ below rely on. The parent used only Inc's functionality; here IS embeds R in Inc, so U covers both. - EQ is outside U. It is used once per sweep (Lemma C), on a derivation that is never compared with another. - Determinism of the machine is not used. sideRL quantifies over all left halves, so it is not obviously functional.

End identities commute with Inc (pass 3). For any u: Inc(u S 0^j) and Inc(u 1) are the same tape, and so are Inc(u S 1 0^j) and Inc(u L). - If the carry stops inside u, the right ends are untouched. - Otherwise the carry reaches the end: - IS with C3 then Z gives 0 S 0^(j-1), the same tape as 0 1, which is I1 then I4. For j = 0 it is R1 then R0, giving 0 1. - IS with C2 then Z gives L S 0^j, the same tape as L 1, which is I3 then I4. - So "S-free" (always the canonical form) does not depend on whether an Inc chain is re-parsed before or after.

3.3.2 Lemma B: S-free words are safe

For an S-free word r: - (B1) R(h1,k,r,·) exists for every k. - (B2) R(hx,k,r,·) exists for every k if and only if r contains a 1 or an L (r is not in 0*). - (B3) Each such output has at most one stray. - (B4) Inc of a word with at most one stray exists and has at most one stray.

Proof: - B1–B3 are proved by well-founded induction on the pair (|r|, number of L tokens in r), ordered lexicographically, together with an inner induction on k for R(h1,k,[]) (TM7's RIncs_nxt_1). - X2, X3, C2, C3, C4 recurse on a strictly shorter word. - X1 and C1 recurse on Inc(r) from L::r: - If the carry stops inside r, |Inc r| = |r| < |L::r|. - If it runs off the end, then r is over {L,1}, |Inc r| = |L::r|, and Inc r has one L fewer than L::r. - No stuck case. With no stray, the only clause-less case is the eater at the right end. E_k(0 r) = L E_{k+1}(r) reaches it exactly when r is in 0*. After an L the rest is Inc(..), which always contains a 1. - Stray count. Every clause emits one non-S token before its recursive output, except Z (S::r with r S-free) and R0. - B4. If the carry reaches the stray, Inc becomes IS, R(h1,1,v,·) on the S-free rest v, and B1 and B3 apply.

3.3.3 The predicate G and Lemma C

Let w = L^n t be a boundary word with n maximal. Assume w is canonical and has at most one stray; B4 needs both. Let t_n be the output of the chain Inc(t, t_1), Inc(t_1, t_2), …, Inc(t_(n-1), t_n). B4 says the chain exists, and U says it is unique (under the R0 convention). Let x(w) be the canonical form of t_n.

Definition. G(w) holds when w is canonical, #S(w) ≤ 1, and x(w) is S-free and contains a 1 or an L.

Lemma C. If G(w), then R(hx,0,w, L^n E_0(x)) is derivable with exactly one use of EQ, at the place given below. The output has at most one stray.

Proof (the derivation, in order): 1. X1, n times: R(hx,0,L^n t, L^n o) <- Inc(t, t_1), R(hx,0, L^(n-1) t_1, L^(n-1) o) and so on. The Inc premise of the i-th X1 is Inc(L^(n-i) t_(i-1), L^(n-i) t_i), by I3 over the remaining L's and then the chain above. This leaves the goal R(hx,0, t_n, o). 2. EQ here, once: R(hx,0, t_n, o) <- toRC t_n = toRC x, R(hx,0, x, o). This is the point after the eater's n increments and before it reads the tail. - t_n and x differ only at the right end. x is S-free, so the stray of t_n (if any) stands in S 0^j or S 1 0^j at the end (§1). - So the identity is s0_eq or s1_eq behind a common prefix, plus d0s_eq for trailing 0 tokens. 3. R(hx,0, x, o) exists by B2, because x is S-free and not in 0*. That B-derivation does not use EQ, and o has at most one stray by B3.

Why EQ is needed here, and not only between sweeps: take w = LS01, for which G holds (x = 0L). The only derivation of Inc(S01,·) is IS, C3, Z, which gives 0S1. The eater then eats the 0 (X2) and meets the S with k = 1, and no clause applies. With EQ, 0S1 is re-read as 0L and the sweep gives LLLL01, which matches the real machine. This derivation is the compiled Example sweep_LS01 in TwinSpec.v. Without EQ, 75 of the 15,593 G words with tails of at most 6 tokens and n ≤ 15 have no derivation; with EQ, all of them do (check 9a). None of the 3,000 orbit boundaries needs it, but the proof cannot rely on that.

After the sweep, the output L^n o is re-parsed canonically at the configuration level: S(L^n o) = S(w') with w' canonical, a tape identity (§3.2). w' has at most one stray by B3, so the first two conjuncts of G(w') hold automatically.

G(1) holds: n = 0 and x = 1.

3.3.4 Lemma D: the domain reduces to one inequality per sweep

Let G(w), let x = x(w), and let a be the number of leading L's of E_0(x). Then the next boundary word is w' = L^(n+a) t', where E_0(x) = L^a t'.

Lemma D. G(w') holds if and only if E_(n+a)(x) is S-free.

Proof: - Apply Lemma A n+a times: E_(n+a)(x) = Inc^(n+a)(L^a t') = L^a Inc^(n+a)(t'), the second step by I3. - The Inc steps here are w''s own chain (§3.3.3), behind a prefix of L's (I3). So x(w') is, up to the canonical re-parse, the tail of this E_(n+a)(x). - By U, this is the (unique) derivation of R(hx,n+a,x,·). - E_(n+a)(x) exists by B2. - w' is canonical with at most one stray (§3.3.3). So G(w') is equivalent to: x(w') is S-free and contains a 1 or an L. The S-free part is the claim. - The "1 or L" part holds automatically (needed for B2 at the next sweep): - a ≥ 1, because X1, X2 and X3 all emit L as their first token. So n' = n + a ≥ 1, and x(w') is the output of at least one Inc. - Every Inc output contains a 1 or an L: - I2 and I4 write a 1, and I3 keeps its L. - I1 outputs 0 :: followed by an Inc output, so the claim holds by induction. - IS runs R(h1,1,r,·). Its first clause is C1 or C2, which emit L. Otherwise it is C3 followed by Z, giving 0 S r, whose re-parse, when S-free, is 0 1 0^j or 0 L 0^j. Otherwise (r = []) it is R1 then R0, giving 0 1. C4 needs k ≥ 2. - Canonical re-parsing does not change the tape, and an S-free word whose tape has a 1-cell has a token 1 or L. - Check 9b confirms this on every word of check 9a.

Threshold. For S-free x not in 0*, let θ(x) be the least M such that E_M(x) is S-free. - It exists. Until the first Z, the sequence of clauses and remaining inputs does not depend on the counts: only the bits written by C3/C4 and the end digits do. By the measure of Lemma B this sequence has finitely many steps, and each step maps a count c to at least (c-2)/2. So a large enough M never reaches 0. - It is monotone. E_(M+1) = Inc ∘ E_M (Lemma A, with U for "the" output). Inc maps S-free words to S-free words (I1–I4), and it commutes with the canonical re-parse (§3.3.1). - It is well defined. By U, E_M(x) is a single word. The check scripts compute θ by doubling and binary search, which relies on monotonicity. Check 9c also computes it by brute-force linear search for its family.

So G(w') <-> θ(x) <= n' with n' = n + a. The next tail is x' = x(w') = drop_a(E_(n')(x)).

Writing N_s := n_(s+1) for the sweep s with S-free word x_s, the whole domain question is this. For the dynamical system

(N, x)  |->  (N + a(x'), x')      with   x' := E_N(x) minus its first a(x) L's,   a(y) := leading L's of E_0(y)

started from the orbit, show θ(x) <= N at every step.

3.3.5 Open: an inductive invariant

What is needed is a predicate J(N, x) that: - holds at some reachable boundary (the start can be moved later by computation); - implies θ(x) <= N; - satisfies J(N, x) -> J(N + a(x'), x').

Refuted candidates (each counterexample is checked in §7, checks 8f, 9c and 9i): - G itself, as a predicate on words. 1001 satisfies G, and its sweep LS001 does not: Inc(S001) = 0S01, and then the eater meets the stray. Among words with G (tails of at most 5 tokens, n ≤ 13), 181 of 1,893 sweep to a word without G. - J0 := θ(x) ≤ N. Take x = 00010001 and N = 5. Then θ(x) = 4, E_0(x) = LLLL 00S01, x' = 100L, N' = 6 and θ(x') = 7. - With a margin, one step is fine: if N - θ(x) ≥ 4, then θ(x') ≤ N' (every S-free x of at most 7 tokens, margins 4 to 39; check 8f). - But the margin can fall below half in one step. Take x = L11111L and N = 26: the margin is 26, x' = 100001, and the new margin is 12. So a count-only margin is not inductive either. - J2 := 2θ(x) ≤ N and x ends with the token 1. Take x = L1111 and N = 60. Then θ(x) = 0, x' = 1000001, N' = 61 and θ(x') = 31, so 62 > 61. Here V(x') = 65 exceeds N'. The orbit never does this (below). - J3 := J2 and V(x) + (leading L's of x) ≤ 5N/4, which adds the orbit's value bound. Take x = L11 and N = 4. Then θ(x) = 0, V(x) + 1 = 4, x' = 111 and N' = 5, but V(x') = 7 > 25/4. - J3 with a lower bound N ≥ N0 is refuted for every N0 (pass 3, check 9c). For m ≥ 4, take (N, x) = (2^(m+1) − 4, 00001). - It satisfies J3: θ = 0, x ends with 1, and V + lead = 16 ≤ 5N/4. - One step gives x' = 1 0^m 1, N' = 2^(m+1) − 3 and θ(x') = 2^m − 1. So 2θ' = N' + 1, and the 2θ ≤ N conjunct fails. - Checked for m = 4..20 (for example N = 252 → 253 with θ' = 127). θ' is found by brute-force linear search for m ≤ 10, and for larger m by binary search with both sides of the threshold checked. - In this family V(x)/N → 0, while the orbit has V(x_s)/N_s ≥ 0.507 for s ≥ 27. So a J that bounds θ through N, as J2 and J3 do, must also bound V from below against N. J4 below avoids this by bounding θ through V* instead. - Replacing 2θ ≤ N by θ ≤ N does not rescue J3 (reviewer's examples): - (428, 10000000LLL1) breaks the value bound: V' = 557 > 5/4 · 429. - (439, LL11111111LLL1) gives x' = 0001110LLLL0L, which does not end with 1. - In every one of these counterexamples θ(x') ≤ N' still held; only the extra conjuncts broke. The reviewer's random search found the same: about 25,000 sampled states, none violating θ' ≤ N'.

Pass 3: a weighted value that makes the sweep affine. For an S-free word y, define V*(y): the little-endian binary value of its 0/1 tokens, plus 2^p for every L that stands after exactly p digit tokens. So an L counts as the +1 it sends to the rest when eaten. For example, V(1L01) = 1 + 2 + 0 + 4 = 7. - (V1, proved.) Inc adds exactly 1 to V* on S-free words. - I1/I2 are binary +1 on the digit tokens. I3 does not change how many digits stand before any L. I4 appends a 1 after all the L's, at position p (the number of digits): every earlier digit was a 1 and turned to 0, so the total gains 2^p − (2^p − 1) = 1 in digits, and the L weights are unchanged. - Check 9e: exhaustive, words up to 8 tokens. - (V2, proved from Lemma A, U and V1.) The sweep is affine. For S-free x not in 0*, let y(x) be the canonical form of E_θ(x) without its first a(x) L's (an S-free word), and let c(x) := V(y(x)) − θ(x). Then for every N ≥ θ(x):

V*(x') = N + c(x), x' = Inc^(N−θ)(y(x)), and the L's of x' are exactly the L's of y(x), at the same digit positions

What is open, precisely. Find a shape condition K(N, x), such that: 1. K(N, x) and x ends with 1 imply c(x) ≤ N + 3. With V2, this keeps V* ≤ 2N + 1. 2. K and J4 together give "x' ends with 1" and K(N', x'). 3. K holds at some reachable boundary.

Then J := J4 ∧ K, together with a proof of Lemma T, closes the domain. - K can only talk about where the L's of x sit relative to its top digit and how many passes reach them. By V2, the L's of x' are those of y(x), and the digits of x' are y(x)'s plus N − θ. - So K is a statement about the threshold output y(x) against the count N − θ that is added to it. - Two-step or "eventually" forms (J4 ∪ sweep(J4)) are an alternative. In all 400 samples of 9j, two sweeps brought the state back to V* ≤ 1.45 N.

What the orbit does (checked in §7, check 8e; these are the first 3,000 sweeps, not the whole orbit): - G holds at every boundary of the 3,000-sweep abstract orbit and at all 278 from-blank boundaries to 1e9. - x_s always ends with the token 1, so the top bit slot is filled. - 2θ(x_s) ≤ 0.962 N_s. The worst case is sweep 27: N = 131 and θ = 63. - V(x_s) + (leading L's of x_s) ≤ 1.25 N_s. The bound is attained with equality at sweep 2 (N = 4, x = 101: V = 5), so J3's constant 5/4 has no slack at all (check 9d). Any reuse needs a slack constant or a start after sweep 27. - V(x_(s+1)) = N_s - θ(x_s) exactly on 2,813 of 2,999 sweeps. Equivalently, the threshold output E_θ(x_s) has value 0, since Inc is +1 on V for S-free words. So each sweep "adds N and eats from the bottom". - V2 is the exact form of this, with the L's counted: V*(x_(s+1)) = N_s + c(x_s) on all 2,999 sweeps.

Why the parent's method does not transfer directly. The parent's key lemma tracks only counts (tp, k, j, tq, q) and works for every input word. - Here the second sweep's count does not grow when it eats an L. The first sweep's view count (k + j) grows instead. - So a second-sweep drain that starts from a 1 bit can meet a view count far larger than its own, and run out. - Whether that happens depends on how many 0 tokens lie ahead, which is a property of the word, not of the counts. - Any working J must therefore bound the shape of the tail, not only counts. Pass 3 narrows this: under V2 and Lemma T, the counts reduce to the single inequality V* ≤ 2N + 1. What remains of the shape is the condition K on the L's.

This is the remaining mathematics. It is not a cryptid: every rule is counter arithmetic (+1, halving, bijective binary), and V2 makes the counts exactly affine. But the closing argument is a new invariant (K plus a proof of Lemma T), not a delta of the parent's.

3.4 Progress

R is inductive (mutually with Inc), so every derivation is finite, and Lemma B's measure bounds the clause sequence. Each sweep is a finite run of at least 4 steps: h' takes at least 1 and the wall takes 3.

3.5 The halting transition F1

Every rule is a proved exact run, so no step reaches F1. Here F is entered only by E0 = 0RF, because A1 no longer enters F. In every clause run of §7, F never read a 1.

4. Initial segment

0^inf A> 0^inf reaches S(1) in 5 steps. A1 is never fired, and init: c0 -[tm]->* S' [D1] compiles by esx: - -A0-> 0^inf 1 B> 0^inf - -B0-> 0^inf 1 <C 1 0^inf - -C1-> 0^inf <D 0 1 0^inf - -D0-> 0^inf 1 D> 0 1 0^inf - -D0-> 0^inf 11 D> 100 0^inf = S(1)

G(1) holds (§3.3.3). If the closing invariant J needs a margin that S(1) lacks, the start can be moved to a later boundary S(w_s). Every boundary to 1e9 is known exactly (§7), and its derivation can be produced by esx or by the clauses.

5. Conclusion: blocked on §3.3.5

Given J, the assembly is the parent's: 1. multistep_nonhalt to the starting boundary (§4). 2. progress_nonhalt_cond with

P(w) := w canonical /\ #S(w) <= 1 /\ G(w) /\ J(n(w) + a(x(w)), x(w))

The first two conjuncts are also inside G (§3.3.3). They are written out because B4, x(w) and the S-free test all need them, and P must carry them from one sweep to the next. 3. Each step: - Lemma C gives R(hx,0,w,L^n o), with exactly one EQ, placed after the eater's L-run. - BigStep then gives S(w) -+-> S(L^n o). - The configuration-level re-parse S(L^n o) = S(w') makes w' canonical. w' has at most one stray by B3, which re-establishes the first two conjuncts. 4. Lemma D (the "if" direction, with its "1 or L" part) and J's closure give G(w') and J(n(w') + a(x(w')), x(w')), so P(w').

Without J, the machine is not shown to run forever. The candidate from pass 3 is J := J4 /\ K with Lemma T (§3.3.5). In it, J4 is a pure count condition and K is the still-unknown condition on where the L's sit.

6. Lemma plan (reusing the parent's .v and scripts/TwinSpec.v)

piece source change state
tm, digits, RD + DS, toRC, h/h' TwinSpec.v none compiles
Inc/RIncs (16 clauses + RIncs_eq, mutual), spec_both, seg_hx_ld, seg_h1_ld TwinSpec.v RIncs_eq added in pass 3 compiles
BigStep, init parent, verbatim none compiles
canonical end identities s1_eq: toRC [DS;D1] = toRC [LD], s0_eq j: toRC (DS::D0^j) = toRC [D1], d0s_eq parent's z1_eq/z0_eq (const_unfold) none compiles (pass 3)
RIncs_eq constructor (re-parse an input up to toRC); spec case = one rewrite; Example sweep_LS01 new the only place it is used is Lemma C, after the eater's L-run compiles (pass 3)
Lemma A RIncs_Inc parent's RIncs_Inc X1/C1 counts as in the twin; drop z1/z0; new Z case by inversion to IS; new EQ case from the IH to do (direct port)
Lemma U (with the R0-on-[] convention, Inc and EQ-free RIncs have at most one derivation per instance; Lemmas A and B respect the convention) none new: mutual induction, inverting the second derivation. In Rocq, the convention is easiest as a predicate on derivations, or as a variant RIncs' without Z on [] to do
Lemma B: totality on S-free words, at most one stray parent's Inc_total, RIncs_nxt_1 new: well-founded induction on (length, #LD) to do
Lemma C good_sweep, Lemma D good_next_iff none new; C: n × X1, one EQ, B2; D iterates Lemma A, uses Inc_ld and the "1 or L" lemma for Inc outputs to do
threshold θ (existence, monotone, well defined by U) none new; or avoided if J is stated relationally, on the derivation that Lemma A builds to do
V and V1/V2 (Inc is +1 on V; affine law) none new, elementary to do (informal proof in §3.3.5)
Lemma T 2θ ≤ V* − 1 (x ends with 1) none conjecture, exhaustive to 11 tokens open
closure of J = J4 ∧ K (the parent's key/domain) parent's key does not transfer (§3.3.5) K not found; J4 alone is refuted open (fatal)
nonhalt parent's skeleton P := canonical ∧ #S ≤ 1 ∧ G ∧ J, possibly a later start blocked

7. Evidence

Run python3 -B check_proof.py in this directory. The default run takes about 23 s and goes from blank to 1e8. --full (about 10 min) goes to 1e9, uses bigger samples, runs the abstract orbit for 3,000 sweeps and adds the Rocq check. All numbers below are from --full (pass 3, 2026-10-10: ALL PASS, and the default run is ALL PASS too). Simulation is evidence only.

claim instances result
Per-token transduction (h/h' on L, 0, 1, and h on S0, S1, SL), compared with the parent and TM7 9 rows the twin differs from the parent exactly at (L,h') and (SL,h): [h,h'] vs [h,h',h]
L entry, eater and drain, twin (6j+9, 6j+8) and parent (6j+13, 6j+12): every X ≤ 5 digits plus 150 random 514 each, 4 cases all pass
§3.1: each R/Inc derivation's pass list on the real machine (exhaustive w ≤ 3 tokens over {L,0,1,S}, k ≤ 6, plus 3,000 random) 2,829 derivations all pass; F never reads 1
BigStep: S(w) -+-> S(sweep w) on the real machine, random w 1,243 (1,088 leave a stray) all pass
From blank to 1e9: consecutive boundaries follow sweep (canonical re-parse) 277 sweeps 277/277; last boundary 991,375,720 = S(L^2009 1LS1111); the parent's rules reproduce 1
Initial segment c0 -(5)-> S(1) 1 pass
8a Lemma A, same tape (exhaustive r ≤ 5 tokens with ≤ 1 S, k ≤ 8, plus random) 14,379 all pass
8b Lemma B (B1–B3 exhaustive S-free r ≤ 8 tokens, k ≤ 10; B4 all words ≤ 6 tokens with ≤ 1 S) 111,349 all pass
8c Lemma C: G(w) gives L^n E_0(x) with ≤ 1 S, equal to the real machine's sweep (tails ≤ 5 tokens, n ∈ {0,1,2,3,5,8,13}) 1,893 all pass
8d Lemma D: G(w') <-> E_(n+a)(x) S-free (same words) 1,893 all pass
8d threshold monotone: E_M(x) S-free implies E_(M+1)(x) S-free (S-free x ≤ 7 tokens, M < 48) 157,056 all pass
8e G at every boundary: abstract orbit / from blank to 1e9 3,000 / 278 all hold
8e along the orbit: x_s ends with token 1; 2θ(x_s) ≤ N_s (max ratio 0.962, sweep 27, N = 131, θ = 63); V + leading L's ≤ 1.25 N_s 3,000 all hold
8e along the orbit: V(x_(s+1)) = N_s - θ(x_s) 2,999 holds on 2,813
8f G is not closed: 1001 -> LS001; 181 of 1,893 words with G lose it 1 + 1,893 as stated
8f J0, J2 and J3 not inductive: counterexamples (00010001, 5), (L1111, 60) and (L11, 4) of §3.3.5 3 as stated
8f one J0 step with margin ≥ 4 keeps θ(x') ≤ N' (S-free x ≤ 7 tokens, margins 4–39) 117,792 all hold
8f the margin can drop below half: (L11111L, 26) gives margin 12 1 as stated
Abstract orbit from S(1) 3,000 sweeps stays in the domain, at most 1 stray
9a Lemma C with EQ: every G word (tails ≤ 6 tokens, n ≤ 15) sweeps with ≤ 1 S; without EQ the 16 clauses have no derivation for 75 of them (first LS01) 15,593 all pass; the 75 strict failures equal the real machine with EQ (75/75)
9a LS01: strict derivation fails, EQ gives LLLL01 = real machine = Example sweep_LS01 1 as stated
9b Lemma D: an S-free x(w') contains a 1 or an L, and n' ≥ 1 (the words of 9a) 14,528 all pass
9c J3 + (N ≥ N0) refuted by (2^(m+1)−4, 00001) → 1 0^m 1, 2θ' = N'+1 (m = 4..20; brute-force θ for m ≤ 10) 17 as stated
9d orbit: max (V + lead)/N = 1.25 exactly, at sweep 2 (N = 4, x = 101) 3,000 as stated
9e V1: Inc adds 1 to V* (S-free words ≤ 8 tokens, exhaustive) 9,841 all pass
9f V2: V*(drop_a E_N(x)) = N + c(x) for N = θ..θ+11 (S-free x ending with 1, ≤ 7 tokens, exhaustive) 13,116 all pass
9g Lemma T (conjecture): 2θ(x) ≤ V*(x) − 1 (S-free x ending with 1, ≤ 11 tokens, exhaustive) 88,573 all hold; 68 tight (2θ = V* − 3)
9g T tight on 1 0^m 1; false for 100000000L; pure-binary c(x) ≤ |x| (≤ 11 tokens); L-driven c examples 1 + 2,047 + 1 as stated
9h orbit: V(x_(s+1)) = N_s + c(x_s); T at every x_s; for s ≥ 27, 0.952 ≤ V/N ≤ 1.193 and c ≤ 0.215 N 2,999 / 3,000 all hold
9i J4 not inductive: (257, 10000000L1) → (259, 0100000LLL01), V* = 642 > 519, θ' = 94 1 as stated
9j 400 random J4 states (N ≥ 131, biased to V* ≈ 2N), 25 sweeps each: θ ≤ N throughout 400 (10,000 steps) all hold; max V*/N from the third state on 1.437
Rocq (not simulation): scripts/TwinSpec.v: Inc_spec + RIncs_spec (mutual, 16 clauses + RIncs_eq), s1_eq/d0s_eq/s0_eq, BigStep, init, Example sweep_LS01; Coq 8.20.1, unmodified busycoq 1 file compiles (3.7 s); 5/5 Print Assumptions closed

Gaps: the closure of §3.3.5 (fatal: Lemma T is a conjecture and K is not found) and therefore nonhalt. Ground rule 3 applies: nothing here is a kill.

AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).

Review log

2026-10-10: skeptic review of pass 2, answered in pass 3

Verdict received: not sound: 1 fatal gap and 5 minor ones. Each gap, and what changed:

  1. FATAL. There is no inductive invariant (§3.3.5, §5). Still open; the status is STUCK. - The line "J3 with N ≥ N0 is untested" is replaced by its refutation, (2^(m+1)−4, 00001). Check 9c covers m = 4..20, with brute-force θ for m ≤ 10. The reviewer's θ ≤ N variants are recorded too: (428, 10000000LLL1) and (439, LL11111111LLL1), re-run here. - Following the reviewer's advice, the next candidate was tested by starting inside it at large N (check 9j), not only along the orbit. - New in this pass, the weighted value V*:
    • V1 (Inc is +1 on V) and V2 (the sweep is affine, V(x') = N + c(x)) are proved.
    • Lemma T (2θ ≤ V* − 1 for words ending with 1) is a conjecture, exhaustive to 11 tokens.
    • J4 (ends with 1 and V* ≤ 2N+1, a count-only condition under T) is refuted at (257, 10000000L1). It is a strong attractor, though: 400 starts × 25 sweeps never leave the domain.
    • The open problem is now stated as: prove T, and find a shape condition K on the L positions that bounds c(x) and is preserved.
    • J4 does not need the reviewer's suggested lower bound V ≥ N/2.
    • The 9c family stays inside J4: V(x') = 2^(m+1)+1 ≤ 2N'+1. The reason is that J4 bounds θ through V, not through N.
    • V2 also gives V*(x') = N + c(x) > N after every sweep, because c ≥ 1 on every word up to 9 tokens.
    • What breaks J4 is the shape, not the size: an L near the top.
  2. Minor. Lemma C's re-parse is needed inside the derivation. Fixed. - RIncs_eq added to TwinSpec.v. Its spec case is one rewrite. Also added: s1_eq, s0_eq, d0s_eq and Example sweep_LS01; all compile, with 5/5 Print Assumptions closed. - Lemma C now gives the derivation step by step, with EQ exactly once, after the n X1's and before the tail. Lemma A has the EQ case. - Check 9a reproduces the reviewer's count, 75 of 15,593 strict failures. With EQ, all 15,593 G words sweep, and the 75 failures match the real machine.
  3. Minor. Lemma D did not show that x(w') contains a 1 or an L. Fixed. - The argument is added: a ≥ 1, and every Inc output contains a 1 or an L. - Check 9b.
  4. Minor. G and P did not carry "canonical" and "at most one stray". Fixed. - Both are now conjuncts of G (§3.3.3) and are written out in P (§5). - The configuration-level re-parse and B3 re-establish them after each sweep.
  5. Minor. "Functional" R and Inc lacked a determinism lemma. Fixed by Lemma U (§3.3.1). - Under the convention "R0, not Z, on []", Inc and the EQ-free R have at most one derivation per instance, strays included. The proof is syntactic. - Lemmas A and B respect the convention, so "the" output is meant syntactically. EQ is used once per sweep, on a derivation that is never compared. - §1 and §6 are updated. The machine's own determinism is not used: sideRL quantifies over all left halves, so it is not obviously functional.
  6. Minor. The orbit claims overstated the evidence. Fixed. - The text now says "the first 3,000 sweeps (and 278 from-blank boundaries)". - The 1.25 bound is attained exactly at sweep 2 (N = 4, x = 101), so J3's constant has no slack (check 9d).

Also changed: the AI-assistance line now uses the standard disclosure wording.

Validation (pass 3): python3 -B check_proof.py (23 s) and --full (10 min) are both ALL PASS, including Rocq with 5/5 closed. The numbers are in §7. Status: STUCK, because the fatal gap remains.