/machines/1RB0LC_1LC0RE_1LA1LD_1LA1LB_0RF1RA_---0RE/notes.md · raw

W5-6 · 1RB0LC_1LC0RE_1LA1LD_1LA1LB_0RF1RA_---0RE (740 line 88), observe notes

Date: 2026-10-13. Stage: PLAN §6 step 1 (Observe). Sheet class: Bell eats counter. Confidence: med.

Checks before starting

Table, starts and the family

start what it is status
A ours (740 line 88) holdout
B 1LB0RD_1LC1LE_1RA0LB_0RF1RC_1LC1LA_---0RD (its A..F = our B,C,A,E,D,F; no mirror) proved: IndBECv1.v Module Others nonhalt17, line 626 (vendor 0940bb9 and upstream 9cf9e88), solve_hlin_nonhalt (config_BEC 1000 3 B F [0] [0] [0;1])
C, D halt at step 4 -
E, F halt at step 1 / 0 -

No other 740 entry shares this table (all 1,440 renamings/mirrors of every start searched in the 740/778/eqv lists, verify/*.v and solved_index).

280 (1RB0LC_1LC0RE_1LA1LD_1LA1LF_0RB1RA_1LC---) is a different table with the same orbit: - 88's state B is entered by A0 and D1; 280 splits it: 280's B = 88's B entered by A0 or (via E0) 88's F reading 1; 280's F = 88's B entered by D1. - So the two runs coincide step for step as long as 88's F reads 1 (88 halts on F0) and 88's B entered by D1 reads 0 (280 halts on F1). Both machines are at the same tape at 1e9 (step 1e9, state A, pos -916, span -2286..1133, 2,395 nonzeros). - 280's own table: start F certified (IndBECv1 Eat1Digit nonhalt6, line 526); starts C and D are Eqv_v2 partners of 280 (lines 17309, 19379); start B and its F-mirror are an Eqv_v2 pair (line 8729). - One proof of the shared orbit that excludes both halting reads covers 280 too; listed as sibling with that caveat.

Simulation

Mechanism

Turn configuration (C has just turned left at the bell):

R(u, e) = 0^inf u <C 0 1^e 0^inf        u = w 1 (101)^k, k maximal

w is the counter, 1 a separator, (101)^k the middle field, 1^e the bell. enc(v) = v in binary, MSB first, digit 1 = 10, digit 0 = 00.

  1. Bounce (R1, R6). The head sweeps left through the middle field (CDA per block: 101 -> 011), increments the counter at its right end, sweeps right (EAB per block: 011 -> 101) and turns at the bell, which loses 3 cells: R(w 1 (101)^k, e+3) -> R(inc(w) 1 (101)^(k+1), e), steps 6k + 4t + 9 for clean w (t = trailing 1-digits). inc on a clean word is +1 (R1). Separators: 110 is transparent to the carry (R2); a lone 1 before a 00 digit lets the counter after it count until its top digit is 1, then it is a 110 (R3). On all 2,000 sampled real words inc does not depend on k or e (R6).
  2. Eat (R4, R5). When the bell is down to e = r in {0, 2} the next pass fills the middle field with 1s, increments twice and drops the counter's low end: - z = inc(inc(w)) ends in 00: R(p 00 ..) -> R(p 1, 3k+3+3[r=2]) (one digit eaten); - z ends in 10: R(q c 10 ..) -> R(q 101, 3k+2+3[r=2]) (the last 3 cells become a middle block). On clean counters this is R4: v = 2m -> enc(m+1); v = 2m+1 -> enc((m+1)//2) with a 1 101 tail (m+1 odd) or a 010 1 tail (m+1 even). R5 matches all 631 checked real eats (287 of the 289 eats of start A to 5.1e7, skipping the first two, whose counters are shorter than 4 cells; all 344 of start B to 4.2e7). Hence e mod 3 is always 0 or 2 (33,987 / 26,014 turns), never 1.
  3. Certified start B stays on the clean orbit R7: R(enc(s) 1, 3s) -> R(enc(s+1) 1, 3s+3) (s bounces, then an even eat). Only R1 and R4's even case are ever used, which is what the hlin certificate (side_binary_inc_rule on 10/00 digits) covers.
  4. Start A leaves that orbit: the bell and the counter value are not tied (s != e/3), odd eats happen (e = 2 mod 3 cycles), and the 010 tail turns into lone-1 separators inside w that move towards the low end and are eaten later. To 5.1e7: 90 of 289 cycle starts have a junk counter; 83 eats act on junk words, with 29 distinct junk-eat shapes. Every rule above still applies.

Halting analysis

Template check

Cryptid check (ground rule 6)

All updates are +1 on a binary counter, a digit drop and +3 on the bell. Which eat case fires depends on the low bits of the counter at the bell's end (a chaotic parity, as in W4-2 and W5-5), but there is no multiplicative or Collatz-like map. Not a cryptid candidate. Caveat: no invariant is known for the junk yet.

Open / next

Scripts and data

Wave 5, stage 1 (2026-10-12)

Run on 2026-10-13. Goal: find a regular counter-word language L that is closed under the bounce (inc) and the eat. Result: no such L exists, whether regular or not. Non-halting needs an arithmetic link between the counter and the cycle length (W4-2 / BECv5 style). Confidence: med.

1. No counter-word invariant (the stage goal is impossible)

bounces counter word at the eat
126 10101010101010
126 110101010101010
30 1011001010101010
14 101110010101010
6 10111100101010
2 1011111001010
0 101111110010

It ends at 10111111, where the bounce and both eats halt. - At least 12 bounces between eats, words up to 22 cells: a halt again, at the bounce of 1011111111010 (data/stage1/free_closure_min12.txt). There the cycles have about 1,000, then 255, 127, 63, 31, 15 and 14 bounces. - Any L that contains 10 and is closed under inc and both eats contains these words. So the plan from the observe stage cannot work. - The halting paths need the cycle length n to be far from the counter value v (n much larger than v, then n halving each cycle). In the real run n never decreases: n' = k + [r = 2] + [z ends in 00], with k = k0 + n. - A whole-tape regular language (CTL, MITM-DFA) is ruled out only heuristically. Pumping the bell keeps the counter fixed while n grows without bound, which is the n >> v regime of the paths above; I did not test the residue-class variant. - scripts/stage1/mitm_driver/ drives busycoq's MITMDFA decider (CTL.v, extracted unmodified) and reads DFA files. It returns true on CTLCertv1 tm28's certificate. It is ready for a later DFA attempt; none was tried, given the result above.

2. Token rules (validated)

Read the counter word left to right in tokens: digit 1 = 10, digit 0 = 00, F = 110 (frozen separator), S = a lone 1 followed by 00. scripts/stage1/tokrules.py checks four rules against exact simulation, on 400 random cases each (353 for T4), with 0 failures:

rule statement
T1 F is inert. inc(H 110 L) = H 110 (L+1); if L is all ones, the carry passes through F: (H+1) 110 0^len(L)
T2 S freezes on its first carry. inc(H 1 00 L) = H 1 00 (L+1); if L is all ones: H 110 0^len(L) (the carry stops there)
T3 Odd eat on clean z = H 1 0^m 1 (bits): w' = H S enc(0^m 1), i.e. S takes the place of the lowest 1 above bit 0; if m = 0, w' = H with k' = 1
T4 Even eat on clean z = p 0: w' = p

So junk is made of particles: - Each odd eat creates an S at the lowest 1 above bit 0. - The S turns into an F at the first carry into it. - Each F stays on its cells. Every eat brings it one digit closer to the low end, where it is eaten. - An F that reaches the low end is absorbed into the middle field at the eat (k0' = 1 or 2; a stack of F's gives a larger k0'). - An odd eat whose S would land inside an F (z = H F 0^m 1, m >= 1) leaves shift junk instead: an 11 pair, E, giving the word H 11 0^m 1. It clears within a few bounces. These are the 10 words of the run to 5.1e7 that do not tokenize (steps 5.30e6 and 1.14e7).

Of the 59,991 turn words that tokenize (to 5.1e7), each has exactly one tokenization. Junk shapes seen: F d, F F d, F d F d, S d, S, S d F d, F S, F S d.

3. Coupling between the counter and the cycle length

Here v is the live value (the digits only, with F and S skipped), n = floor(e/3) at a cycle start, and L = (|w| + 3k0)/2. - Over the 263 cycle starts after turn 500 (to 5.1e7): log2(n) - L lies in [-3.43, 0.55], and log2(n) - D - k0 (D = live digits) lies in [-2.39, 0.86]. - v/n lies in [0.24, 0.997], so v < n at every cycle start. With k0 = 0 the range is [0.575, 0.997]. The low values come from k0 >= 1, where the eat removed more than one digit. - In clean terms the cycle map contracts: v' - n' is about (v - n)/2. - T2 roughly halves v when an S freezes. The contraction then restores v/n over the next cycles.

4. Robustness of the real dynamics (no halts)

scripts/stage1/cyc.c is an exact TM runner that starts from a turn configuration. The real dynamics never halted from random starts:

starts start condition steps each halts
300 n/v in [0.8, 4]; F/S junk in the low 5 tokens 3e7 0
300 n/v in [0.05, 0.8] 3e7 0
300 n/v in [4, 40] 3e7 0
400 arbitrary 1-6-cell junk without 1111 planted at a random depth; n/v in [0.8, 4] 2e7 0

scripts/stage1/rstart.py and rstart2.py generate the starts; the results are in data/stage1/randstart_*.txt. Every start converges to the v/n band. So non-halting looks robust, and the dynamics are not cryptid-like.

5. Coupled closure (window on n)

scripts/stage1/cclos_*.c compute the closure of the cycle map when the adversary may pick any cycle length n inside a window tied to the counter. Each bounce and each eat is an exact simulation of the turn; the bounce is memoized at the word level. The window types: - size: 2^(D+k0-1.25) <= n <= 2^(D+k0+1.25), with D the live digits; - value: v-1 <= n <= 5(v+2), with v the live value. Unparsable words get a size window. The check also tests whether n' (from the real rule) lands in the successor's window.

window max cells cycle-start states halts
size 20 24,220 0
size 22 62,562 0
value 18 11,052 0
value 20 29,056 0
value, top F/S words on a size window 20 28,258 0

Results are in data/stage1/coupled_closure.txt. No value closure ever showed a bell residue of 1 (the size closures do not check it).

Window maintenance. The value window is almost inductive. On the 20-cell value closure (42.0M checks), n' leaves the window 2,875 times (0.007%). - 99% of the 18-cell exits (1,270 of 1,283, data/stage1/value_window_violations_18.txt) come from unparsable predecessors. - These are E words, H 11 0^m 1, made when an odd eat puts its S into an F (z = H F 0^m 1). - An E resolves within a few carries, mostly into FF. In doing so it can cut the live value by a factor of about 4: H = 1001, m = 4 gives an effective value of 65 against H·2^(m+1) = 288. The effective value is not a simple function of H (H = 100 gives a negative offset). - The other exits come from S at the top (z = 1 0^m 1 gives v' = 1 while n' stays large) and from F near the top.

So the invariant needs a value with pending-loss terms for S, E and a top F, or wider windows for those shapes. Ordinary F and S particles keep the window as it is.

Effective value (first try at the pending-loss terms). scripts/stage1/cclos_veff.c sets v_eff(w) = V(inc^J(w)) - J, with J = 2^ceil(|w|/2). After J bounces every particle has had a carry, so v_eff is the value the counter behaves as from then on. The window becomes v_eff - 1 <= n <= 10(v_eff + 2). Each state's incoming n' range is checked against its own window when v_eff >= 32.

max cells states states checked window exits
18 8,083 4,664 0
20 20,770 13,443 6

The 6 exits at 20 cells: 5 low (n' = v_eff - 3 at v_eff = 33..35, or n' = 1 handed on by exempt small states) and 1 high (not inspected). The lower ratio bound has to be 0.1 rather than 0.2: an S created high up over a small H (for example 10 00 S 00 00 00 00 00 10) leaves v_eff/n near 0.12.

The 2 bell-residue-1 events come from one exempt state with v_eff < 32 that was explored at n = 1. They are not real dynamics, since n only grows. So an effective-value window, with ratio in [0.1, 1] and a few units of slack at the lower end, is the candidate invariant. The open part is a closed form for v_eff per junk shape.

Validated / open

Wave 5, stage 2 (2026-10-12)

Run on 2026-10-13, about 2 h. Goal: close the effective-value window exactly and write proof.md. Result: the effective value now has an exact closed form and the bounce is understood at every length, but no closed window was found. Two of the planned window shapes are provably not invariant, and the weakest closed set computed so far depends on the word in a way that is not yet a formula. Outcome: still progress, confidence med. No proof.md.

1. Closed form for the effective value (validated)

Tokens as in stage 1: 10 = digit 1, 00 = digit 0, F = 110, S = a lone 1 together with the 00 after it (100). - A normal digit is a 10 or 00 that is not S's own 00. - The weight of a token is 2^(number of normal digits below it).

Phi(w) = sum of weights of the normal 1-digits  -  sum of weights of the S tokens

Why: the time until the first carry leaves a tail X, and the period after that, follow a recursion. A 1-digit keeps the time and doubles the period. A 0-digit adds one period and doubles it. F changes neither. S adds one period but does not double it, because S's 0 freezes into F at its first carry. Phi(w) = P(w*) - T(w) gives the formula above. It is exactly "a pending loss of one place value per live S".

Checks (scripts/stage2/phi.h, cclos_phi.c): Phi equals the simulated v_eff = V(inc^J w) - J on every parsable closure state, with 0 mismatches on 2,416 / 5,989 / 15,089 states at 16 / 18 / 20 cells. Words that do not parse (E junk, a lone 1 at the low end, 11 at the top) fall back to the simulated value: 842 / 2,094 / 5,681 states, needing at most 31 / 31 / 63 incs.

2. The bounce at every length (validated, with a cell-level argument)

G0 = canonical words in (10 | 00 | 110 | 100)*. On G0 the carry runs right to left: - C or D reading 0 writes 1 and goes to A. - A reading 1 writes 0 and goes to C (a 1-digit, now 01). - A reading 0 stops: 00 becomes 10 via B and E. - C reading 1 goes to D (the top cell of an F, now 101). - D never reads 1 inside G0.

The right sweep in E then restores 01 to 00 and 101 to 110. S never sees the carry, since the carry stops at S's own 00, which leaves 110 = F. So inc maps G0 to G0, never halts, and adds exactly 1 to Phi, at any length. An F that reaches the low end is absorbed into the middle field.

Exhaustive check (g0check.py 16): all 6,111 canonical G0 words up to 16 cells, 0 failures.

3. Windows that are not invariant

4. What is closed (bounded checks)

cells states transitions unsafe (halt or r = 1) g = 1 max g
16 5,722 3.1M 18 5,711 2
18 18,019 15.3M 69 17,974 4
20 56,845 76.0M 258 56,674 8

The real seeds lie inside the set. The states that need g > 1 are junk words with long runs of 1s (max at 20 cells: 101111111000010, g = 8). Max g doubles every 2 cells, so these words need about n >= 2^(|w|/2 - 6). Reading: nothing is dangerous unless a word carries a long 1-run while n is small next to its size. In the real run, Phi/n lies in [0.036, 0.99] over the 58 parsable cycle starts with n >= 20, up to step 9e5 (data/stage2/realcyc.txt). It never has a 1-run longer than 3 (stage 1: 111 in 6 words, 1111 never).

Validated / open

Funded stage (2026-10-10, stage3)

Run on 2026-10-13, about 2 h (Dennis 2026-10-13: "go with recommendations"). Goal: turn the computed closed set into a closed-form invariant (junk grammar plus a formula for g), test it as a window with 0 exits, then proof.md for 88 and 280. Result: no closed form, so the stage ends at its stop rule and W5-6 is parked (with 280). One new exact object was found: the junk grammar of the forward-least closed set. Confidence stays med. No proof.md.

1. Greatest closed set n >= g(w) at 22 cells

scripts/stage3/gfixl.c is stage 2's gfix.c with light storage: it keeps a transition only if its n2 is below a cap (256), which is exact because the final max g is below the cap. At 20 cells it reproduces stage 2 exactly (56,845 states, the same g values) in 24 s and 0.2 GB.

cells states transitions (with too-long) unsafe g = 1 max g
20 56,845 76.0M 258 56,674 8
22 179,610 380.6M 971 178,926 16

(data/stage3/gfix22_n1.out, the 684 states with g > 1 in data/stage3/g22_gt1.txt.) Max g doubles every 2 cells (2, 4, 8, 16 at 16 to 22 cells). The 24-cell run was stopped at 60,000 / 190,006 explored states (machine load above 28, stage budget).

g is not a function of the 1-runs. At 20 cells, 130 states with no run longer than 3 have g > 1, and 4,928 states with runs of 4 to 8 have g = 1. With L = a lone 1 (a 1 that is not part of a digit, F or S), the g > 1 words are all L-rich, mostly ending in F L L S 1 or L S S. The worst ones are 1 L^j S 0^i 1 (g = 8 for 1LLLLLLS01), and they are reached only along paths where n halves every cycle.

2. The forward-least closed set has a small grammar (new, exact up to 22 cells)

scripts/stage3/hmin.c computes h(w, k0), the least cycle length with which a cycle start is reached from the real seeds (data/stage2/seed50.txt) when every n >= h is allowed at every state. The set {n >= h} is forward closed by construction and contains the real orbit from the seeds on.

cells states transitions halts / r = 1 in G* n >= Phi + 1 min log2(h) - D
18 5,071 5.4M 0 / 0 all 3,943 / 3,943 -0.994
20 14,547 26.4M 0 / 0 all 11,021 / 11,021 -0.997
22 40,998 126.2M 0 / 0 all 30,242 / 30,242 -0.999

Here D is the number of digit tokens, and the Phi column counts the states where Phi has a closed form. The grammar is:

G* = (d | F)*  T        T in { nothing,  L (k0 = 1),  S 0^j 1 (k0 = 0),  L S 0^j 1 (k0 = 0) }

The real orbit agrees. To step 17,829,276 there are 204 cycle starts, all 204 in G*. n >= Phi + 1 holds on all 191 parsable ones after the first (data/stage3/realcyc_1.78e7.txt). L words are real: dL (9 times), dLSd (2), dFL (1). The first one is at step 223,794 (1000101000001, k0 = 1, n = 63). Their first bounce is not a word-level inc: it turns 1 0 1 1 0 0 L plus one middle block into 1 0 1 F 0 F 0.

3. Closed-form windows are not closed

scripts/stage3/swin.c runs the window closure with every n >= nlo(w) at every state. The full table is in data/stage3/window_tests.txt; at 18 cells: - Digit windows. 2^(D - C) has exits for every C from 1 to 4: 105 to 8,378. For C = 2 to 4 it also halts, along 101110 -> S0000001 (n = 209) -> 1LS000001 (254) -> 1LLS00001 (62) -> ... -> 1LLLLLLS1 (2). There n halves every cycle, which n' >= n forbids but a word-only window allows. Weighting S or L as digits gives more exits (up to 129,680). - The two bounds of §2 combined. max(Phi_eff + 1, 2^(D-1)) has 571 exits, and 397 with Phi_eff instead of Phi_eff + 1. - Adding the freeze bound for the fresh S (2^dS - 1 or 2^dS). 472 to 483 exits, plus 268 new states outside G. - Where the exits are. S-top words entered with n below 2^D: in the forward-least set h(S000001) = 64 = 2^D exactly, but the window lets n = 62 in, and that gives LS0001 with Phi_eff = 64 > n2. Also L-bottom words with n below their h: 1000000L at n = 29..36 gives S10001, S10010, ..., which are outside G. And F F .. L words at n = 4..8.

So the two bounds that hold on every reachable state (n >= Phi + 1 and n >= 2^(D-1)) are not inductive. What keeps the real set inside G* is a memory of the n at which the fresh S or the L was made. That n is about 2^(depth) and is not a function of the word. A closed invariant would have to carry it as a third coordinate, for example (w, n, n at the last odd eat), or a per-particle "time to freeze". That is a new design, not a formula for g.

Validated / open