Funded edge-return study — 2026-10-14

The funded study found exact local sweep identities, an exact reduced word interpreter, and three concrete edge-return families. R1 now has an informal universal derivation; R2 and R3 remain finite-tested candidates. It did not find a closed family of edge words or a whole-machine invariant. No formal proof or kill is claimed.

The initial observation used a long run to expose the period-seven bulk. This stage instead studied how a finite edge word changes between visits to the blank left boundary. Work was authorized by the study decision for the shared table family, with a maximum budget of 30 minutes ending at 10:36:30 PDT.

Conventions and separate starts

All formulas below use the line-6 orientation. A>u means that state A reads the first bit of u; the displayed zero in an edge word is part of that word. Exponents repeat the entire binary word. Unless a rule explicitly permits arbitrary exterior context, both exterior half-lines are blank.

The exact reflection and renaming is A→E, B→B, C→C, D→A, E→D, F→F. It maps line-6 blank A to line-348 blank E. The standard line-348 blank-A run instead corresponds to line-6 blank D.

The two starts reach the same kind of boundary, with different words:

These are separate finite initial-state obligations. No result for one blank start has been silently transferred to the other.

Two general sweep identities

These identities follow directly from the transition table. They are local mathematical derivations, not Rocq lemmas. Arbitrary tape outside the displayed window is unchanged and unread before the endpoint.

For every integer k ≥ 1, the right-moving rule is:

A>0 1^k 0  →  1 0^(k+1) A>       in k+2 steps.

A writes the first 1 and enters B. B erases the first 1 of the run and enters F. F erases the remaining k−1 ones, crosses the following zero, and enters A on the next cell. This proves the displayed step count and leaves the outside tape untouched.

For every integer n ≥ 0, the left-moving bulk identity is:

(1000000)^n A>1  →  A>1 (1001111)^n       in 17n steps.

For one block, number the cells 0 through 7. The input is 10000001, with A at cell 7; the output is 11001111, with A at cell 0. The exact state/position path is:

A@7 D@6 B@5 C@4 D@5 E@4 A@3 B@4 F@5
A@6 D@5 B@4 C@3 B@2 C@1 D@2 E@1 A@0

Here E@1 means state E at position 1, where the symbol is zero. It is not the undefined transition E reading 1. Every read lies in cells 1 through 7. Repeating this one-block computation proves the identity by induction on n.

The parent investigator independently replayed 160 instances of each identity: ten parameter values through 256 and all sixteen combinations of two exterior bits on either side. All state, head, full-tape, step-count, and read-footprint checks passed. Those are additional finite checks; the derivations above supply the general reasoning.

An exact reduced word interpreter

Eliminating forced visits to C, D, E and F leaves seven cases at A/B boundaries. Let the current head position be zero. Words in the middle columns list the specified cells in increasing position; all other cells are unchanged.

The script also applies the two sweep identities above as accelerations. It retains a literal transition fallback for non-A/B starts and stops inside a macro exactly when a requested checkpoint requires it.

The undefined E1 transition is never a defined machine step. The direct simulator represents it by an additional 1RZ tick, and the interpreter mirrors that convention only when comparing simulator output. In the dangerous A/111 case, two defined transitions reach the undefined entry; a reported third simulator tick must not be confused with a Rocq step.

Independent comparison with the earlier C evidence matched every full saved slow-edge configuration and the 100,000,000-step endpoint: 122 checks for line 6 and 142 for line 348. This validates a finite implementation trace. It does not prove that the dangerous case is absent forever.

Three concrete return families

Set P = 1111001. A return starts at 0^inf A>U P^n 0^inf and ends at 0^inf A>V P^(n+d) 0^inf. The output head shift is measured from the original head position. In the tested cases this is the first later A visit strictly to the left of the original boundary.

R1 is derived for every n ≥ 0 below. R2 and R3 remain candidate parameter families, with no universal derivation established. None is a Rocq theorem. The reduced interpreter and an independent C run agree at every tested endpoint: all parameters from the stated lower bound through 32, followed by 63, 64, 127, 128, 255, 256, 511, 512 and 1024. All 124 checks passed. First-return status was checked by the reduced interpreter; the independent C replay checked the exact endpoint and elapsed steps. A further independent literal-transition review checked 31 cases across the three rules, including previously untested parameters 33, 65, 129, 257, 1025 and 2048. It also checked the first-return condition, and all cases passed.

R2 and R3 require their lower bounds. At n=0, R2 returns after 222 steps with word 0101111100111100111 P^2; R3 returns after 206 steps with word 01011100101111100111100101 P^2. Both exception endpoints were separately replayed in C. Their head shifts remain −2 and −4 respectively.

These families occur in the actual line-6 run: R1 applies at step 83 with n=1; R2 at step 249 with n=2; R3 at step 1082 with n=5. Short exact prefix returns connect them. Beyond those cases the edge word continues changing, so this three-rule collection is not closed under iteration.

Universal informal derivation of R1

The fixed edge words in R1 are U = 01001111100101 and V = 0100111101110010. Define the additional words:

R  = 0111110       S  = 1000000       T = 1001111
L1 = 1001000100100000000
L2 = 100100010010100

For n ≥ 1, put m = n−1. The following table is a complete derivation. Blank exterior is implicit; every intermediate word is at the same absolute tape coordinates as its predecessor. A's displayed location identifies its scanned cell.

The 7m, 17m, 7n and 17n rows follow by repeated use of the general sweep identities. The remaining rows are exact finite computations, with their full transition paths recorded in evidence/study-20261014/R1-symbolic-certificate.json. All five finite pieces also passed 80 independent C-engine checks: each piece in all sixteen two-bit exterior contexts.

Indices in that table start at the left end of the displayed window. Every read stays inside its window, and no case reaches the undefined entry. Arbitrary exterior is therefore unchanged. The exit needs its three displayed left zeros; the right cap and the n=0 case need their displayed right zeros. The blank exterior of R1 supplies those guards.

Three word identities align the finite pieces with the parameterized blocks:

01 P^m               = R^m 01
01111 T^m 1001       = R^(m+1) 01
111 T^n 1001         = P^(n+1)

They follow by induction from the literal equalities 01 P = R 01, 01111 T = R 01111, and 111 T = P 111, together with their displayed zero-exponent cases. Thus the derivation does not infer the formula from sampled values of n.

The total time is:

33 + 7m + 10 + 17m + 20 + 7n + 10 + 17n + 24
= 97 + 24(m+n)
= 48n + 73.

For n ≥ 1, the bulk traversals stay at positions at least 15, and the setup and bridge never move into the negative region. The exit's transition trace has no earlier A occurrence at a negative position. The separate n=0 trace also has its first negative A occurrence at the endpoint. Hence this is a first-return identity as well as an endpoint identity, with head shift −3.

An independent review checked the configuration chain and guards, replayed all five finite pieces in the sixteen exterior contexts (80/80), and verified the three commutation and base word identities. Its receipt is coord/audits/2026-10-14-family6-R1-finite-bridges.json.

This proves R1 informally for every n ≥ 0 under its stated blank-exterior guards. It does not show that the evolving edge remains in R1's domain, does not prove R2 or R3 universally, and does not establish nonhalting.

Exact bounded prefix rules and the obstruction

A symbolic exploration starts with blank cells to the left and A>01…, branching only when it first reads a new unknown bit on the right. It stops at the first A visit to a negative position. At a width limit of sixteen input bits it yields 473 exact finite prefix-return computations and 1,914 unresolved branches that require another input bit. No branch hit the step cap or reached E1 within this bounded tree.

For example, for an arbitrary untouched tail r:

0^inf A>0101 r  →  0^inf A>0100111 r

This takes eleven steps and shifts the head left by three. All 473 rules were independently replayed in C with each of three tails: empty, 111111, and 010101. All 1,419 endpoint checks passed. The symbolic paths show that those tails are unread; the C tests are supporting checks rather than a proof over all tails.

The rules explain 22 of 37 consecutive observed A-edge returns for line 6 and 24 of 45 for the reflected line-348 start. The final checkpoint for each start has no next recorded return and is excluded from those denominators.

A sixteen-bit prefix alone is insufficient. At line-6 steps 83 and 249 the first sixteen bits are both 0100111110010111, but the next A-edge returns take 121 and 822 steps. This is not a refutation of a model that also records the bulk count and the remaining edge word: the R1/R2 families show why those extra data matter.

Removing the maximal suffix P^n from the sampled edge words leaves a changing prefix of 121 bits at the final line-6 edge checkpoint and 141 bits at the final canonical line-348 checkpoint. No bounded list of edge shapes, symbolic word grammar, or update law for these growing prefixes was established. That is the outstanding proof obligation, together with excluding A/111 for every future reachable edge.

Recommendation and evidence

Keep whole-machine formalization parked. A further funded stage would need to derive a closed symbolic transformation of the variable edge word, including the small-bulk exceptions, and prove that the reachable word language excludes the unsafe case. Extending simulation horizons or collecting more fixed-prefix rules alone does not discharge that obligation. No pseudo-random arithmetic recurrence was established, so there is no confirmed cryptid classification.

The principal machine-readable results are in evidence/study-20261014/: R1-symbolic-certificate.json, parametric-return-rules.json, prefix-return-rules.json, prefix-return-validation.json, transducer-validation.json, and result.json. The implementation scripts are astra/study_family6_transducer.py, astra/study_family6_prefixes.py, astra/study_family6_validate_prefixes.py, and astra/study_family6_parametric.py.

An additional adversarial-input probe tried 1,024 reproducibly sampled 64-bit constructed words for 100,000 steps each and found no halt. These inputs are not claimed reachable from either blank start, and this negative probe supplies no invariant; its receipt is retained only as research provenance.

AI assistance: these observations, scripts and checks were produced with the help of GPT-6 Astra (OpenAI).