/machines/1RB0LD_1RC0RD_1LA0RC_1RE1LB_1LF0LA_---0LE/study.md · raw

Funded mechanism study — 2026-10-14

The study found two exact families of left-edge returns and an executable word-rewrite model that reproduces every saved early return. It did not find a closed whole-tape invariant or prove nonhalting. The main remaining problem is describing the relation between the changing word and its far endpoint; short factors and a length residue do not capture that relation.

The approved stage was at most 30 minutes, from 10:06:30 to 10:36:30 PDT. No Coq work was started. The earlier billion-step blank run remains finite evidence only. No pseudo-random arithmetic map was extracted, so the machine is not being classified as a confirmed cryptid.

Two parameterized return rules

The head starts in state B at cell 0. Each displayed word occupies a fixed finite window beginning at cell 0. Superscripts mean repetition of the entire parenthesized word. At the end the head is at cell −1, which is the first visit to any cell left of the window.

All reads before that exit stay within the stated window. Therefore the rules allow arbitrary tape contents outside it. These are informal compositional results backed by exact finite component checks, not Rocq theorems.

Rule Before After, in the same window Exit state Steps Range
R1 010 (110)^n 0100 00 (101)^(n+1) 01 A 20n + 41 n ≥ 1
R2 010 (110)^n 101100100 100 (010)^(n+1) 110101 B 12n + 69 n ≥ 0

R1's window has 3n+7 cells; R2's has 3n+12 cells. R1 does not include n=0: that input first exits left in state D after 13 steps. R2 does include n=0.

R1 includes the previously checked 81-step window at n=2. In the saved blank run, R1 also explains a 121-step return at step 669. R2 explains the 129-step return at step 795 and the 105-step return at step 1,026.

Together with the old 5-step and 11-step windows, these families cover 1,027 of 1,282 saved consecutive left-record gaps. The other 255 gaps still require iteration of the word-rewrite model below. This coverage count does not imply that the two families close under their own outputs.

Why the formulas hold

Each component below has a complete transition trace in study-20261014/parameterized-returns.json. The input and output words occupy the same offset interval, with the initial head at offset 0. Every read is inside that interval.

Component State Offsets Before → after New state/head Steps
Start B 0..3 0101 → 1101 B at 2 6
Right loop B 0..4 01101 → 10101 B at 3 7
Right turn B 0..4 01100 → 10101 E at 5 7
First turn E −5..2 10101100 → 11010101 E at −4 32
First left loop E −3..1 01110 → 10101 E at −3 13
First left boundary E −3..1 11110 → 10101 E at −3 15
Exit to A E 0 1 → 0 A at −1 1
Second turn B 0..9 0101100100 → 1010110101 E at 0 60
Second left loop E −2..0 011 → 010 E at −3 5
Exit to B E −2..0 111 → 100 B at −3 3

For R1, apply Start, then Right loop n−1 times, then Right turn. The head is now E at cell 3n+4. First turn moves it to 3n; the tape is

111 (011)^(n−1) 1010101.

First left loop applies n−1 times, moving E to cell 3. First left boundary moves it to cell 0, and Exit to A makes the first left exit. The word replacements give R1's output, and the elapsed time is

6 + 7(n−1) + 7 + 32 + 13(n−1) + 15 + 1 = 20n + 41.

For R2, apply Start and then Right loop n times. B is at 3n+2. Second turn leaves E at that same cell. Second left loop applies n times, moving E to cell 2 with 111 in cells 0..2. Exit to B makes the first left exit. The replacements give R2's output, with time

6 + 7n + 60 + 5n + 3 = 12n + 69.

The loops are word concatenations of the checked local components, so their justification does not depend on extrapolating the sampled n values. As a separate implementation check, the study replayed 263 parameter instances up to n=1,024. Root independently checked both families on smaller and larger n values, including arbitrary values of two cells on each exterior side; the shared receipt is coord/audits/2026-10-14-funded-rule-samples.json.

A complete executable rewrite relation

Removing intermediate A, C, D and F visits gives a relation between configurations whose state is B or E. A variable-length C sweep is represented by the length of its run of ones. This is an exact reduction of the transition table, not a proof that the resulting relation always returns or avoids its failure branch.

The following table again uses offsets relative to the initial head. For the two variable rules, r ≥ 1.

State Offsets Before → after New state/head Steps
B 0..1 11 → 01 B at 0 2
B 0..1 10 → 01 E at 2 2
B −1..1 100 → 101 B at −2 4
B −1..1 000 → 101 E at 0 4
B 0..r+2 0 1^r 01 → 1 0^(r−1) 101 B at r+1 r+5
B 0..r+2 0 1^r 00 → 1 0^(r−1) 101 E at r+3 r+5
E −1..0 10 → 01 E at −2 2
E −1..0 01 → 10 B at 0 2
E −2..0 011 → 100 E at −1 3
E −2..0 111 → 100 B at −3 3
E −1..0 00 → 01 F at −1, reading 0 1

The last row reaches the undefined F0 transition. It is the explicit safety condition that a future invariant must exclude.

The implementation is astra/study_282_word.py. Its 550,698 rewrites through two million steps match an independent microstep implementation and all 1,283 saved C-simulator left-record configurations, including the gaps not covered by R1/R2. The whole finite tape, state, head and step number agree at each saved record. Root independently verified 32,768 local contexts plus 12 long-run contexts; see coord/audits/2026-10-14-line282-independent-rewrites.json.

Only run lengths r=1 or r=2 occurred in that finite blank orbit. The B/10, B/000 and E/00 branches did not occur there. Those absences are observations; they have not been established as invariants.

The remaining obstruction is a language, not a missing simulation

A first candidate language used observed 18-cell B-prefixes, observed interior 12-cell factors, and terminal 01. Twenty thousand constructed words passed the initial, weaker check for a return and preservation of interior factors. Adding the actual boundary checks invalidated the proposed language.

The shortest counterexample in the enumerated lengths 18..20 is

B at 0: 01011011011011001001
    121 steps
A at −1: 000101101101101101011   (cells −1..19)

The input satisfies the fitted prefix, internal-factor and terminal conditions. The output ends in 11, so the language is not closed. This is a constructed input, not the blank run, and it does not halt. Its full first-return trace is in study-20261014/boundary-counterexample.json.

Adding a length residue modulo 6 does not repair the endpoint condition. For example,

B at 0: 0101101101101011001001
    105 steps
B at −1: 01000100100100101101011   (cells −1..21)

This input has length 22, or 4 modulo 6. The identical initial 18-cell prefix occurs with every residue modulo 6 in the real saved records. The output still ends in 11. Root independently checked both examples; receipts are in coord/audits/2026-10-14-study-counterexamples.json.

State/head-marked factor candidates at widths 8 and 12 also fail a local closure check. Their concrete 3-step E/111 rewrites create unobserved pure-bit factors. A separate width-8 experiment that leaves the bulk unconstrained reaches an abstract E/00 case after 152 refinement rounds. These tests reject those particular abstractions; they neither prove a reachable halt nor rule out a stronger regular-language invariant.

Crossing sequences provide another measure of the unresolved repeated sweeps. The 1,282 observed returns use 730 distinct crossing sequences and 819 observed cell relations; the longest sequence crosses one boundary 100 times. That is a finite diagnostic, not a proof that the required transducer has infinitely many states.

Recommendation and artifacts

Pause at the end of this funded stage. The useful next stage, if prioritized, is a word-language invariant with explicit boundary phases or markers, using the two return families as lemmas. Longer blank simulation and formalizing the existing finite cases would not resolve the missing closure/safety argument. Overall mechanism confidence remains low; confidence in the checked local rewrites is high.

The scripts are astra/study_282_word.py, study_282_returns.py, study_282_language.py, study_282_boundary.py, study_282_phase.py, study_282_local_invariant.py, study_282_head_closure.py, and study_282_crossings.py. They use owned files only. Heavy runs used one worker at a time, nice -n 10 and a 6,000,000-KiB virtual-memory cap; available-memory and load guards were within the shared limits.