Initial observation: holdout line 593
Machine: 1RB0LD_0RC1RA_1LD1RC_1LE0RF_---1LA_1LF0LA. Owner: Astra. Halting status: open.
A 51-cell periodic bulk dominates the observed tape; the smaller irregular left edge is still unexplained.
Recommendation and stopping point
Rank first of these two for a future bounded edge-return study, but stop proof work now: the irregular edge update has no established model.
Confidence is high in the finite measurements, medium in the visible bouncer/periodic-bulk description, and low in a complete mechanism. No arithmetic return recurrence has been established, so no claim of pseudo-random arithmetic is made. Stop before constructing an unsupported invariant. This is an observation result, not a kill claim.
Measurements
| primitive step | visited left | visited right | compressed tokens, max period 64 |
|---|---|---|---|
| 1,000,000 | -212 | 876 | 34 |
| 10,000,000 | -324 | 2,868 | 24 |
| 100,000,000 | -792 | 9,156 | 33 |
The longest primitive-period run in the 100m snapshot has period 51, with 170 full copies and 8,670 cells. observation/periodic-runs.json records its exact word and offset from the visited left edge. Rotations of the word can arise from the chosen starting cell. The period search and byte equality certify the sampled substring only.
The qsim endpoint is 1,846,460,530 steps after 100,000 macro loops, with 2103 rules and 0 Collatz rules. Reported rule statistics: {"count": 2103, "types": {"Diff_Rule": 2103}, "uses": {"1": 2103}}. These are external simulator facts, not Rocq certificates. The default block finder chose block size 1 and gave no rules for either candidate.
A separate direct C run to 1,846,460,530 agrees with the block-51 qsim on state, direction, step number, and all nonblank cells relative to the head. This comparison does not independently compare qsim's absolute head position, which its exported snapshot does not provide. The farthest direct run reaches 1,846,460,530 steps without a halt, visits [-2,676, 39,516], and has 31,455 ones.
Mechanism boundary
E is entered only by D0=1LE. Thus D reading 0 with a 0 immediately to its left reaches E0, the undefined transition. Excluding this state-sensitive pattern globally remains unproved.
No finite macro rule was promoted into an invariant, and no Coq work was attempted. The diagrams of periodic regions and the compression sizes do not show that those regions will retain their structure forever.
Artifacts and reproducibility
index.html: labeled observation card, rendered fromobserve.json.img/first-200k.png: rows every 100 transitions through 200,000; full cell resolution.img/first-10m.png: rows every 10,000 transitions through 10,000,000; column scale is stated on the card. These are sampled rows, not a continuous trace.img/default-10k.png: the standard site view of the first 10,000 steps.observation/direct-100m.jsonl: direct snapshots every million transitions plus the final configuration.observation/qsim-block51.jsonl: accelerated probe with exact counts; default probe isqsim-30s.jsonl.observation/direct-qsim-crosscheck.jsonlandqsim-direct-agreement.json: independent direct endpoint and comparison.observation/compressed-k64.json,compressed-samples.json,periodic-runs.json: lossless compressed samples and exact periodic-substring measurements.- Every simulator/diagram invocation has a neighboring
.meta.jsonrecording its command, elapsed time, memory preflight, load, and 6,000,000-kB virtual-memory limit.
The initial runner is astra/observe_bouncers_593_715.py; the analysis/card-data builder is astra/summarize_bouncers_593_715.py. Commands for additional bounded probes are preserved in the per-command metadata. Runs used one worker, nice level 10, MemAvailable above 10 GB, and one-minute load below 28. No existing proof, vendor, shared tools, mailbox or git-state edits were needed. The card linter's sole remaining warning is the intentionally unset historical pool rank; the exact current holdout line is stored separately.
AI assistance: GPT-6 Astra (OpenAI).
Priority decision — 2026-10-14
The user said: “Follow your recommendations for the 5.” Recorded study for this family; a mechanism study is funded for at most 30 minutes.
Funded mechanism study — 2026-10-14
Derived the exact uniform bulk/right-edge roundtrip G W C> P^n T 0^8 -> <A P^(n+2) T in 906n+2881 steps. Confined component traces and independent finite checks support the composition; no Rocq proof was attempted. All 792 left-record configurations of the 100-million-step prefix match an exact bulk-shortcut interpreter. The remaining obligation is a safe closed language for the irregular left word: arbitrary words and simple leading 011-prefix families have explicit halting counterexamples. See study.md and study/result.json.
Funded stage closed — 2026-10-14
The approved mechanism study is complete. Its answered decision is archived in decisions/2026-10-14-study.json. No research job remains running. The new priority card concerns a separate stage and is unanswered. Full comparison: coord/audits/bouncer-studies-20261014.md.
Funded invariant study — 2026-10-14
Proved internal safety for an unlimited 011 prefix, formalized in LocalSafety.v; this premise excludes blank tape. Derived an exact word/counter normal form including k=0 and every one-return boundary, reproducing all 792 saved primitive records from blank start. The sole halting branch is an A return with reserve exhausted; requesting another block at zero reserve instead gives a safe F escape. LocalObstruction.v proves that arbitrarily long shared prefixes can have opposite constructed halt/nonhalt outcomes. The remaining target is an ordered reserve-debt invariant, with an 81-bit seed at record 32 / step 5104. See the invariant study, normal-form derivation, and machine-readable result.json in that directory. No whole-machine theorem or kill claim.