Line 593 funded invariant study

The study proved internal safety with an unlimited prefix and derived an exact word/counter model covering the real zero-reserve cases. The blank-tape machine remains open. Its unresolved obligation is now precise: exclude an A return exactly when the finite prefix reserve is exhausted, or prove that the computation takes the safe infinite left escape.

This report preserves the earlier mechanism study in ../study.md and ../study/. The funded interval began at 12:59:26 PDT and ends no later than 13:59:26 PDT on 2026-10-14. Updated 2026-10-14T13:41:41.066482-07:00.

What is now proved locally

At each reduced A/C boundary, suppose the tape strictly left of the head contains no adjacent zeros. Eight exhaustive local rules preserve this condition. The hazardous windows A001 and C000 violate it. This gives nonhalting for an arbitrary right word with an infinite 011 reservoir on the left.

The complete argument is formalized in ../LocalSafety.v. The premise fails on blank left tape, so this theorem is explicitly not a blank-start nonhalting theorem. Root also formalized the uniform bulk roundtrip in ../LocalBulk.v, the sweep schemas in ../LocalSweep.v, and the local prefix interfaces in ../LocalRules.v. Their assumptions are closed; independent kernel receipts are maintained by root.

The run-sweep derivation is order-sensitive. A one-run is split into groups of three, emits 011 blocks, and either continues left or turns C right. A right turn can increase the preceding one-run before that run is scanned. Counts of run residues therefore discard information used by the next return. The precise schemas and finite checks are in run-sweep-schemas.json and run-sweep-samples.json; an independent checker replayed 17,120 instances with arbitrary two-bit exteriors.

The exact finite-reserve reduction

normal-form.md defines N(k,w)=A>0(011)^k w and gives every branch. It includes blank start as (k,w)=(0,empty).

The virtual core processes the full word w independently of k. A D call with right bit zero consumes one prefix block; a D call with right bit one returns without consuming one. If it terminates at the interface, record its consumption d, exit state s, and output word v.

• If the core asks for more than k blocks, the real machine enters F on a blank left tail and moves left forever.
• If s is A and k=d, the real machine reaches E0 two transitions later and halts.
• All other terminating cases return to the normalized section. A with one block remaining and F with no block remaining need one-return boundary rules. E with no block remaining still has a regular two-return rule and regenerates at least one block.

The zero-reserve entry convention is exact: A00 reaches the same state as the first five virtual C steps in only two steps. This supplies an accounting offset of -3, not a negative transition sequence.

astra/study_593_normal_form.py reproduces all 792 saved primitive records from blank start, including every tape bit up to blank-tail equivalence, absolute head positions and times. Its 399 normalized steps comprise 393 two-return steps and six one-return boundary steps. The last saved record is at step 98,148,758, head -792, reserve 25. This validation establishes the observed agreement; the general reduction is supported by the local compositional derivation, not by extrapolating those records.

The core interpreter independently passed 1,914 full-configuration comparisons after a right-span bookkeeping error on the empty word was fixed. The expanded finite-reserve classification independently passed 2,087 cases, including 336 halts, 152 certified escapes and 1,599 returns. These are constructed tests, not additional blank-tape decisions.

The independent normal-form review checked 2,482 constructed cases (2,214 distinct input pairs), with zero skips or mismatches. It compared every tape cell, state, head position and time for 4,289 emitted A-return records, 154 E0 halt endpoints and 22 F0 escape endpoints whose entire left tail was verified blank. The cases cover exhaustive short canonical words, seeded random inputs, the lookahead families and bulk shortcuts; the literal checker executed 480,485 transitions. This finite review validates these implementation cases, not a universal normal-form theorem or a blank-start classification.

A clean remaining proof target

Away from the explicit boundary restarts, canonicalization gives a word-only two-return map. If c counts leading 011 blocks absorbed into the next reserve, its debit is

delta = d + [exit=A] - c.

For cumulative debit D_i, a sufficient invariant is a bound on D_i + threshold(w_i), where the threshold is d+2 for A, d+1 for F, and d for E, together with the entry-domain condition. Below the threshold, the exact boundary rules can change the word trajectory. The model therefore does not claim that one word trajectory works for every reserve forever.

The final one-return boundary in the saved prefix ends at record 32, step 5104, head -32. Its normalized seed has reserve 1 and the following 81-bit word:

111001111011001110111011101110110111111111011001111011011111111001111011011111111

The next 380 observed normalized steps all lie in the common two-return domain. Their required initial reserve is exactly 1. This yields a concrete future target: prove the infinite supremum of cumulative debit plus threshold is at most 1 for this seed. The present evidence only establishes the finite prefix through record 792.

Precise obstructions

Simple run constraints are insufficient. The constructed configuration A>0(011)^4 1111 P²T has no internal 000 and no isolated one-runs, but reaches E0 after 108,338 defined transitions. Its halt was independently replayed. It is not a state asserted to occur from blank tape.

A stronger obstruction is universal. lookahead-obstruction.md derives two families of right words sharing arbitrarily long prefixes. With a single remaining prefix one and blank tape farther left, one family halts and the other takes the infinite F escape. Both can satisfy the same simple run constraints. Independent literal checks passed 6,336 cases with sixteen exterior contexts, exact tape/head/time agreement and read confinement. ../LocalObstruction.v formalizes these opposite outcomes uniformly in the parameters and arbitrary unread suffixes. No fixed left window can classify the relevant arbitrary core inputs.

The complementary potential study gives 16 exact rational certificates excluding specified additive monotone potentials built from small subword counts, run residues, and related features. Ordered prefix/suffix/subword debts with the tested bounded coefficients also fail. These conclusions exclude only the stated families; they do not exclude a richer ordered invariant. See the potential report.

Recommendation

Keep the machine open and retain the checked local modules. A further whole-machine proof attempt needs an ordered invariant for the exact normal form, ideally the 81-bit seed above. Repeating generic simulation, expanding the same count features, or replacing the word by a bounded left window is not supported by these results.

No closed pseudo-random arithmetic recurrence has been identified, so this work does not label the machine a cryptid. No whole-machine kill checker was run. result.json and the adjacent receipts record the exact scope of every result.

AI assistance: GPT-6 Astra (OpenAI).