/machines/1RB0RA_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---/notes.md · raw

1RB0RA_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---

Status: STUCK (2026-10-10, pass 3 after skeptic review; fatal gap: no inductive invariant closes the domain predicate G, proof.md §3.3.5. All 5 minor review gaps fixed) Class guess (agent / Dennis): Bell eats counter, the "twin #2" of pilot #2: the parent's mechanism without the extra pass at L's, plus a stray token / – Spreadsheet notes / Discord thread: Results row 1048, class "Bell eats counter" (also on Classifications, row 6). Status, Notes, Sources and Done By are blank; no links or strikethrough. Not in data/discord/. Unclaimed. Viewer: https://bbchallenge.org/1RB0RA_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---

Observation

Candidate rules

The parent's transducer carries over except at the L digit. Full table and checks: proof.md §2 and check_proof.py. - L entered (by the eater or by a drain pass): out [h, h'] instead of the parent's [h, h', h]. So there is still a +1 to the rest, but no new pass. - Why: A1 = 0RA then A0 = 1RB writes a 1 where the parent's F0 wrote 0. - Coming back, C1 = 0LD restarts the eater one cell to the left, behind 0 111. - When the eater returns, 011 closes directly to 110, with no extra bounce. - Machine level: eater 1 D> 110 <X> -(6j+9)-> 0 111 D> <X+1>; drain B> 1 110 <X> -(6j+8)-> 0 111 D> <X+1>. - Since the eater no longer gains passes at L's, it often reaches the first 1 with k = 0, or a drain runs out in the middle of the word. - The drain then stops and leaves its stray 1 in front of an untouched rest: clause Z R(h1,0,r,S::r), for every r. The parent's Z0/Z1 are the end-of-word instances. - The next sweep's n L's send n +1 passes to the tail. One that reaches a stray resumes that drain with one pass: IS Inc(S::r,r') <- R(h1,1,r,r'). - Through C1, such a +1 can start a whole nested eat-and-drain. Example: S(L^5 SL1) -> S(L^9 S001), worked in proof.md §2. - Tests: the model reproduces 277/277 consecutive boundaries from blank to 1e9. The parent's rules reproduce 1/277. Every clause passes on the real machine (2,829 derivations), and BigStep passes on 1,243 random words. The abstract orbit runs 3,000 sweeps without leaving the domain, with at most 1 stray. - Not a cryptid: +1, halving and bijective binary, as in the parent.

Checkpoint A (Dennis)

None yet (non-blocking). Twin task brief from the orchestrator: determine whether the parent's rules carry over.

Informal proof

proof.md is now a full document, not a delta. It is complete except for one lemma. - Carries over and compiles in Rocq (scripts/TwinSpec.v, 4/4 closed in pass 2; 5/5 with RIncs_eq and Example sweep_LS01 in pass 3): - §3.1 RIncs_spec, with the new token DS, mutual Inc/RIncs, the changed X1/C1 and the general Z; - §3.2 BigStep; - §4 init. - New in pass 2 (informal; checks 8a–8f in check_proof.py): - Lemma A. One more pass is +1 on the result. It is the parent's RIncs_Inc, plus the case Z -> IS. - Lemma B. On S-free words every clause chain exists and leaves at most one stray. The eater fails only on words in 0*. Proof by induction on (length, #L). - Lemma C. If G(w), where w = L^n t and Inc^n(t) is S-free, then the sweep is defined. - Lemma D. G(sweep w) holds iff θ(x) <= n', where θ is the monotone threshold of the eater count that leaves no stray. - So the domain is a single inequality per sweep, for the system (N, x) -> (N + a(x'), x'). - Open: an invariant J(N, x) that implies θ(x) <= N and is preserved by the sweep. - G alone fails: 1001 -> LS001. - J0 (θ <= N) fails: (00010001, 5). - J2 (2θ <= N and x ends with 1) fails: (L1111, 60). - J3 (J2 plus V + lead L <= 5N/4) fails at small N: (L11, 4). J3 with any lower bound N >= N0 also fails: (2^(m+1)-4, 00001) -> 1 0^m 1 with 2θ' = N'+1, for m = 4..20 (pass 3, check 9c; found by the reviewer). - The margin N - θ can halve in one step: (L11111L, 26). - Pass 3 (after the skeptic review): a weighted value V (an L after p digits counts 2^p). - Inc is +1 on V (V1). The sweep is affine: V*(x') = N + c(x) (V2). Both are proved. - Lemma T is a conjecture, exhaustive to 11 tokens: 2θ(x) <= V*(x) - 1 for x ending with 1. Under T, J4 := ends with 1 /\ V* <= 2N+1 gives θ <= N. - J4 is not inductive: (257, 10000000L1) -> V(x') = 642 > 519. That is an L just below the top bit, reached by the drain with 1 pass. - But in 400 random J4 starts x 25 sweeps the domain never failed, and V/N falls below about 1.45 after two sweeps. - Open, precisely: a shape condition K on the L's with c(x) <= N + 3 and K preserved (proof.md §3.3.5). - Pass 3 also fixes the review's minor gaps: - RIncs_eq re-parse constructor, placed inside Lemma C after the eater's L-run. Without it, 75 of 15,593 G words have no derivation, for example LS01. With it, all of them do. - Lemma D's "1 or L" argument. - Canonical and #S <= 1 are now inside G and P. - Lemma U (uniqueness up to tape) replaces the appeal to determinism. - The orbit claims now say "first 3,000 sweeps", and the 1.25 bound is attained exactly at sweep 2. - Orbit (3,000 sweeps; 278 boundaries from blank to 1e9): - G always holds; - x_s always ends with 1; - 2θ <= 0.962 N (worst at sweep 27); - V(x) + lead L <= 1.25 N, so the tail is a counter tracking the L-run. - A working J must bound the tail's shape (its zeros against log2 N), not just counts. The parent's count-only key cannot transfer, because the second sweep's count does not grow at L's (proof.md §3.3.5).

Formalization log

Outcome

STUCK (pass 3, 2026-10-10, about 2 h; pass 2 was also about 2 h). Skeptic review: 1 fatal gap and 5 minor ones. - The 5 minor gaps are fixed in proof.md, check_proof.py and TwinSpec.v. - The fatal gap remains: no inductive J. Pass 3 narrows it to two pieces of new mathematics: 1. Prove Lemma T (2θ <= V* - 1). 2. Find a shape condition K on the L's that bounds c(x) and is preserved. - Not a cryptid. The rules are exact and checked, and V2 makes the counts exactly affine. - Validations: check_proof.py default and --full both ALL PASS (proof.md §7), including Rocq 5/5 closed. - A decision.json asks Dennis whether to fund one more stage on T and K or to park the machine. - The pass-3 Rocq tactics are logged in atlas/rocq-notes.md. STATUS.md was not edited: the orchestrator owns it.

Decision (2026-10-10, auto-applied)

Question: Fund one more stage (at most 2 h) to prove Lemma T and find the shape condition K that closes twin #2's domain, or park it as STUCK? Answer: park (Park as STUCK). auto-applied: Claude's recommendation, under Dennis's standing instruction 'do your recommendations and continuously orchestrate' (2026-10-10, while he was at lunch). Override any time. Parked 2026-10-10 (auto-applied recommendation): Lemma T and shape condition K are new math; reopen if the queue runs dry.