/machines/1RB0LD_0RC1RA_1LD1RC_1LE0RF_---1LA_1LF0LA/study.md · raw

Funded mechanism study: line 593

The periodic bulk and its right boundary now have an exact uniform roundtrip rule. The remaining obstacle is a safe language for the changing left-edge word. No whole-machine nonhalting invariant or Rocq proof is claimed.

This was the user-funded 30-minute mechanism stage beginning 2026-10-14 at 10:06:30 PDT, with a hard deadline of 10:36:30 PDT. The study did not extend the previous direct-simulation record; it analyzed returns within the existing 100-million-step prefix.

Main result

Use ordinary tape strings in left-to-right order. C> reads the first cell on its right; <A reads the last cell on its left. All unspecified exterior cells are unchanged until the displayed endpoint. Let the following fixed words have lengths 51, 51, 51, 24, 70, and 94 respectively:

P = 110011011110110011111001111011011111011101101111111
Q = 101111111011111110111011101101101110111101111101111
R = 101101101110111101111101111101111111011111110111011
G = 101111111011111110111011
W = 0111111111111101101111111111011111110111111111011011111011101101111111
T = 1101100111101101111111100111101101111101110110111111111011001111011011111111001111011011111111

For every nonnegative integer n, the following composed rule is valid, provided the eight cells immediately to the right of T are blank:

G W C> P^n T 0^8  -->  <A P^(n+2) T
steps = 906n + 2881

The initial head is at offset 94 relative to the start of G. The final A head is at offset -1, immediately left of the displayed output. That final cell is not read by the rule. The rewrite preserves length after accounting for the eight consumed blank cells: both finite sides have length 51n + 196.

This is an exact mathematical composition of three confined finite runs. It is not a Rocq certificate, and it does not show that the left edge always returns to the input form.

Why the rule works

Component Rewrite Steps Cells read relative to its finite input
Right-moving front W C> P -> R W C> 705 0..120
Right reflection G W C> T 0^8 -> <A P^2 T 2881 0..195
Left-moving crossing Q <A -> <A P 201 0..50

In the third row A initially reads the last cell of Q. In the first row the final C has moved just beyond W; that next cell has not yet been read.

Write Q = G B, where B is its final 27 bits. Then R = B G, hence G R^n = Q^n G. Repeating the right-moving rule n times, reflecting once, and repeating the left-moving rule n times gives the displayed roundtrip in 705n + 2881 + 201n steps. This identity resolves the phase alignment between the observed 51-cell words.

Every component transition, including read positions and state changes, is saved in study/local-certificates.json. Run python3 -B astra/study_593_rules.py to regenerate that certificate. Independent root checks also replayed the composed rule for n = 0, 1, 2, 3, 7, 16, 32 with all sixteen choices of two exterior bits on each side. Exact state, head, whole tape, step count, and read confinement matched. Those finite checks supplement the composition argument; they are not an unbounded formal proof.

What the actual left returns show

All 792 new-left records through 100 million transitions occur in A on a blank cell. From record 101 through record 792, all 692 tapes admit an exact factorization:

0 w P^n T

Here w retains every bit of the irregular edge; P is chosen as its longest consecutive run in the tape and the same 94-bit T works in every case. These are observations of the blank orbit, not a claimed invariant. The prefix and the bulk exponent both change.

The left record phases simplify further. Even records have a leading (011)^k; odd records have (110)^k. Removing that prefix leaves 346 distinct residual words per phase, with lengths 89..257 and sampled k between 3 and 26. Every sampled odd-to-even return takes seven steps, explained by the confined rule A> 011 -> <A 011.

The maximal P exponent is not monotone. At record 324 (step 9,782,908) it is 57; at record 325 (step 10,056,729) it is 56. The visited tape has still grown. Consequently, a proof cannot simply take the maximal visible P exponent as an increasing measure.

Across the 691 complete returns starting at records 101..791, 615 never reach the P run, two enter that run without reaching T, and 74 reach or pass the right tail. A fixed local-window return rule would miss those long excursions.

Exact executable word model

astra/study_593_edge_model.py keeps the whole irregular word and performs ordinary transitions there. It replaces a matching bulk excursion by the uniform rule above. It matches all 792 left records from an independent primitive C implementation, including every tape bit, exact times, absolute positions, visited endpoints, and the maximum position touched between left records.

The 100-million-step comparison used 1,123 bulk excursions, skipped 97,942,261 primitive transitions, and executed 2,057,739 primitive transitions in the unresolved region. This model is useful for further grammar work. It is not a decider or a nonhalting proof.

The left-edge reduction

The executable model also has a complete A/C word-rewrite version, astra/study_593_reduced.py. Its local rules eliminate B, D, E, and F excursions. Undefined E0 is retained as an explicit terminal branch; a pure F sweep into an entirely blank left tail is classified separately. The model matches the same 792 primitive-C records and all five constructed halting witnesses. Its complete case table is saved in study/word-rewrite-rules.json; head offsets and terminal E0 branches are explicit.

One half of the even-record return is uniform. With A on the first displayed zero and blank cells to the left:

A> 0 (011)^k 00 v  -->  A> 0 (011)^(k+1) 1 v
head displacement = -2
steps = 10k + 12

The right word v is arbitrary and is never read. The finite certificate includes the two new blank head cells on the left. The first return takes 10k+5 steps: a C sweep crosses the isolated zeros, reflects at the final 00, and an A sweep repeatedly applies 101 -> 110. The next seven steps produce the second new-left record. study/left-repair-rule.json specifies the finite input and head offsets without shorthand.

The difficult branch can spend these leading blocks. Define L_k = 1(011)^k for k >= 1, the prefix after the initial rightward departure. When the head enters its final 1 from the right, the exact interface is:

Entry state Output word replacing L_k Exit Steps
A (110)^(k-1) 0111 A immediately left 3k+3
E (110)^k 1 A immediately left 3k+1
F (110)^k 0 A immediately left 3k+1

D instead returns control to the irregular word. With D reading the third cell, 0110 -> 1011 takes seven steps and leaves C on the fourth cell; 0111 -> 0110 takes four steps and leaves C just after the word. The first branch consumes one trailing 011 block from L_k. Its replacement 101 becomes part of the irregular word. These interfaces are confined finite runs or repetitions of the local 101 -> 110 rule. The root independently checked the parametric interfaces for k = 1..32, 64, 127 and all sixteen exterior contexts.

An instrumented primitive C run tracks those interface events, including the intermediate steps inside each D return. Across all 346 complete even-to-even returns beginning at records 100..790, the resulting counter prediction agrees exactly with the next observed prefix exponent.

For each sampled easy branch, k increases by one. For a hard branch, let d count the D returns that consume a prefix block, and let epsilon be one when the eventual left exit is A and zero when it is F. Then the next even-record exponent is k-d-epsilon. In this finite prefix the 173 hard branches have 98 A exits and 75 F exits; d is 0, 1, 2, or 3 in 120, 50, 2, and 1 cases respectively.

Combining a hard branch with its following easy branch gives:

k_next = k + 1 - d - epsilon

This is exact conditional accounting, not a closed arithmetic recurrence: d, epsilon, and the new residual word are determined by the word-rewrite execution. The unresolved proof obligation is a safe language or potential bounding cumulative prefix consumption and handling the k=0 boundary. The observation that d never exceeds three in this prefix supplies no universal bound. The initial blank orbit has not been shown to preserve such a language.

The full interface specs, event trace, and counter comparisons are in study/left-prefix-interface.json, left-interface-trace.jsonl, and left-counter-update-check.json.

Concrete failures of simple edge languages

Allowing an arbitrary w is false. The constructed configuration A> 0 11 P^2 T, with blank exterior, reaches undefined E0 after 477 defined transitions, at head -3. This configuration is not claimed to occur on the blank orbit. The root independently checked the endpoint and the saved first 100 transitions.

Adding a few observed leading blocks is still insufficient. The configuration A> 0 (011)^3 110011 P^2 T has the expected repeated prefix and no internal 000, yet it reaches E0 after 8,678 defined transitions, at head -14. study/language-falsification.json records this and additional witnesses.

A complete proof therefore needs a stronger language that includes the reachable irregular words, proves their closure under the return transformation, and excludes the A001 / C000 routes to E0. The bounded study has not established that language. No pseudo-random arithmetic recurrence has been identified, so irregularity alone is not used to label this a cryptid.

Recommendation and evidence

Prioritize a bounded left-word-language investigation using the exact bulk roundtrip and the word-preserving model. Do not start a whole-machine Rocq proof from the current family: its unrestricted-word version has explicit halting counterexamples.

Updated 2026-10-14T10:31:52.170323-07:00. AI assistance: GPT-6 Astra (OpenAI).