BB(6) hunt
Machines / 740 line 593

1RB0LD_0RC1RA_1LD1RC_1LE0RF_---1LA_1LF0LA

740 line 593In progressBouncer + Chaotic Edgebbchallenge ↗Explorer

Where it stands

In progress: Rocq proof

Completed bounded follow-up: exact finite-reserve normal form and formal local components; the infinite reserve bound for the blank orbit remains unproved.

Observe
Deepen
Informal proof
Rocq
space-time diagram, first 10,000 steps from blank
The first 10,000 steps from a blank tape. Time runs down; white is 1.
About this picture

The standard picture (bbchallenge.org's Default view): each row is the whole tape at one step, time runs downward, and the head's path draws the pattern.

bbchallenge-defaultStart blankRows steps 0 → 10,000, top to bottomWindow cells −200..199, left to rightColors 1 0 or unvisited

Overview

In one sentence

Exact reserve model and local proofs completed; the infinite bound for the 81-bit seed remains open.

Status
In progressinvariant study complete · updated 2026-10-14T15:20:20.197471-07:00Not blocking · Stage: invariant study complete.
idle since Oct 14 15:20 (46 h ago) · status.json 2026-10-14T15:20:20.197471-07:00
Informal proof
proof.mdconditional; see Proof for what is still open
Class
Bouncer + Chaotic Edgeours: sheet Bouncer + Chaotic Edge ≠ ours Bouncer with period-51 bulk and unresolved irregular boundary · low confidence
On the list
line 532 of BB6_holdouts_663.txt · historical 740 line 593
eqv ×2sim 1e15UBRRBA
Your calls on file 3
next
Retain checked local components. Further mathematical progress needs an ordered invariant for the record-32 seed; repeated generic simulation or bounded-prefix rules do not close the gap.
2026-10-14 · study
Fund a 60-minute study of line 593’s left-word invariant and prefix-consumption bound, or defer? (Okay do the follow-up I guess.)
2026-10-14 · study
Fund a 30-minute edge-return study using the period-51 bulk of line 593? (Follow your recommendations for the 5)

Mechanism

How it works: 3 notes
  • The uniform 51-cell bulk roundtrip is formally proved for every n>=0, with arbitrary exterior tapes. A separate counted composition gives exactly 906n+2881 transitions.
  • The exact normal form N(k,w)=A>0(011)^k w accounts for every terminating virtual-core case, including zero-reserve halts and safe F escapes. It reproduces all 792 saved primitive records.
  • At step 5104 the observed orbit reaches reserve 1 and an explicit 81-bit residual word. Its next 380 observed pairs all satisfy the common-domain reserve bound; no infinite bound has been proved. Uniform constructed families with arbitrarily long common prefixes have opposite halting outcomes. Fixed-prefix tests and the specified small additive potentials cannot establish the needed global safety invariant.

Figures

Fig 1 · Early bounces, first 200,000 steps

Follow the moving head and compare the two outer edges.

Early bounces, first 200,000 steps
bbchallenge-defaultStart blankRows every 100 stepsWindow cells -128..372, 1 px = 1 cellsColors 1 0 or unvisited head after a right move head after a left move
Rows: 0..200,000, 2001 rows; time runs downward · Window: sampled columns when scale exceeds 1
Fig 2 · Growth through 10 million steps

Compare regular bands with the irregular boundary region; rows and columns are sampled.

Growth through 10 million steps
bbchallenge-defaultStart blankRows every 10,000 stepsWindow cells -324..2868, 1 px = 2 cellsColors 1 0 or unvisited head after a right move head after a left move
Rows: 0..10,000,000, 1001 rows; time runs downward · Window: sampled columns when scale exceeds 1
More figures (1)Fig 3: First 10,000 steps, site view
Fig 3 · First 10,000 steps, site view

Compare the initial widening trace before the much larger sampled views.

First 10,000 steps, site view
bbchallenge-defaultStart blankRows steps 0..9999 squeezed to 500 display rowsWindow cells -200..199, 1 px = 1 cellColors 1 0 or unvisited head after a right/left move
Rows: each row blends source rows 20y+9 and 20y+10 · Colors: pale colors are blended
Rules (2/2 validated)exact tape rewrites the proof will formalize, each re-checked by simulation
rulefrom ⟶ tocasesstepschecked
Uniform bulk roundtrip
G W C> P^n T 08
⟶ <A P^(n+2) T
n>=0; fixed words defined in study.md; arbitrary untouched left context906n+2881✓112/112
Left 00 repair
A> 0 (011)k 00 v
⟶ A> 0 (011)k+1 1 v
k>=0; final head two cells left; arbitrary untouched v; blank cells on left10k+12✓560/560
Compressed historythe tape as Observed span and snapshot compression; no invariant skeleton established at 3 moments: where the rules are read off
Observed span and snapshot compression; no invariant skeleton established
steplohiK64_tokens
1,000,000-21287634
10,000,000-3242,86824
100,000,000-7929,15633
lolast -792
-212-7921e61e8step 1000000: lo = 212step 10000000: lo = 324step 100000000: lo = 792
hilast 9,156
9,1568761e61e8step 1000000: hi = 876step 10000000: hi = 2868step 100000000: hi = 9156
K64_tokenslast 33
34241e61e8step 1000000: K64_tokens = 34step 10000000: K64_tokens = 24step 100000000: K64_tokens = 33
Template comparisontemplate: unknown · the nearest solved proof, what carries over, and the transitions that differ
01
A1RB0LD
B0RC1RA
C1LD1RC
D1LE0RF
E---1LA
F1LF0LA
file
—
module
—
machine
—
diff
—
note
Preflight found no existing machine-table conjugacy or current open-PR overlap. No proof template selected.
Proof strategy & riskshow the formal proof will go · 3 risks to watch

Retain checked local components. Further mathematical progress needs an ordered invariant for the record-32 seed; repeated generic simulation or bounded-prefix rules do not close the gap.

  • ▲No global invariant excludes the zero-reserve A-return halt on the actual blank orbit.
  • ▲The executable normal form has extensive exact finite checks but its full general correctness is not yet formalized.
  • ▲The local Rocq theorems and finite entrance do not imply blank-start nonhalting; no whole-machine kill gate has run.
Stats & provenance1.8·109 steps simulated · 42,193 cells · the status in full · files
simulated
1.8·109 steps
tape
42,193 cells · 31,455 nonzeros
growth
Expanding span in the measured prefix; no asymptotic law established.
status now
Completed bounded follow-up: exact finite-reserve normal form and formal local components; the infinite reserve bound for the blank orbit remains unproved. (status.json, 2026-10-14T15:20:20.197471-07:00)
files
observe.json · notes.md · proof.md · status.json · LocalBulk.v · LocalEntrance.v · LocalObstruction.v · LocalRules.v · LocalSafety.v · LocalSweep.v

Proof & checks

Files

machines/<tm>/: 40 entries · raw notes, status, scripts, images

namesizechanged
notes.md ↓6.0 KB2026-10-14 13:41
proof.md ↓7.1 KB2026-10-14 13:58
status.json ↓2.9 KB2026-10-14 15:20
observe.json ↓7.1 KB2026-10-14 13:48
LocalBulk.v ↓1.3 KB2026-10-14 13:12
LocalEntrance.v ↓2.6 KB2026-10-14 13:52
LocalObstruction.v ↓4.9 KB2026-10-14 13:39
LocalRules.v ↓4.3 KB2026-10-14 13:07
LocalSafety.v ↓5.5 KB2026-10-14 13:22
LocalSweep.v ↓2.3 KB2026-10-14 13:20
decisions/2 items2026-10-14 13:48
img/3 items2026-10-13 18:25
invariant-study-20261014/22 items2026-10-14 13:46
observation/26 items2026-10-13 18:26
study/23 items2026-10-14 10:31
LocalBulk.glob ↓11 KB2026-10-14 13:18
LocalBulk.vo ↓20 KB2026-10-14 13:18
LocalBulk.vok ↓0 B2026-10-14 13:18
LocalBulk.vos ↓0 B2026-10-14 13:18
LocalEntrance.glob ↓15 KB2026-10-14 13:52
LocalEntrance.vo ↓14 KB2026-10-14 13:52
LocalEntrance.vok ↓0 B2026-10-14 13:52
LocalEntrance.vos ↓0 B2026-10-14 13:52
LocalObstruction.glob ↓80 KB2026-10-14 13:39
LocalObstruction.vo ↓24 KB2026-10-14 13:39
LocalObstruction.vok ↓0 B2026-10-14 13:39
LocalObstruction.vos ↓0 B2026-10-14 13:39
LocalRules.glob ↓70 KB2026-10-14 13:17
LocalRules.vo ↓606 KB2026-10-14 13:17
LocalRules.vok ↓0 B2026-10-14 13:17
LocalRules.vos ↓0 B2026-10-14 13:17
LocalSafety.glob ↓26 KB2026-10-14 13:22
LocalSafety.vo ↓22 KB2026-10-14 13:22
LocalSafety.vok ↓0 B2026-10-14 13:22
LocalSafety.vos ↓0 B2026-10-14 13:22
LocalSweep.glob ↓30 KB2026-10-14 13:20
LocalSweep.vo ↓16 KB2026-10-14 13:20
LocalSweep.vok ↓0 B2026-10-14 13:20
LocalSweep.vos ↓0 B2026-10-14 13:20
study.md ↓11 KB2026-10-14 10:31
status.json in full
{
 "tm": "1RB0LD_0RC1RA_1LD1RC_1LE0RF_---1LA_1LF0LA",
 "status": "OPEN",
 "stage": "invariant_study_complete",
 "updated": "2026-10-14T15:20:20.197471-07:00",
 "updated_utc": "2026-10-14T22:20:20.197471+00:00",
 "owner": "astra",
 "holdout_line": 593,
 "reason": "Completed bounded follow-up: exact finite-reserve normal form and formal local components; the infinite reserve bound for the blank orbit remains unproved.",
 "confidence": "low",
 "observation_complete": true,
 "proof_started": false,
 "formal_checker_run": false,
 "recommendation": "Retain checked local components. Further mathematical progress needs an ordered invariant for the record-32 seed; repeated generic simulation or bounded-prefix rules do not close the gap.",
 "next_action": "Completed 593 stage and verification; retain the specific seed/reserve bound as the future mathematical target.",
 "observation_completed": "2026-10-13",
 "next": "Retain checked local components. Further mathematical progress needs an ordered invariant for the record-32 seed; repeated generic simulation or bounded-prefix rules do not close the gap.",
 "study_started": "2026-10-14T12:59:26.349236-07:00",
 "study_deadline": "2026-10-14T13:59:26.349236-07:00",
 "study_budget_minutes": 60,
 "study_result": "invariant-study-20261014/result.json",
 "local_formal_components": {
  "status": "compiled_and_kernel_checked",
  "modules": [
   "LocalRules",
   "LocalBulk",
   "LocalSweep",
   "LocalSafety",
   "LocalObstruction",
   "LocalEntrance"
  ],
  "receipt": "../../astra/autonomous-20261014/local-rules/verified-components-final.json",
  "scope": "Six local modules: conditional rules and nonhalting cases plus exact finite blank-start entrance. No whole-machine halting/nonhalting theorem and no kill gate.",
  "additional_receipts": [
   "../../astra/autonomous-20261014/normal-form-review/kernel-check-result.json",
   "../../astra/autonomous-20261014/window-checker/20261014-133711-coqchk.json"
  ]
 },
 "study_completed": "2026-10-14T13:41:41.066482-07:00",
 "proof_scope": "Local conditional components only; no whole-machine nonhalting theorem.",
 "whole_machine_proof_started": false,
 "remaining_obligation": "From the exact 81-bit residual seed at primitive step 5104 and reserve 1, prove an infinite upper bound of 1 on cumulative debit plus the word-dependent safe-domain threshold, or otherwise establish the exact normal-form safety conditions.",
 "finite_entrance": {
  "steps": 5104,
  "head": -32,
  "reserve": 1,
  "residual_word_bits": 81,
  "theorem": "LocalEntrance.blank_entrance_5104",
  "kernel_checked": true
 },
 "last_session_review": {
  "completed": "2026-10-14T15:20:20.197471-07:00",
  "report": "../../coord/audits/astra-autonomous-20261014.md",
  "result": "Local checked components retained; global reserve obligation unchanged; no new kill."
 }
}
observe.json contract (tools/README-card.md):
1 contract warning
  • rank: missing