W4-7 · 1RB0RA_1RC0RD_1RD0LC_1LE1RA_---1LF_1RB0LC (740 line 317), observe notes

Date: 2026-10-11. Stage: PLAN §6 step 1 (Observe). Sheet class: Bell eats counter. Confidence: med.

Checks before starting

• Byte-exact on data/holdouts/BB6_holdouts_740.txt line 317 (also on every older list back to 2024-07-12_7296).
• No claim: data/discord/*.txt has nothing; data/sheet/2026-10-09_results.csv row 1035 has Status/Notes/Done By empty, class "Bell eats counter".
• data/solved_index.tsv lists it only as tm' of Eqv_v2.v Module TM1815 (halts tm c0 <-> halts tm' c0, tm = 1RB0LC_1RC0RD_1RD0LC_1LE1RF_---1LA_1RB0RF, mapping FBCDEA, 1 step each). That is an equivalence between two holdouts, not a decision.

Table, starts and siblings (canon up to renaming + mirror)

88 (1RB0LC_1LC0RE_1LA1LD_1LA1LB_0RF1RA_---0RE) and 280 (1RB0LC_1LC0RE_1LA1LD_1LA1LF_0RB1RA_1LC---) do not share this table (canon checked from all 6 starts); separate family.

Start A's trajectory never meets start B's or start C's within 20,000 steps (translation-invariant config compare; B vs C not checked), so "trajectory twins" holds only at the level of mechanism, not as identical runs.

Simulation

• 1e10 steps, no halt; span -2866..5597 (8,464 cells), 5,627 nonzeros, head in D at cell 600. Span ~ t^0.33.
• Halting analysis: the only undefined cell is E0. E is entered only by D0 = 1LE; after C0 = 1RD the cell to its left is 1, so only B1 = 0RD can lead to E reading 0, i.e. B> 1 0, which needs A> 0 1 0 (F0 = 1RB lands on a cell E just set to 1, then on a cell D just set to 1).

Mechanism (our orientation)

Tape at a pass boundary, field 2 active (step ~2.0e6): 0^inf (101)^3 00 (101)^90 | 111 (110)^k 100 (101)^(65-k) 11 C> [idle field 3: (110)^3] [counter] 0^inf and with field 1 active (step ~2.01e6): 0^inf (101)^a 00 (101)^b 11 C> [idle field 2: 00 (011)^66 | (110)^67 | 0 (101)^66 1] [idle field 3] [counter] 0^inf.

1. Bell step F (validated 200/200): (101)^a 00 (101)^(b+1) 1 <C 0 ->[8b+16] (101)^(a+1) 00 (101)^b 11 C>. Context-free on both sides (a >= 1).
2. Counter K1-K6 (validated 200/200 each): exactly the six clauses of side_3ary_Pos_inc_rule [0;0;0;0] [1;1;0;0] [0;1;0;0] [1;1] [0;1] [1;1;1;1] [1] [0] B B of the cert, mirrored: digits read left to right from the head 0000 = 0, 1100 = 1, 0100 = 2, carry 1111; top digit 11 = 1, 01 = 2; qL = the second 1 of 11 C>, qR = the 0 left behind.
3. Wide digits (the "idle fields"). The counter digit format generalises to d (110)^n 0 with d = 000 / 110 / 010 for 0 / 1 / 2; n = 0 gives the 4-cell digits 0000 / 1100 / 0100. Rules (all validated 200/200, context-free in l and r): - I2 1 C> 000 (110)^n -> <C 0 (110)^(n+1) (0 -> 1, 4 steps), I0 1 C> 110 (110)^n -> <C 0 010 (110)^n (1 -> 2, 2 steps), - I1a 1 C> 010 (110)^n 0 -> 1111 (011)^n 1 C> (2 carries: the head crosses the digit, 3n+4 steps; n = 0 is K3), - I1b 1111 (011)^n <C 0 -> <C 0 000 (110)^n 0 (carry cleared on the way back, 5n+4 steps; n = 0 is K4). So a wide digit is touched only in its first block except when it carries. The digit right after a wide 2 is read with the crossed wire on its left and uses another encoding: 0011 -> 1111 -> 0111 -> carry (J0, J1 validated; J2 leaves in state A, next encoding not pinned).
4. Two big fields take turns. When field 2's marker reaches its right end, field 2 goes idle and field 1's marker restarts moving right; when field 1's marker reaches its end, field 1 restarts at its left end and field 2 becomes active again (traces at 2,011,920 -> 2,013,101 and 2,082,683 -> 2,083,906; and again at 1e8). Fields grow: field 1 = 93 -> 318 -> 669 blocks, field 2 = 66 -> 282 -> 627 blocks at 2e6, 1e8, 0.98e9. A third, small wide digit (3-4 blocks) sits before the 4-cell digits. Hand-over E (from the traces): l 111 (110)^k 100 (101)^3 11 C> R -> l' 11 C> 000 (110)^(k+4) R': the finished bell becomes a wide digit 0 and the bell on its left takes a step. Field counts at pass boundaries: 2 big bells + 1 small wide digit at 2e6, 1e8, 1e9 (674 / 630 blocks) and 5e9 (1,144 / 1,071 blocks).
5. Certified start B (same table) has one field only: (101)^a 00 (101)^b 11 C> [counter], marker moves right one block per pass; the field grows by 2 blocks per traversal.

Right records (counter overflows: the right end is a run of 1s from carries, K3) see markers at unrelated phases, so the field data at right records look irregular; at pass boundaries they are regular.

Template check

• Nearest proved neighbour: IndBECv1.v _3ary nonhalt3 (same table, start B). Its rule set is the 3-ary counter (K1-K6) plus whatever the hlin decider finds with block size 3 after 745 steps; that is one bell + counter. Ours needs a second big field and idle-field phases.
• Decider grid on the flipped table 1LB0LA_1LC0LD_1LD0RC_1RE1LA_---1RF_1LB0RC with the same 3ary rule (QL = QR = C): config_T_bsz T 3, T = 746, 1000, 2000, 5000, 20000: decider returns false each time (104-129 s each). Calibration: the cert lemma itself compiles in 12 s (4.4 s Qed) with our coqc setup. Files and log: rocq/ (grid.log). Grid 2: mnc 3 and mnc 4 at T = 5000 fail (125 s each); sibling 707 (flipped 1LB0RA_1RC1LF_---1RD_1LE0RA_1LA0LB_1LE0LF, QL = QR = A) fails at T = 745 and 5000; block size 0 at T = 5000 (g2_bsz0_T5000.v) was still running when the session ended and did not finish; rerun it first in the next decider stage.
• A hand-proof template for this class exists upstream (not in vendor): BellEatsCounter_1RB0RF.v (HEAD 9cf9e88), built on SOMDCv6/Longitudinal.

Cryptid check (ground rule 6)

No pseudo-random arithmetic seen: the counter is plain base 3, the bells step by one block per pass, the field alternation is driven by marker positions. Not a cryptid candidate. Caveat: E and J2 are not formalized, and the number of fields is only observed (2 big bells + 1 small wide digit) up to 5e9.

Open

• Pin E (bell hand-over, both directions: bell 2 -> bell 1 and back) and J2 (carry past the digit after a wide 2) with exact case splits; then the full right-part grammar.
• Decide whether the field count stays bounded (needed for a bounded invariant / the decider).
• Proof options: (a) more decider configs (cheap), (b) hand proof: two-bell invariant + ternary counter, rules in Rocq, then Flip.v.

Scripts and data

• scripts/validate_rules.py (13 rules, 200 random instances each, seed 3 -> data/validation.json).
• data/compress_track_1e9.json, data/history.json.
• rocq/run_grid.sh, rocq/*.v, rocq/grid.log.

Decision (2026-10-11)

Question: Spend one more short stage on decider configurations, or go straight to a hand proof (two bells + ternary counter)? Answer: decider2 (One more decider stage (about 1 h)). Dennis: go with recommendations (2026-10-11).

Funded stage (2026-10-10, decider2)

Run 2026-10-11 (Dennis: go with recommendations). Outcome: no certificate. All 384 hlin decider runs are false, and so are the 178 runs of a small CTL tail (2 of them time out). Confidence stays med on the mechanism. The cheap route is closed for the pinned framework. Scripts: scripts/hlin_extract/ (README.txt, summary.json), scripts/ctl_tail/, scripts/left_visits.py.

1. The hlin decider now runs natively. busycoq's hlin decider (Inductive BB62 . decide_hlin_nonhalt, the one behind IndBECv1.v) is extracted to OCaml (Ext.v, 6 s). The driver hlinx takes the whole Config as key=value arguments: T, block size, mnc, max_repeater_len/size, arithseq, exp loop, max_period, allowed repeaters, fuel and any ExtraRules. Calibration against Coq: - the certified start B (config_T_bsz 745 3 + the 3ary rule) is true in 0.01 s (Coq: 4.4 s; fuel 1,000 is enough); - IndBECv1 Bell nonhalt1 is true in 2.35 s; - our flipped table with the cert's config is false in 59 s at fuel 1e6, as in Coq (115 s).

A false costs 5-14 s at fuel 1e5 (50-127 s at 1e6) and about 8 MB, so the grids ran 2 at a time with no coqc. A trace driver (tracex) prints the decider's layer stack.

2. Grids. 317f = our flipped table 1LB0LA_1LC0LD_1LD0RC_1RE1LA_---1RF_1LB0RC with the cert's 3ary rule at QL = QR = C. 707f = 1LB0RA_1RC1LF_---1RD_1LE0RA_1LA0LB_1LE0LF with QL = QR = A (707 is this table started in our C). Fuel is 1e5 unless noted. 0 true and 0 errors in 384 runs (summary.json).

CTL tail (scripts/ctl_tail/, the extracted CTL62 decider from #7, both orientations of our table): 79 NG settings (len 2-20) and 10 CPS_LRU settings (size 3/6/9) per orientation, 178 runs. 176 are false, and CPS_LRU size 9 times out at 120 s in both orientations. The larger CPS_LRU lines (size 9-18) were stopped to stay in budget. No true.

3. Why it fails (trace). The decider closes only when it finds a one-parameter family c0 =lb=> config(n). For the cert this is 1 (101)^5 00 (101)^(2n+6) 0inf <A 0 TER(3n+9). On our table the traces (scripts/hlin_extract/runs/trace_*.txt) keep the wide digits as explicit segments in front of the 3ary side. For example, at T = 1e5 the left side reads 0 (110)^6 0 0 1 0 (110)^15 0 (110)^5 0 TER(6) (flipped orientation). The top layer only steps forward: l = 608 → 8,109 for a period guess of r = 8,192, and it never closes. 707f looks the same (two fields, then TER(44)). Two facts make the needed family unavailable: - The framework has no rule for wide digits. ExtraRules in the pinned Inductive.v has 7 constructors, and none is a ternary counter with digits of free width d (110)^n 0. The binary rules carry d1^^n runs, and BL ties each digit's width to the value of the digits above it. So the decision's "extra side rule for wide digits" is not a configuration. It would need a new constructor with its own soundness proof inside the decider, i.e. a change to vendor code; not done. - The left-end visits are not a one-parameter family. These are the state-F left records (scripts/left_visits.py, data/left_visits_3e7.json, 200 visits to 3e7). At each one the tape reads 011 (110)^k, then the second field as 011 (110)^m (form A) or 00 (011)^m (form B), then small digits. - k grows by exactly 1 per visit (199/199). - The form cycles B, B, A with period 3, like a wide ternary digit. - m stays constant for runs of 1-7 visits, then jumps. Increments: 0 (133 times), +1 (23), +2 (15), +3 (10), +4 (6), +5 (4), +6 (2), +7 (4), +8 (2). Jumps happen at all three form transitions; e.g. m = 125, 129, 135, 142, 143, 144, 146, 150, 154, 162, ... while k runs 156 → 216. - So (k, m) is not (n, a·n + b). This is an orbit measurement, not a rule, and m is only the first segment of the second field.

4. No new local rules this stage, so there are no new validation counts. The 13 observe-stage rules stand (200/200 each, data/validation.json).

Still open (unchanged from observe; now the only route): - pin E (both directions) and J2; - the law for the second field's size (the m jumps above); - then proof.md (two bells + ternary counter with wide digits) and Rocq from BellEatsCounter_1RB0RF.v / SOMDCv6.

The answered decision is in decisions/2026-10-10-decider2.json. The new decision.json asks: hand proof (recommended; its first stage pins these rules, with a stop rule) or park.

Decision (2026-10-12)

Question: The decider route found nothing (384 hlin and 178 CTL runs, all false): start the hand proof with one stage that pins the open rules, or park W4-7 and its sibling 707? Answer: hand (Hand proof, first stage: pin the open rules (about 2 h)). Dennis: apply recommendations (2026-10-12).

Funded stage (2026-10-10, hand)

Run 2026-10-12 (Dennis: apply recommendations). First hand-proof stage: pin the hand-over E (both directions), J2 and the second field's size law. Outcome: the field-size law is exact (a local "bell eats the next digit" law, 673/673 bell-2 ends to 1e9), six new local rules validated 200/200, J2 and the right-part grammar still open. Confidence stays med. The stop rule (park if the size law is not exact) does not fire. Scripts: scripts/handover/ (validate_handover.py, merge_law.py, wsim.c = small C tracer for head turning points and snapshots, tok.py). Data: data/validation_handover.json, data/merge_law_1e9.json.

1. What a traversal is (from the head turning points, 3e7 steps). One field-1 traversal = field 1's marker moving through all k blocks (rule F, one block per pass). Each pass increments the digit chain that starts at field 2. Field 2 is a wide ternary digit (I-rules), so it carries every third pass. The first carry into field 2 after a left visit makes field 2 run as a bell (rule F2 below, m passes, each incrementing the chain from field 3 on). Later carries in the same traversal only cross it (I1a/I1b). The same holds one level down: field 3 sometimes runs as a short bell inside a traversal (the 'two runs per traversal' cases, e.g. step 8,320,923: width 3 → 4). So "bell" and "wide digit" are one object in two modes. A digit runs as a bell when a carry reaches it in the form the last long left sweep left behind.

2. New rules (all 200/200 from random instances, random far contexts with a window check: the head never reads l or r before the RHS; seed 5, data/validation_handover.json).

H2 matches the orbit: at step 8,309,027 the tape is ... 00 (101)^141 111 (110)^105 111 D> 0 (011)^6 000 (011)^3 ..., and the next field-1 marker visit (step 8,310,267) has 000 (011)^112 (105+6+1). H1 is validated as a local rule. Which right contexts actually occur when it starts in the orbit is not pinned.

3. The field-size law (exact; orbit check scripts/handover/merge_law.py). Look at the last field-2 bell pass, where the tape reads 111 (110)^j 1 [F0] 11 (110)^3 Y ([F0]: head on a 0 in state F). After the collapse, field 2 is a wide 0 of width m' = j + 4 + w. Here w is the number of 011 blocks at the very start of Y: the next digit, in its adjacent (011) form, is eaten. When Y starts with 0, w = 0 and the width is unchanged. - 3e7 steps: 180/180 (120 with w = 0, 60 merges). - 1e9 steps: 673/673 (451 with w = 0; 222 merges, w = 1..10: 81, 53, 28, 24, 6, 10, 8, 7, 3, 2). The last width is 631. - 60 of the 734 bell-2 ends have another shape and are not counted: field-3 bell runs inside a traversal, and the first visits.

This explains the jumps of m seen in decider2 (+0 in 133 visits, +1..+8 in 66): m grows exactly when the bell's last pass finds the next digit in adjacent (011) form. Field 1 grows by exactly 1 block per left visit (199/199, decider2). It is the bell at the blank left end, so what it eats is blank. The law is exact as a local rule, but it is not a closed form in the visit count. It depends on the counter's state, as in every bell-eats-counter machine.

4. Not pinned (honest gaps). - The piece between G and the start of the D-sweep (the B> carry into the next digit, where the merge happens) is pinned only through the orbit law above, not as a local rule from random instances. Field 3's forms at the last pass are many (000 (011)^w, 00 (101)^w 1, (011)^w 0, and over 60 shapes of 4-cell digits in shifted encodings). - J2 (the carry past the digit after a wide 2) is not pinned. Probing 1 C> 010 (110)^5 0 0111 R gives different outcomes for each R, and R = 0100 ... / 01 0^inf runs off. - Context matters for halting. The collapse started with Y = (011)^4 0 1 0^inf (not a grammatical tail) halts. So a proof needs the exact right-part grammar (digit encodings by phase, plus which digits are in bell-ready form), not just these rules. - Bounded nesting is not shown: field 3 also runs as a bell, so the "2 big bells + 1 small digit" picture is one level of a recursion.

Next (proof route, unchanged in kind). Pin the right-part grammar as a finite set of digit encodings with phase and ready flags, closed under F/F2/G/H1/H2, the I/K/J increments and the B> carry. Each transition is validated from random grammatical instances, with an abstract simulator that must reproduce the left-visit configurations exactly to 1e9. Then proof.md, then Rocq (BellEatsCounter_1RB0RF.v / SOMDCv6 templates). This is several stages. decision.json asks: grammar stage (recommended) or park.

Decision (2026-10-12)

Question: The hand-over rules and an exact field-size law are now pinned: fund a grammar stage (exact digit encodings, J2, the merge carry, checked by an abstract simulator), or park W4-7 and 707? Answer: grammar (Grammar stage (about 2-3 h)). Dennis: b (fund all five), 2026-10-12.

Funded stage (2026-10-10, grammar)

Run 2026-10-12 (Dennis: b (fund all five)). Goal: pin the right-part grammar (digit encodings, ready flags), J2 and the B> merge carry; check them with an abstract simulator against the real left-visit tapes. Outcome: the grammar does not keep growing. Six digit encodings cover 99.29% of all bell-1 marker turns to 1e9. A digit-level abstract simulator built on five rule groups reproduces 1,540 consecutive turns exactly, 18 left visits among them. It first fails on a narrow edge case at the top of the counter. The stop rule does not fire, but closure is not shown. Confidence stays med, now on a concrete, finite rule set. Scripts: scripts/grammar/ (README.txt, b1z.c, census.py, absim.py, passcheck.py). Data: data/grammar_census_1e9.json, data/absim_orbit_check.json, data/validation_grammar_R600.json, data/validation_grammar_U300.json.

1. Where to look. The checkpoints are the bell-1 marker turns: head in F on a 0, left part exactly 0^inf (101)^a, right part 11 (110)^b followed by the counter. There are 227,415 of them to 1e9 (b1z, 6 s), and the left visits are the case a = 0. No inner bell is active at these moments.

2. Grammar (6 encodings, widths free). Parsed from the cell right after field 1, the counter is a list of digits. Each digit is one of two kinds: - rest (v, n): 0 d (110)^n, with d = 000 / 110 / 010 for v = 0 / 1 / 2; - ready (v, n): d' (110)^n, with d' = 000 / 011 / 001. A ready digit has no boundary cell of its own: its left neighbour is one cell longer.

Narrow and wide digits use the same encoding: n = 0 gives the old 4-cell digits 0000 / 1100 / 0100, and the top 11 / 01 is just the last digit. The "60+ digit shapes" of the last stage were block-phase artifacts of the tokenizer. Census (census.py, backtracking parse): - 225,804 of 227,415 turns (99.29%) parse completely; - the 1,611 others all fail at the very top, which reads ...0001111 or ...000111 (1,592 of them at a >= 3); - the 6 encodings appear at every depth, and no new encoding appears as the run goes on.

3. Rules (digit level; absim.py docstring). One bell-1 pass is inc(field 2). - inc on a rest digit: v < 2 gives v+1; v = 2 gives 0 and carries on (K1-K6, I0/I2/I1a/I1b). - inc on a ready digit: v < 2 gives v+1 (000 → 011 → 001). v = 2 runs the digit as a bell: n increments of the next digit, then the collapse. The digit becomes rest 0, one cell further right, and passes a B> carry to the next digit. A bell run therefore delivers exactly n+1 increments. - B> carry (the merge carry) into the next digit: - rest 0 becomes ready 1; - rest 2 becomes ready 0, and the carry is absorbed; - rest 1 is eaten by the collapsing bell (new width n_i + n_j + 1), and the digit after it is incremented; - a ready digit takes an ordinary inc.

In the last stage's notation this is the size law j+4+w, with w = n_j + 1. - H1 (the field-1 pass with b = 0) is a B> carry into field 2, then b' = a + 1. Of the 667 H1 passes to 1e9, 661 parse with field 2 rest (2: 438, 0: 218, 1: 5); the other 6 fail at the top. Field 2 at H1 is rest in all 18 that the abstract run covers. - Top: an inc past the last digit appends rest (1, 0).

Recursion: field 2 is ready after every left visit, so its first carry runs it as bell 2. Each collapse makes the next digit ready, so field 3, field 4 and so on later run as nested bells. This is the "field 3 sometimes runs as a short bell" of the last stage.

4. Validation. - One bell-1 pass from random grammatical instances (passcheck.py: real TM until the next marker turn vs the abstract render; a <= 6, b <= 8, up to 6 digits, widths <= 8): - 600/600 (seed 5) on the grammar with no two adjacent ready digits, and at H1 field 2 rest and not 1. That is 562 ordinary passes and 38 H1 passes. - Unrestricted (seed 6, 300): ordinary passes 217/217 without adjacent ready digits and 40/47 with them. The 7 failures all start a width-0 ready-2 bell next to a ready digit. H1 passes fail only when field 2 is ready, which never happens in the orbit; 7 instances raise (H1 with field 2 = 1). - Orbit (absim.py): the run starts from the left visit at step 1,016,724 (field 1 = 76 blocks; digits (1,45,ready) (0,7) (1,1) (0,0) (2,0)). It reproduces all 1,540 following marker turns exactly (full right part, string-equal), through 18 left visits (field 1 = 77..94 blocks). That covers every bell-2 run, nested runs of fields 3 and 4, and the merges (e.g. field 2: 45 → 53 = 45+7+1). - First mismatch, at step 2,083,626: at the top, a ready (2, 0) receives a B> and runs a width-0 bell, whose B> meets a rest (1, 0) top digit. The machine leaves ...000111 instead of the merge. This is the same top family as the 1,611 unparsed turns.

5. J2. The observe-stage J0/J1/J2 ('digit after a wide 2': 0011 / 1111 / 0111) are not needed in the new frame. The increment of a ready 2 is the bell rule, validated within the pass rule. No marker turn to 1e9 outside the top family needs another encoding.

Still open: - the top family: width-0 ready-2 bells and merges of a narrow top digit, which leave 111 / 1111 forms (0.71% of turns); - the width-0 ready-2 bell next to a ready digit (7/47 failures); - H1 with field 2 = 1 (at most 5 of 667 H1 passes); - running the orbit check past 2.08e6 to 1e9 once these are pinned; - then proof.md (invariant = this grammar + an arithmetic argument that no top form reaches A> 0 1 0) and Rocq.

The answered decision is in decisions/2026-10-10-grammar.json. The new decision.json asks: one more grammar stage to close the top family (recommended), or park.

Decision (2026-10-12)

Question: The grammar stage found 6 digit encodings and a digit-level rule set that reproduce 1,540 consecutive turns exactly: fund one more stage to pin the top case and run the check to 1e9, or park W4-7 and 707? Answer: grammar2 (Close the top case (about 2 h)). Dennis: 'fund w4-7' (2026-10-12).

Funded stage (2026-10-10, grammar2)

Run 2026-10-12 (Dennis: 'fund w4-7'). Goal: pin the width-0 bell and narrow-top merge forms, extend the abstract simulator until it matches every bell-1 marker turn to 1e9. Outcome: done. The abstract simulator absim2.py reproduces every bell-1 marker turn from step 10 to 1e9 exactly (227,414 turns, 667 left visits). The stop rule does not fire: there is no separate top family. Confidence stays med: the rules are validated and the orbit is matched, but an invariant that excludes the few unsupported configurations is not shown yet. Scripts: scripts/grammar/absim2.py, opcheck2.py, passcheck2.py, orbit_check2.py, ready00_contexts.py, tm47.py. Data: data/absim2_orbit_check_1e9.json, data/validation_grammar2_op20000.json, data/validation_grammar2_pass2000.json, data/grammar2_ready00_contexts_1e9.json.

1. The '111/1111 top family' was a parser artifact. census.py needed every (110) block complete. But the last cell of the top digit lies in the blank 0^inf. With zero-padded tops, all 227,415 marker turns to 1e9 parse in the 6 encodings. For example, ...0001111 is rest (0,0) followed by ready (1,1) = 0000 011 11[0].

2. The real gap: a B> carry into a ready digit. The old rule "B> into ready = ordinary inc" (absim.py) is wrong for every ready kind. That is the first mismatch at step 2,083,626. A ready digit is 0 e (110)^n with a 2-cell core e = 00 / 11 / 01, and a rest digit is 0 e 0 (110)^n. Cell-level traces give the full B> table. The bell is the collapsing digit, of width n; the "next" digit is the one after the target.

• "ready (0,0) + n × ready (1,0)" is the cell string 000 (011)^n. The bell does not take the target's leading cell, which is the same tape as a rest (0,n) whose last cell is lent to the target. The orbit uses this split 5 times.
• B> into ready (0,0) sets the leading cell of Y to 1. The re-read in the 6 encodings is a closed form:
• Y = rest (0,m): ready (1,0), ready (0,m);
• Y = rest (1,m): ready (1, m+1);
• Y = ready (0,m), m ≥ 1: rest (1,0), rest (1, m-1);
• Y blank (top): rest (1,0).
• Any other Y (rest 2, ready 1 or 2, or a non-top ready (0,0)) leaves a flagged digit (leading cell 1). That is outside the grammar and can halt: ready (2,0) followed by a flagged rest 2 halts at its next inc, through the B> 1 0 path.
• H1 (field 1's B> into field 2) follows the same table:
• rest 1 is eaten: the next b is a + 1 + m + 1, then inc(next);
• ready (1,0) is eaten, then B> passes into the next digit.
• Field 2 ready (0,·), ready (2,·) or ready (1, m ≥ 1) at H1 is unsupported. With ready (1, m ≥ 1) the next marker turn is not a left visit (a' = a + 2).

3. Validation from random instances (unrestricted grammar: adjacent ready digits allowed, widths 0-8). - Op level (opcheck2.py, seed 41): an inc arrives at digit 0 (1 C>, left stub 11) and the real TM runs until the head leaves to the left. 19,907/19,907 pass, 0 fail, 93 unsupported (all B> into ready (0,0) with an unsupported Y). Rule uses in passing instances: - bell 4,170, split 276; - B> into rest 0 / 1 / 2: 973 / 1,113 / 982; into the blank top: 402; - B> into ready 2 / 1: 475 / 422; into ready (0, ≥1): 125; into ready (0,0): 100 (top 45, rest 1 21, ready 0 20, rest 0 14). - Pass level (passcheck2.py, seed 13, real TM to the next bell-1 marker turn): 1,405/1,405 (840 H1, 565 ordinary), 0 fail, 595 unsupported (592 H1 into a ready field 2, 3 B> into ready (0,0)). H1 with field 2 = rest 0 / rest 1 / rest 2 / ready (1,0): 233 / 267 / 277 / 63.

4. Orbit check to 1e9 (orbit_check2.py). Start: the first bell-1 marker turn, at step 10 (a = 0, b = 0, digits [rest (1,0)]; it is 10 concrete steps from blank). - Every later marker turn matches: 227,414 of 227,414 (a and the full right part, exact string), 667 left visits, at most 9 digits. - Final state at step 999,967,828: a = 2, b = 672, digits ready (2,631), rest (1,3), rest (2,0) ×3, rest (1,0), rest (2,0). - Rule uses: inc rest 0/1/2 = 212,722 / 212,587 / 211,566; inc ready 0/1 = 1,037 / 1,978; bell 1,956; B> into rest 0/1/2 = 779 / 623 / 1,017; blank top 163; ready 2 21, ready 1 13, ready (0,0) 20 (10 top, 10 rest 1); split 5. - H1 667 times. Field 2 is rest each time: rest 0 221, rest 1 5, rest 2 441. - No unsupported case occurs. The dangerous pattern (a ready 2, any ready 1 digits, a ready (0,0)) appears at marker turns only at the very top: 587 turns, with Y blank, ready (1,0) or rest (1,0) (data/grammar2_ready00_contexts_1e9.json).

Still open (the step to proof.md): - an invariant on digit lists, closed under the rules, that excludes both unsupported configurations: - (a) field 2 ready at a left visit; - (b) B> into a ready (0,0) whose next digit is rest 2, ready 1 or 2, or a non-top ready (0,0).

The orbit data say (b) is a top-of-counter effect: the ready (0,0) is always within the last two digits. - then the non-halting argument (the rules compose into passes, E0 is read only in the excluded configurations), then proof.md and Rocq (BellEatsCounter_1RB0RF.v / SOMDCv6; start B = IndBECv1 _3ary nonhalt3).

The answered decision is in decisions/2026-10-10-grammar2.json. The new decision.json asks: an invariant stage (recommended) or park.

Decision (2026-10-12)

Question: The digit-level simulator now matches all 227,414 marker turns to 1e9 with validated rules: fund an invariant stage that shows the unsupported cases never occur (then proof.md), or park W4-7 and 707? Answer: invariant (Invariant stage (about 2-3 h)). Dennis: 'Invariant stage' (2026-10-12).

Funded stage (2026-10-10, invariant)

Run 2026-10-12 (Dennis: 'Invariant stage'). Goal: a property of digit lists, closed under the absim2 rules, that excludes the two unsupported cases: (a) field 2 ready at a left visit; (b) B> into a ready (0,0) whose next digit Y is rest 2, ready 1 or 2, or a non-top ready (0,0). Stop rule: park if no small invariant closes.

Outcome: the stop rule fires, and W4-7 (with 707) is parked. No property of the digit word can exclude these cases. The orbit avoids them because of exact sizes: changing one field size by 1 makes nearby orbits reach them. Most cases reached this way do not halt: about half are parse artifacts (the same tape has another parse that absim2 handles), and the rest need top rules that absim2 does not have. But 3 of the 69 do halt in the real TM, within 400,000 steps. All three have a ready (2,0) as Y, and all three come from a large change of one width. So halting tapes sit inside the 6-encoding grammar at the level of the digit word. A proof needs a quantitative invariant (counter value against the field sizes), which is not small. Line 707 (start C) is now matched by absim2 to 1e9 as well. Confidence stays med on the mechanism; not a cryptid candidate (see 3). Scripts: scripts/invariant/ (README.txt). Data: data/invariant_*.json, data/absim2_orbit_check_707_1e9.json.

1. Where the ready digits are. Call a ready digit a wave: the collapse of the bell to its left made it ready, and it will run as a bell itself. waves.py runs absim2 alone for 20 million passes (the 1e9-step orbit is 227,414 passes): 0 flags, at most 10 digits, field 2 width up to 6,214. - At all 6,317 left visits, every ready digit is among the last three digits (1,022 / 92 / 310 at distance 0 / 1 / 2 from the last digit), and case (a) never occurs. - Of two consecutive ready digits at a marker turn, the upper one is always among the last four digits (258,397 / 19,150 / 1,584 / 15 at distance 0 / 1 / 2 / 3). - Every B> into a ready digit (139 times) happens among the last three digits.

Below the top a wave climbs one digit per bell. It dies at the first rest 1 (it eats it), and it cannot pass an older wave. Case (b) needs a new wave to reach an older one. On the orbit this happens only at the top, because each field-2 bell (n0 increments into the rest of the counter) pushes all older waves up there. At left visits the counter above field 2 has a value close to n0 (for example 2,333 vs n0 = 2,366). So the safety is a balance of sizes, not a matter of form.

2. The stop rule: no invariant on the digit word. perturb_check.py takes 237 orbit states at left visits (passes 2,000 to 300,000). It changes one number, keeps the digit word (kinds, widths 0 / >= 1) and everything else, and runs absim2 for 30,000 passes.

Every hit is case (b). In 94 of the 98 hits Y is ready (1,0) (else ready (2,0) or ready (1,1)). An invariant that excludes the unsupported cases must therefore tell apart field sizes that differ by 1. Any invariant that depends only on the digit word (and a, b) contains one of these perturbed states, so closure would carry it to an unsupported case. A quantitative invariant (counter value against n0 and a) would not be small, and it was not attempted.

3. What the unsupported cases are: mostly missing rules, a few halts. - Where: all 69 distinct flagged runs hit case (b) within the last four digits (flag_where.py: distance 1 / 2 / 3 from the last digit: 2 / 57 / 10). 55 of them are the same top: ready (0,0), ready (1,0), rest (1,0). - Parse artifacts (reparse_check.py, data/invariant_reparse.json). The 6 encodings are ambiguous at digit borders: ready (1,0) rest (1,m) = rest (1,m+1), and ready (1,0) rest (0,m) = rest (1,0) ready (0,m). Every parse of each pre-flag tape was tried; 3,238 parses in all: - 35 of the 69 states have another parse on which the pass is supported; - all 1,578 unflagged parses give exactly the real TM's next marker turn (0 mismatches; this also cross-checks the rules); - 34 states have no supported parse. - Real TM (flag_tm.py, data/invariant_flag_tm.json): from each of the 69 pre-flag marker turns, up to 2e9 steps. - 66 do not halt. Eight of them were followed for 300 more marker turns: in 7 all 300 turns parse in the 6 encodings again, in the eighth 261 do. - 3 halt, at steps 61,670 / 307,823 / 376,776. Each is a B> into ready (0,0) followed by ready (2,0), near the top: ... ready (2,0), ready (0,0), ready (2,0) (twice) and ... ready (2,0), ready (1,0), ready (1,0), ready (0,0), ready (2,0). They come from the redraws (n0 redrawn twice, all widths once), less than 1.1 traversals after the change. - The runs started from the ±1 / ±3 / ±10 changes all reach Y = ready (1,0), and none of them halts in 2e9 steps (that is far beyond the 30,000 abstract passes). - Op level (flag_probe.py, seed 7, data/invariant_flag_probe_op4000.json): 4,000 random instances of a width-n bell into ready (0,0), Y, tail; 1,586 of them absim2 calls unsupported. Real TM: 0 halts, 0 timeouts. 185 results parse in the 6 encodings (Y = ready (0,0): 127, ready (1,0): 58). 1,401 leave a digit whose leading cell is 1 (a flagged digit, outside the 6 encodings). - Known from grammar2: a flagged rest 2 after a ready (2,0) halts at its next inc. In the three halts above the flagged digit is a ready (2,0) instead; their cell-level path to E0 was not traced. - Cryptid check: the halts need a drastic size change and happen at once, and the long perturbed runs never halt. So there is no sign of pseudo-random arithmetic deciding halting. The orbit looks like a stable balance (counter value near n0) that nearby states rejoin. Not a cryptid candidate, but no proof route in reach either.

4. Line 707 (start C of this table). b1zs (b1z with a start state) to 1e9, then orbit_check_start.py. absim2 reproduces every bell-1 marker turn from step 117 (a = 0, b = 3, no digits) to 1e9: 226,216 / 226,216, 669 left visits, at most 8 digits (data/absim2_orbit_check_707_1e9.json). The six turns before step 117 include an H1 into a lone top ready (2,0), which absim2 does not support. In the TM that digit simply disappears (b' = a + 1). A proof covers these turns by direct simulation.

Still open (restart route, if the machine is picked up again). - (i) Make absim2 total near the top. Re-parse the ambiguous border pairs, and pin B> into ready (0,0) for every Y together with the flagged-digit forms it leaves. Validate from random instances, and use the perturbed orbits as a stress test. - (ii) That alone is not enough, because the halting tops (ready (2,0), ready (1,0)*, ready (0,0), ready (2,0), then B>) are word-level grammatical. The invariant must be quantitative: for example, every ready digit at a left visit lies in the last three digits, kept true by a size balance (counter value near n0, a - n0 small). No candidate was found. - Then proof.md and Rocq.

The answered decision is in decisions/2026-10-10-invariant.json. Parked by the stage's own stop rule, as Dennis agreed when funding it, so no new decision.json.