/machines/1RB0RF_1RC1RF_1LD1RA_---0LE_1LA0LE_0RA0LC/notes.md · raw

1RB0RF_1RC1RF_1LD1RA_---0LE_1LA0LE_0RA0LC

Status: CRYPTID_CANDIDATE (2026-10-10; the funded lemma_x stage reached its agreed exit) Class guess (agent / Dennis): Bell eats counter, partial eat with residue digits / – Spreadsheet notes / Discord thread: Results row 1047, class "Bell eats counter", status/notes/sources blank; no link, no strikethrough, no xlsx comment. Not on dyuan01's 24 or mxdys's UBRRBA 86. Twin 1RB0RE_1RC1RE_1LD1RA_1LA0LD_0RA0LF_1LD--- (row 1032) is also blank. Viewer: https://bbchallenge.org/1RB0RF_1RC1RF_1LD1RA_---0LE_1LA0LE_0RA0LC

Observation

Candidate rules

enc(v) = v0 010 (00 v1)…(00 vk) (LSB first) · enc3(m) = (00 m0)(00 m1)… · F(v) = 1 0 v0 (00 v1)…, F(0) = 1

rule from → to cases validated
R1c K(a, b+1, enc(a)) → K(a+1, b, enc(a+1)) in 8b+8 (+6t+8 if t>0, t = trailing 1s of a) steps a≥1, b≥1, incl. overflow 127/127 (a ≤ 1e6, b ≤ 2000)
R1g K(a, b+1, X) → K(a+1, b, X⁺), X⁺ independent of a, b residue words from epochs N=37 and N=331 160/160
E0 K(1, N-1, 101) →* K(1, N, 110 enc3(N/2)) N even 60/60
E1 K(1, N-1, 101) →* K(1, N+2, F((N+1)/4)) N ≡ 3 mod 4 40/40
E2 K(1, N-1, 101) →* K(1, N+3+r, F(N >> (3+r))) N ≡ 1 mod 4, r = run of 1-bits from bit 2 (r = 0..7) 50/50

E0–E2 were tested up to N = 14,077. Scripts: scripts/val_r1.py scripts, scripts/val_r1g.py scripts data/khub_epoch37.txt data/khub_epoch331.txt, scripts/val_r2.py scripts.

Wrong guesses that died here: - My first enc (bit k at cell 3k+2) failed 64/142. - My first R1c step formula (8t+6) failed. - R1c with b = 0 fails: that is the eat phase, not a bounce.

Open: the epoch map with residue. Residue changes dN only in the r ≥ 1 branch (for example N=21: clean +5, with residue +10; N=309: +5 vs +8). The ≡3 mod 4 and ≡1 mod 8 cases matched clean in 15 probes.

Template check (FractalBEC.v tm10, mirror differs only in C1 = 1RB vs our 1RA), simulated on our machine: - RInc 4/4 and Ov 8/8 hold. - LInc holds 8/16: it fails for every odd counter, where C reads LSB 1 and goes 1RA. - config i → i+1 holds 1/6.

Verdict: partly. The bounce shape carries over; the counter digits and the doubling epoch map do not.

Not a cryptid by ground rule 6: branching is on the low bits of N, N grows linearly, and nothing is exponential or ×3/2.

Checkpoint A (Dennis)

Questions in observe.json → checkpoint_questions.

Informal proof

Not started (waiting on Checkpoint A).

Formalization log

–

Outcome

CRYPTID_CANDIDATE (2026-10-10). Not a kill. See "Funded stage (2026-10-10, lemma_x)".

Card data pass (2026-10-10)

Deepen pass (overnight 2026-10-10)

Result: every regime from the blank tape is covered by exact rules. The abstract epoch map reproduces all 1,142 TM epochs up to 1e11 steps (n = 2 → 8,416). Non-halting comes down to one size invariant. It holds along the trajectory (checked for 200,000 abstract epochs, n up to 2.28M), but I have not yet found a version that is proven to be inductive. Confidence: med. Not a cryptid: the condition is a size inequality whose slack does not shrink, not a parity or Collatz-style coincidence.

Notation

Micro-automaton (how all the rules were derived)

Rules (all exact, validated by deepen_val.py: 3 seeds × 1,000 random instances per rule, 9,000/9,000)

rule from → to cases
R restart L(n,Q) → K(1,n,1Q) in exactly 3n+5 steps n ≥ 1, Q ∈ {100,010,000}*
B bounce K(a,b+1,X) → K(a+1,b,inc X) b ≥ 1, X ∈ L_X; inc keeps L_X; a and b are inert
inc x0=0: set x0=1. x0=1: x0:=0, carry in state A at g1: 010 pass · 001→000 pass · 000→001 stop · end: append 001 · 100→010 and toggle the groups after it up to and including the next 000 (010↔000, 100 untouched, past the end the 000 becomes 010), then go on to the next group the toggle is a binary +1 on the i/0 string (i=1), skipping S
E eat K(n,1,X) → L(n',Q'), X normalized n odd: H = carry(g1…), n' = n+1. n even: J-walk with a = n+1 over g1…: 001 drop, a+1 · 010 drop, carry(rest), a+1 · 000 drop, stop; H = rest; n' = a+1 (a counted before this drop)
map Q' = regroup(cells(H)[1:]), i.e. per group of H: 010→100 (S), 001→010 (i), 000→000 the old inert groups become S, the old 1-digits become i

Bounce-phase facts: - X0 = 1Q has value 1. After the n-1 bounces the value is n, so K(n,1,X_end) holds the binary of n spread over the digit groups. - The S groups disappear only when a carry first reaches them, at increment 2^D - 1, where D is the normalization depth. That depth is fixed by Q alone (deepen_model.bounce_phase). - The intermediate hubs K(a+2,1,·) and K(a+3,1,·) seen during the eat are the C> moments of the J-walk. - The clean E0, E1 and E2 rules of the observe pass are special cases of R + B + E with Q = i.

Cross-checks

Non-halting argument and the remaining gap

Scripts (new; run with python3 -B from scripts/)

Next step

Informal proof stage. Find a version of I that is provably inductive, for example by adding to Z* the constraint that reachable Q are images of counters whose top run sits above every inert group, or by a weighted count. If no inductive invariant turns up within budget, re-flag the machine as a cryptid candidate with this heuristic. On a borderline tail fit (ratio about 0.4 against B growing like log n), the expected number of violations over all time is not clearly finite.

Informal proof pass (overnight 2026-10-10)

Result: I wrote proof.md. The informal proof is complete except for one arithmetic lemma, Lemma N. Status OPEN, stage informal_proof. check_proof.py passes every check (seed 2; log in scripts/check_proof_full.log; --quick gives a fast pass).

New: the epoch map in closed form

The state at an eat is (n, c): - the layout is λ = i^c0 d i^c1 d …, and its d-slots hold bits 1, 2, … of n; - C = Σ c_j 2^j, and J is the index of the top inert slot.

The map: - n odd: M = (n+1)/2 + C, H = c, n' = n+1. - n even: V = n/2 + C, t = number of trailing 1-bits of V, M = V >> (t+1), H = c[t+1:], n' = n + 2 + t + Σ_{r≤t} c_r. - Next layout: merge(H, M). That is H's inert groups, plus one i for each 1-bit of M, with a d at each 0-bit of M. - Normalization depth: D = 1 + #{0-bits of M below J(H)}. The next eat is normalized iff D ≤ B(n') - 1.

Agreement: - with the deepen map: 20,000/20,000 epochs along the orbit, 17,169/17,169 random states; - with the TM: 276/276 records to 1e9 steps.

This replaces Z and D from the deepen pass. Z = J(c) = #zeros(M_prev).

Proven sufficient conditions

Both hold at every eat for 20 ≤ t < 200,000. The orbit's margins are max C/2^(B-1) = 0.688 (t = 62,386) and J ≤ B-2 at every even n.

Open: Lemma N

This looks like a hard barrier on the image of the map, not a rare-event tail. - Next step: describe the image Φ^k for small k, i.e. c = merge(H_prev, M_prev) with M_prev ≈ (n/2 + C_prev) >> s. Then prove slack ≥ 0 on that image. Candidate potential: V = ⌈n/2⌉ + C against 2^B(n), together with J ≤ B(n)-1. - Fallback: ground rule 6, i.e. flag as a cryptid candidate. The condition depends on the bit patterns of ⌈n/2⌉ + C.

Cell level

Formalization plan

Templates are BECv7.v (Inductive digit words, bin_inc, progress_nonhalt_cond with P := canonical), FractalBEC.v (bounce shape) and BinaryCounterFull.v (N-valued counters). The rule layer can be formalized now. Only the final progress_nonhalt_cond is blocked, on Lemma N.

Skeptic revision pass (overnight 2026-10-10, proof.md revision 2)

Result: STUCK at informal_proof. The skeptic's fatal gap stands. Revision 1's Lemma N in the Inv_S form is false on the orbit. A cascade starts at t = 350,272 (M = 2^21 at odd n). The slack is exactly 0 at t = 350,273, and Inv_S fails at t = 350,274 (C = 1.5001·2^{B-1}). The slack itself never goes below 0. Lemma N now keeps only the slack form, and P := Inv_S is gone from the busycoq plan. Not a kill.

New and proved (proof.md §5.4–5.5)

Evidence (check_proof.py revision 2, seed 2, all PASS, 69 s)

Rule layer (proof.md §2.5)

Cryptid assessment

Not flagged. Excursions start with a coincidence, ⌈n/2⌉+C (nearly) a power of two, but every follow-up examined is kept safe by exact arithmetic. This is a priority call for Dennis: spend another stage on Lemma X (a finite case analysis over excursion entry types), or flag CRYPTID_CANDIDATE and formalize only the rule layer, AntiHydra-style.

Decision (2026-10-10)

Question: Fund one more stage on Lemma X (classify the excursion entries exactly), on the condition that if the entry types do not close into a finite list within the stage, #10 gets flagged CRYPTID_CANDIDATE? Answer: lemma_x (One more stage on Lemma X, with the cryptid flag as the exit). Dennis: go with all recommendations (2026-10-10).

Funded stage (2026-10-10, lemma_x)

Result: the stop rule fires. CRYPTID_CANDIDATE. The excursion entries do not close into a finite list of safe types. Every entry comes from an odd eat (proved), but the entry shapes form an infinite family. More decisively, whether an entry is safe depends on the exact residue counts, not on its shape. For one shape there is an explicit family of states, one for every B ≥ 8, that satisfy everything Lemma X may assume (slack ≥ 0, no excursion) and still reach a non-normalized eat 4 epochs later. So Lemma X cannot be proved by a case analysis over entry types. A proof would have to show that this one orbit's residues never solve an exact equation of the form P = 2^B. That is ground rule 6.

Notation (as proof.md §3)

New lemmas (proved; checked by scripts/fs_lemmax.py, seeds 1 and 2, N = 20,000 each, all PASS, logs scripts/fs_lemmax_seed{1,2}.log)

id statement proof idea check (both seeds)
F4 odd n: P' = P + m(P) - L(c,P) ⌈n'/2⌉ = (n+1)/2 = P - C, then the merge 19,952/19,952
F5 even n: P' = V + 1 + ⌈(s+σ_s)/2⌉ - C_lo - (2^{s+1}-1)·C(H) + m(M) - L(H,M) the same, with n/2 = V - C and C = C_lo + 2^{s+1} C(H) 20,048/20,048
A no excursion starts at an even eat: even n and P < 2^{B1} imply P' < 2^{B1} P' ≥ 2^{B1} would need C' ≥ 2^{B1-1}, and m(M) ≤ 2^{B(M)-1} ≤ 2^{B1-s-2}. For s ≥ 1 that forces C ≥ 3·2^{B1-1} > V. For s = 0, F5 gives P' ≤ 2M + 2m(M) + 1 - 2^{B1-1} ≤ 2^{B1} - 1 32,448 even non-excursion states, 0 entries
B P + m(P) ≤ 2^b + 2^{b-2} for 1 ≤ P < 2^b, so an odd entry has P' ≤ 1.25·2^{B1} split P into its top run of ones and the rest, then induct on b exhaustive for b = 2..18 (the maximum is exactly 2^{b-2}); 32,110 odd states
R2 if slack(σ) ≥ 0 and slack(σ') < 0, then σ is (odd with P = 2^{B1}, the super-cascade), or P ≥ 2^{B1+1}, or (even with V = 2^{B1} and B(n) < B1) Lemma Z gives J(c') ≤ max(B1-2, Z(M)). At odd σ, n' is even, so D' ≤ max(B1-2, Z(P)), and Z(P) ≥ B1 needs P = 2^{B1}. At even σ, M < 2^{B1}, so only M = 2^{B1-1} (V = 2^{B1}) at odd n' is dangerous; EC covers B(n) = B1 238,873 slack ≥ 0 pairs: 36 failures (15 super-cascade, 21 P ≥ 2^{B1+1}), 0 unclassified
EC even cascade: even n, V = 2^{B1}, B(n) = B1 and slack ≥ 0 give slack' ≥ 0 and 1.125·2^{B1} < P' ≤ 1.25·2^{B1} + 1 slack ≥ 0 forces J(H) ≤ B1-2, so L = 0. For odd n', P' = 3·2^{B1-1} + (3-C)/2 with 2^{B1-1} < C ≤ 3·2^{B1-2}, so P' has a 1-bit below B1-1 39,535 states; P'/2^{B1} ∈ [1.125, 1.25]

EC extends cascade lemma (iii) to any residue. Together with A, B and R2 it shows that every slack failure passes through a super-cascade or through a potential ≥ 2^{B1+1}. Both of these can only be reached from inside an excursion.

The counter-family (proved for every B ≥ 8, by exact symbolic computation)

σ0(B) = (3·2^{B-2} - 7, c = [3, 0^{B-6}, 10, 0, 2]), i.e. c_0 = 3, c_{B-5} = 10, c_{B-3} = 2.

epoch parity P slack
0 odd 15·2^{B-4} (not an excursion; entry shape: top run w = 4) 2
1 even V = 17·2^{B-4}, s = 0, M = 2^{B-1} + 2^{B-5} 3
2 odd, n = 3·2^{B-2} - 1 2^B (super-cascade), c = [.., 10 at B-6, 7 at B-5, 1 at B-2] 0
3 even, n = 3·2^{B-2} V = 2^{B+1}, M = 2^B, J(H) = B-1, D = B -1
4 even, n = 3·2^{B-2} + 2 the eat is non-normalized

Search data (scratch runs, then saved as scripts)

Why this is the cryptid exit

Still open