/machines/1RB---_1LC1RE_1LD0LC_1LE1LC_1RF0RE_1RA0RB/notes.md · raw

1RB---_1LC1RE_1LD0LC_1LE1LC_1RF0RE_1RA0RB

Status: KILLED_NONHALT (stage done, 2026-10-13; see ## Kill at the end) Class guess (agent / Dennis): 3/2 wall conveyor + right-edge counter (sheet: Structural counter + counter) / — Spreadsheet notes / Discord thread: Results row 842, no status, notes, links, strikethrough or comments. Not in data/discord lists (dyuan 24, mxdys UBRRBA 86). Viewer: https://bbchallenge.org/1RB---_1LC1RE_1LD0LC_1LE1LC_1RF0RE_1RA0RB

Observation

Candidate rules

Checked by validate_rules.py: random n, m (0–3, 4–40, 100–3000), random context words on both sides, exact step counts. Each rule passed 140/140. A mutation check (wrong steps, wrong RHS, Lw2 claimed to pass) fails 0/140, as it should.

S_R   B> (11000)^n                 --> (10111)^n B>                          5n
S_L   (11110)^n <C                 --> <C (00011)^n                          5n
S_L'  (10111)^n <C                 --> <C (11000)^n                          5n
EdgeR E> 0^inf                     --> 1^3 <C 1 0^inf                        4
EdgeL 0^inf <C                     --> 0^inf 1 0 B> 1                        4
W0    B> (11000)^n 0               --> <C (11000)^n 1                        10n+1   (bounce; wall -> W1)
W1    B> (11000)^n 1 (11000)^m     --> (10111)^n 1 00111 (10111)^(m-1) B>    5n+5m+1 (pass; m>=1)
Lw1   1 00111 (10111)^m <C         --> 000111 (10111)^m B>                   10m+11  (bounce)
Lw2   000111 (10111)^m <C          --> 101111 (10111)^m B>                   10m+11  (bounce)
Lw3   101111 (10111)^m <C          --> <C 110000 (11000)^m                   5m+6    (pass; wall now 5 cells right)

Cycle (validate_cycle.py): X(a, R) reaches X(a', R') two C-left-records later with the prefix unchanged in 40/40 random cases (a in 60..300, the 4 observed R). a' − a ranges over 4..12 and depends on a. The observed successor R' is reproduced only at the run's own a. Spot-checked at a = 182 and 198: both match the run, including the step count (25,925,018). Robustness: 200 random perturbations of segment lengths (±1..5 blocks in 1–3 segments) of the step-1,139,175 tape. None halted within 1e8 steps.

Checkpoint A (Dennis)

Informal proof

proof.md (2026-10-12, round-3 self-review), validated by check_proof.py S1-S12. Every lemma is proved; nothing in the informal argument is open. Next: Checkpoint B (Dennis), then the Rocq formalization (proof.md §10). See the last stage section.

Formalization log

rocq/log.md (rounds 1-4; kill file assembled in round 4).

Outcome

KILLED_NONHALT (2026-10-13): check_kill PASS, independently re-verified, packaged in submission/. See ## Kill.

Card data pass (2026-10-10)

The card now shows at most 3 short mechanism bullets and yes/no questions that point at figures by number (primary figures first). The text they replaced is kept here. - Figure order on the card: Fig 1 = img/zigzag_every8_from1139175.png, Fig 2 = img/phase_solid_every100_from1139175.png, Fig 3 = img/default_site_1e4.png, Fig 4 = img/records_1e8.png, Fig 5 = img/blaze_1e8.png (Figs 1-2 primary). - Mechanism, full observer version: - Tape is a period-5 pattern: B sweeping right turns dark 11000 into light 10111; C sweeping left turns it back (5 steps/block). - Segments are separated by walls (+1 phase step). A wall is a 5-state gadget: B bounces once then passes, C bounces twice then passes; one round moves it 5 cells right. - So each wall is crossed 3/2 times as often as the wall to its left: walls drift right x1.5 per level, segments 12, 18, 27, 41, 61, 92, 138, 206 blocks. - Every 2 left records the whole prefix repeats exactly (left edge -8 cells): a new wall is born at the left, the outermost one is absorbed at the right. - Right barrier = period-4 0001 zone plus a lone 1 behind a growing gap (second counter); right edge about +32 cells per cycle, span ~ t^(1/3). - Checkpoint questions before the rewrite (some were decisions, not questions about a figure): - Diagram 1: do the colour bands read as walls drifting right and fanning out, with new bands born at the left edge? - Diagram 2: is each long vertical line a wall the head bounces off (1 bounce from the left, 2 from the right, then a pass)? - Not a cryptid (the 3/2 rounding only sets wall spacings, no halting branch): go for a list-of-walls invariant proof?

Deepen pass (overnight 2026-10-10)

Outcome: confidence stays med (better evidence, one named gap). Not a cryptid. Recommend one more targeted observation pass (the right-zone language) before proof work. Scripts are in scripts/, results in scripts/results/.

1. Every head event to 2e10 steps is one of 19 rules (scripts/junctions.py, results/junctions_2e10.json). The coverage simulator applies 6 sweep macros with a variable length n ≥ 1. Everything else is simulated directly as a "junction" and stored by its visited window. From the blank tape to 20,000,003,117 steps it sees only 13 junction types. The final tape, head and state match the C core exactly (also at 1e8 and 1e9). Macro counts: SR 8.5M, SR6 2.6M, SL' 4.3M, SL 4.3M, KB 4.3M, KC 5.6M.

sweeps:  SR  B> (11000)^n -> (10111)^n B>  5n     SL' (10111)^n <C -> <C (11000)^n  5n
         SR6 B> (111000)^n -> (100111)^n B> 6n    SL  (11110)^n <C -> <C (00011)^n  5n
         KB  B> (1000)^n -> (1111)^n B>   4n      KC  1^n <C -> <C 0^n              n
junctions (count to 2e10):
 J1 B> 0 -> <C 1                          1   (5.2M)  W0 bounce / set a counter digit
 J2 0 0 0 <C -> 1 0 B> 1                  4   (2.6M)  C bounce at a dark wire; EdgeL
 J3 1 0 0 <C 0 0 0 -> 0 0 0 1 1 1 B>      8   (2.6M)  Lw1 core (E-F-A run over 000; halts if that cell is 1)
 J4 1 <C -> <C 0 (isolated 1)             1   (1.3M)
 J5 1 0 0 <C 0^4 -> 0 0 0 1 1 1 <C 1      9   (1,145)  J3 + J1 with a 0-block wire (wall meets the zone)
 J6-J10: 5 left-edge (nursery) windows, 7-22 steps, 287-863 each (1-3 per cycle); J11-J13: the first 75 steps only

scripts/validate_deepen.py: all 13 rewrites hold with random context outside the window (520/520).

2. Right barrier = binary counter (closes the "second counter" gap). Its digits are period-4 cells: 1000 = 1, 0000 = 0, least significant digit next to the last wire. Rule K: (10111)^m B> (1000)^j 0 --> <C (11000)^m (0000)^j 1 in 5m+8j+1 steps, 192/192 (random m, j from 0, random context). Each B arrival is one increment. A dark block 11000 inside the zone passes carries through (B sweeps it), so the zone is digits plus single wire blocks and lattice shifts. One cell per new top digit is the only way the counter itself moves the right edge. The +32 cells per cycle come from the wires getting longer.

3. Walls are rotors: 2 arrivals in, 3 out (the 3/2 law, now exact). The event order at a wall is fixed by its state: b b c c c. An arrival from the left at W1 forwards exactly 3 arrivals to the next wall, and one at W0 forwards none. A binary digit is the same kind of rotor with 2 in, 1 out. Lemma (derived, not yet machine-checked): the leftward crossings of an interior wire alternate between "no change" (the right wall's W0 bounce) and "+1 block" (its Lw3 pass). Its left wall eats one block per 3 such crossings. So the wire length, read at each W1 pass of its left wall, never decreases (+0, +1 alternately), and interior walls never collide. The last wire is different: only its left wall acts on it, so it shrinks by 1 per round until the wall is absorbed into the zone (J5).

4. Left edge = exactly periodic nursery. From 203,465 steps on there are 2,251 left records. All of them come in the fixed 8-record cycle XC XD XE YC YD YE ZD ZE, each with its own fixed prefix. The 282 X records have the identical prefix 1^6 0 00011000011^2 00011^2 10001^3 10 00011^6 10001^8 11000^12 1, and the left edge moves −8 exactly per X record. Each cycle the nursery sends one wall into the conveyor.

5. Levels (regime transitions) to 2e10. The frozen wire lengths at X records are 12, 18, 27, 41, 61, 92, 138, 206, 309, 463, 695. The last one is the latest level, frozen at about 1.54e10. Each new level freezes when the growing last wire reaches about 1.5× the one before it. Level start times: 18 @4.6e5, 27 @1.1e6, 41 @3.4e6, 61 @1.1e7, 92 @3.9e7, 138 @1.24e8, 206 @4.1e8, 309 @1.38e9, 463 @4.59e9, 695 @1.54e10, about ×3.3 in time per level. Every level-up is made of the same 19 rules (item 1). There is no new regime.

6. Closure tests. These run random members of the abstract family: the real X nursery, random W0/W1 wall states, random wire lengths and a random zone. - closure_test.py (junction catalog): 100/100 runs at 5e7 steps with wires 1..20, and 60/60 at 1e8 steps with wires 1..400. No halt and no new junction type. - closure_records.py (C core, every left record): with the zone lattice offset ≡ 3 mod 4 after the last wall cell, the offset seen in the blank-tape run, 150/150 runs reach 5e7 steps without halting. Offsets 0/4: 48/48 no halt. Offsets 1/5: 31/48 halt; 2/6: 48/48 halt. A random nursery prefix P with random walls also halted (1 of 8). - So the machine is NOT robust to any zone alignment. The invariant has to fix the zone lattice phase relative to the last wire (≡ 0 or 3 mod 4). The blank-tape run keeps offset ≡ 3 at every left record. Random wall states and wire lengths do not break it, so the alignment is held structurally (absorption puts it back), not by arithmetic luck. The strict zone regex 0^(4k+3) (0000|1000|11000)* 1 is too narrow: 110 of 150 aligned runs leave it without halting, through single-0 lattice shifts inside the zone, the same as the 56 blank-tape records it misses.

Non-halting argument (sketch). A halt needs A to read 1. A runs only inside an E-F-A pass over cells that every rule above requires to be 000. So a halt needs a junction outside the catalog. The tape at left records is nursery · (wire ≥ 1, wall) · aligned zone. Each piece keeps its form: the nursery is exactly periodic, interior wires never shrink (item 3), the zone is a binary counter (rule K), and absorption is J5 plus the standard rules. Open:* the exact closed language of the aligned right zone (where single-0 shifts may sit, and that the alignment survives every absorption). This is the one remaining gap before proof.md.

Deepen pass 2

Outcome: confidence stays med. Recommend more observation, aimed at one coincidence condition (below). The zone-language gap from round 1 is closed: the exact language is now known, and the open point is narrower than before. Not flagged as a cryptid, but see item 5. Scripts are in scripts/deepen2/. All numbers are in scripts/deepen2/results/summary.json.

1. One cell language for everything right of the nursery (L_gap). Read the tape as 1-runs and the 0-gaps between them. At every left record from 2e5 to 2e10 (2,251 records), every run after the first 3 (the left edge) satisfies three conditions (realcheck.py, 0 violations): - each run has length 1, 2 or 3; - each gap is at least 3 and is 0 or 3 mod 4; - each 3-run follows a gap that is 3 mod 4.

The residue of the gap before a run tells you what the run is:

gap = 3 mod 4:  run 1 = counter digit 1 (1000)   run 2 = P (11000, wire/pass block)   run 3 = W (W1 wall: 1 11000)
gap = 0 mod 4:  run 1 = S1 (shift + digit, 0 1000)   run 2 = SP (W0 wall: 0 11000)     run 3 = forbidden ("sW")
each extra 4 zeros in a gap = one 0 digit (0000)

Walls, wires, the binary counter, round 1's "single-0 lattice shifts" and the 11000 blocks inside the zone are all units of this one alphabet. A wall Wx:n is the unit SP or W followed by n-1 P units. The halting offsets 1 and 2 from round 1 are gaps of 1 or 2 mod 4, which means two shifts in one gap.

2. One B arrival is an exact carry rewrite (unitinc.py; matches the machine on 79,527 of 79,527 random arrivals, checkinc.py). The carry enters at the bottom unit:

0 digit -> 1, stop        1 digit -> 0, carry on        P -> P, carry on
S1 -> P, stop             SP (W0) -> W (W1), stop
W -> its rest gets 3 carries, then W becomes P and a shift (one 0 cell) attaches to the first run above

Rule K, the rotor rules W0/W1/Lw1-3 and wall absorption (J5) are special cases. - Absorption is the W rule when the last wall's wire is down to 1 block. The shift lands on the first run above: on a 1 digit it becomes S1, which becomes P on its next carry. On a zone P it becomes SP, a zone wall that climbs through P blocks and dissolves at the next 1 digit. - Lattice alignment is self-repairing. Every shift ends as P or as a wall, so the counter never sees gaps of 1 or 2 mod 4.

3. Closure tests. Each test applies repeated arrivals to the right end, using the machine in isolation (arr.py). This is exact, because the right end only ever gets B from the left and returns C. - Random L_gap words (explore4.py): 2,984 of 3,000 stay in L_gap for 60 arrivals and 0 halt. All 16 exits are a shift landing on a W. - Natural family (explore6.py): conveyor walls with wires 1..12 plus a random digit/P zone stay in L_gap for 400 arrivals in 1,500 of 1,500 cases. With one S1 or SP planted in the zone, 1,498 of 1,500 stay in. Both exits are an interior 1-block wire directly followed by a wall (SP W, W W), which the interior-wire lemma rules out outside the periodic nursery. - A looser language that allows 4-runs degrades: runs grow up to 18, gaps of 1 appear, and 1 of 3,000 runs halts (explore5.py). So L_gap is the right invariant shape.

4. The one open point: a wrap coincidence. The W rule leaves L_gap only in one situation: - a W whose wire is down to 1 block finishes a round, - the k digits between it and the next non-digit unit X wrap to exactly 0 under its 3 carries (value 2^k−3 before, k ≥ 2), and - X is a wall (SP or W).

The shift then lands on a wall (cells 0111000). In the blank run to 2e10 (zonewalls2.py; to 2e9 and to 2e10 give the same counts, and no zone wall appears after 2e9): - at most 1 zone wall exists at a time, and 11 of 2,251 left records have one; - no two wall units are ever separated by digits alone; - but 6 of those 11 zone walls sit on digits only, directly above the last conveyor wire. These are the candidates for the coincidence when the next last wall arrives.

Timing makes the coincidence unlikely. A zone wall over k digits moves on after 2^(k+1) carries. The next last wall needs about 3× its wire length in carries (the wire is 100s of blocks) to reach the digits. The coincidence also needs the k digits to wrap at that exact round. This is a counting argument, not a structural one.

Forcing the coincidence (coinc.py, 400 cases) leaves L_gap in 154 cases, and none halt within 3,000 arrivals. So a shift on a wall is not immediately fatal, but its rules are not written yet.

5. Cryptid assessment. The local dynamics are a fixed, fully validated rewrite, so this is not a cryptid in the rule sense. However, the L_gap invariant holds only if a counter-value coincidence never happens. Closing that needs one of two things: - (a) a timing invariant: "a zone wall that sits on digits only is gone before the next last wall reaches it". This has to be argued from the 3/2 wire growth. - (b) a larger closed language that also gives rules for the 0111000 (shift-on-wall) states.

Next step: derive the shift-on-wall rules with arr.py (two to four arrivals on 0111000+context). If they always reduce back to L_gap, (b) gives a purely structural invariant and the proof can start (proof.md = nursery period + interior-wire lemma + L_gap closure under the unit rewrite). If they do not, (a) is needed, and Dennis should decide whether that counts as pseudo-random arithmetic.

Decision (2026-10-10)

Question: Spend one short targeted stage on rules for the shift-on-wall (0111000) states before proof.md, start proof.md now with the wrap coincidence as an open lemma, or park? Answer: targeted_deepen (One targeted stage (at most 2 h): rules for the shift-on-wall states). Dennis: go with all recommendations (2026-10-10).

Funded stage (2026-10-10, targeted_deepen)

Outcome: confidence stays med. The shift-on-wall states now have exact rules and every single or double hit returns to L_gap, but no purely structural closed superset of L_gap exists: a third hit on the same wall can halt. The coincidence itself is now understood exactly. At the conveyor top it is impossible (a divisibility lemma). Inside the zone it happens exactly when 3m+1 = 2^k. Scripts are in scripts/deepen3/, numbers in scripts/deepen3/results/summary.json.

1. One alphabet for all states: head words. Every unit is h 1000 (h a 0/1 word with no 000), plus the 0 digit 0000. The L_gap units are h = ε (digit 1), 0 (S1), 1 (P), 01 (SP), 11 (W). A shift s lands on the first unit above and prepends a 0 to its h. Two rules cover every unit: - the first cell is 0: it flips to 1 and the carry stops (B> 0 -> <C 1, J1). This is the rule for SP, S1 and every shifted unit; - otherwise the rule depends only on h (hrules_all.py, all 94 head words of length ≤ 6, 300 random rests each). 64 have one exact local rule h 1000 r -> h' 1000 s^e inc^f(r), 16 halt, 4 exit left in state D/E (they act on the unit below), 10 have no unit form.

h (unit)        one carry                         h (unit)        one carry
0     (S1)   -> 1 (P), stop                       011  (sW)    -> 111 (Q), stop
1     (P)    -> 1, 1 carry on                     111  (Q)     -> 01 + s, 2 carries on
01    (SP)   -> 11 (W), stop                      001  (sSP)   -> 101, stop
11    (W)    -> 1 + s, 3 carries on               101          -> 01 + s, 1 carry on
0111         -> 1111, stop                        0101         -> 1101, stop
1111         -> 111 + s, 2 carries on             1101         -> 111 + s, 1 carry on
01111, 01101 -> 11111, 11101: E runs left out of the unit (no local rule; halts in context, item 3)

The depth of a unit is the number of shifts it emits before it is P: 1 for SP and W, 2 for 001/011/101/111, 3 for 0101/0111/1101/1111. A shift landing on a wall of depth d (right after the carries it brought) gives depth d+1. Starting from L_gap and letting a shift land after 1-3 carries, 22 head words are reachable (tower closure). All 12 of depth ≤ 3 have local rules, and depth 4 is the first that does not.

2. The extended carry model equals the machine. incplus.py (the two rules plus the table) against arr.arrive (checkplus.py): 79,839 of 79,839 arrivals with a planted sW or Q, and 78,765 of 78,765 with planted depth-2/3 towers, 0 mismatches and 0 halts. Every arrival the model could not handle (45) has a depth-4 head (11111 ×28, 11101 ×15, 111101 ×2).

3. Towers of depth ≤ 3 always come back. Depth 4 can halt (tower.py 1 40 3000, one tower planted in a natural word: conveyor walls with wires 1..30 and a random zone): - depth ≤ 3 (11, 011, 111, 0111, 1111): 200 of 200 runs return to L_gap, 0 halts; - depth 4 (01111, 11111): 13 of 80 halt; - depth 5-6: 7 of 160 halt or exit left; 01111111 and 11111111: 80 of 80 halt. - Forced coincidences (ctrack.py 2 3000 3000, as in coinc.py with richer contexts): 635 of 3,000 leave L_gap, all 635 return, 0 halts. The longest excursion is 2,260 arrivals, and depth-3 heads (0111, 1111, 001, 101) occur. 3,000 random L_gap words × 3,000 arrivals (hexplore.py): 0 halts, 31 reach depth 2 and all return. - So the closed superset of the decision exists only with a cap on hits per wall. L_gap plus all depth ≤ 3 states is closed exactly when no wall is hit 3 times. That cap is a counting statement, not a structural one.

4. When a shift lands on a wall (exact). A wall emits s with f ≥ 1 carries, and s lands on the first run above after those carries. It lands on a wall X only if the whole digit block between emitter and X wraps to exactly 0 at that moment. - Creation lemma (structural). Digit positions can turn into P (via S1) but never back, and a wall that moved leaves a P behind. So a wall X directly above a pure digit block was put there by a shift that jumped that block when the block was 0. The emitter was the unit directly below the block, and it is P right afterwards. After every absorption the bottom zone block is all 0: either it wrapped, or s split it at its lowest 1 digit. - Conveyor-top lemma (structural, mod 3). Between two absorptions the zone receives carries only from the last conveyor wall, exactly 3 per round. A zone wall X over the bottom block (k digits, created at an absorption with the block 0) has N = 3n carries after n rounds. A hit on X needs N = 2^k (X = SP after 1 carry) or N = 2^(k+1), and neither is a multiple of 3. After 2 carries X has moved on. So the coincidence named in the decision (last wall W:1 → shift on a zone wall) never happens. toplemma.py: n = 1..120 rounds, k = 0..8 digits, last wall in W or SP state, 2,160 of 2,160 stay in L_gap through the absorption. A zone wall over a nonzero block, which the creation lemma rules out, is what coinc.py forced. - Zone-internal coincidence (arithmetic). The remaining way needs 2 zone walls. U1 sits over the bottom block B0 (k0 digits) and jumps the next block B1 (k1 digits) to create X. A later absorption makes B0 wrap exactly again (the last wall ran n = m·2^k0 rounds), which puts a wall back on U1. When U1 fires again, B1 has received 3m+1 carries since X was created. So X is hit exactly when 3m+1 = 2^k1 (m = 1, 5, 21, …). Constructed in zcoinc.py: 6 of 6 cases with 3m+1 = 2^k1 reach sW, and 4 of 4 with 3m+1 ≠ 2^k1 stay in L_gap for 4,000 arrivals. For depth 3 on the same X the simplest chain needs the next absorption interval to be the same n again. Other chains (blocks split at an absorption, longer nestings) each add one more condition on the interval lengths mod powers of 2.

5. Blank run: no hit at all to 2e10. A stacked unit that takes its second carry runs a junction outside the 13-type catalog (jstack.py: 40 of 40 planted sW/Q configurations with the real nursery make new types). The blank run to 20,000,003,117 steps uses only the 13 types, and L_gap holds at all 2,251 left records. So no wall was ever hit in that range, not only at the sampled records. zoneview.py 2e10: zone walls at 11 of 2,251 records, never 2 at once.

Still open. - Show that no zone wall is hit 3 times (depth 4). The hits are fixed by the absorption intervals n_j (rounds of each last wall between absorptions) mod powers of 2 and by 3m+1 = 2^k. The n_j come from the 3/2 conveyor. The next step is to extract n_j from the blank run, drive an abstract zone automaton with them (exact by items 1-2), and list the interval patterns that give 1, 2 and 3 hits on one wall. If 3 hits need a pattern the conveyor structurally avoids (for example equal consecutive intervals), the proof is structural. If they need only n_j mod 2^k conditions, this is Mahler-type 3/2 arithmetic, and the machine is a cryptid candidate. - The nursery period and the interior-wire lemma are still argued and sampled, as before. - Answered decision moved to decisions/2026-10-10-targeted_deepen.json. New decision.json: chain_stage (recommended: one stage on hit chains vs absorption intervals), cryptid_flag, proof_conditional, park.

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

Question: Spend one more targeted stage testing whether the conveyor's absorption intervals can ever give one wall three hits, flag the machine as a cryptid candidate now, or park? Answer: chain_stage (One more targeted stage (at most 2 h): hit chains vs absorption intervals). 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.

Funded stage (2026-10-10, chain_stage)

Outcome: not a cryptid candidate; confidence stays med, with a much narrower and structural gap. The absorption intervals follow an exact counter-type law (a period-32 table plus a ruler term), not 3/2 arithmetic. Under that law no zone wall is ever hit, and three stacked hits would need repeated intervals of exactly 2^p, which the law never produces. Per this stage's stop rule, proof.md can start. Two lemmas are still observed rather than proved (below). Scripts are in scripts/deepen4/, numbers in scripts/deepen4/results/summary.json.

1. The blank run's right end replayed exactly from record to record. match.py takes the top K conveyor walls plus the zone at each left-record group, feeds carries at the bottom with the deepen3 unit model, and finds the record's successor. K starts at 3 and grows when all K walls are absorbed in one interval; the Y→Z intervals absorb 3 walls each. Results: 843/843 intervals to 2e10 and 988/988 to 3.18e10 reproduce the next record exactly (0 failures). This gives every absorption: 2,238 to 2e10 and 2,623 to 3.18e10, about 8 per nursery cycle.

2. Zone automaton driven only by the intervals. Let N_j be the carries that cross the zone boundary between absorption shifts j-1 and j. One step of the automaton is "N_j carries at the zone bottom, then the absorption shift". Leading P units join the next wire. - zcheck.py: it reproduces the zone at every record group (843/843 to 2e10, 988/988 to 3.18e10). - fastzone.py (bulk carries) matches it after every one of the 2,238 absorptions. - fzmachine.py: against the machine itself on random zone words with zone walls, 2,000/2,000 instances and 7,010 carry batches plus shifts, 0 mismatches.

3. Correction to the round-3 conveyor-top lemma. That lemma assumed N = 3n (3 carries per round of the last wall). In the real run N mod 3 is 747/744/747. When a wall is absorbed, the rest of the triple the wall below was emitting goes straight to the zone (in-flight carries). The lemma's conclusion (the last wall never lands a shift on a zone wall) still holds, but for the reason in item 4. The 2,160 toplemma cases only covered δ = 0.

4. Absorption-interval law (observed, exact). N_j = j + 50 + g(j), where j is the absorption index: - g(j) depends only on j mod 32 for residues 1..25: -3 -2 -4 -6 3 1 -1 0 -3 -2 -4 -6 0 3 -1 0 -3 -2 -4 -6 3 -5 -6 -6 for residues 2..25 (residue 1 gives 0). There are 0 violations in 2,623 absorptions. - The other 7 residues (26..31 and the next 0) form one of 7 tuples per 32-block b, chosen by ν2(b+2) (a ruler sequence). There are 0 violations in 80 blocks, ν2 = 0..6 seen; ν2 = 2 and 4 share a tuple, and ν2 = 5 and 6 each brought a new tuple. A 32-block is 4 nursery cycles, matching the 8,8,4,12 growth of the X-record wire. - Consequences: N grows by exactly 1 per absorption on average, and level-ups (11 of them) leave the law untouched, so the 3/2 conveyor does not enter the zone's input arithmetic. N = 2^k (k = 6..11) occurs exactly once per k, at j = 2^k − 50 (≡ 14 mod 32), between N = 2^k − 7 (odd) and 2^k + 4. The longest run of equal consecutive N is 2.

5. Hit chains, listed exactly (chains.py). A zone wall is created at absorption j at depth p (the shift jumps a zero block of p digits onto a P, which needs 2^p | N_j). It survives to the next absorption only if the next interval is a small multiple of 2^p. From each of the 11 real creation kinds, N_{j+1..j+4} = a_i·2^p with a_i in 1..4 (256 patterns): - depth 2 (one hit) in 115-120 patterns, depth 3 in 46-50; - depth ≥ 4 (three stacked hits, off the rule table, halts in 13/80 planted runs) in exactly 10 patterns: 1111, 1112, 1113, 1114, 1121, 1211, 1311, 2111, 3111, 4111. That is, three intervals of exactly 2^p among the four after creation.

In the natural range (N ≥ 49, consecutive N differ by at most 18), these patterns mean intervals that repeat and equal a power of 2. Law 4 never produces them. The law also rules out the direct one-hit route: a hit by the very next absorption needs N_{j+1} = 2^p after 2^p | N_j, but N_{j+1} = 2^p only follows the odd 2^p − 7. Every other route needs a wall to survive an interval with N_{j+1} ≤ 4·2^p, so the creation depth p must be about log2 N − 2. In the blank run the creation depth is at most 4 and the next interval is always ≥ 8.25·2^p. Checks: - with natural-size intervals (real N + offset −40..40), 81/81 runs per kind have no hit; - perturbation census (perturb.py): one interval changed by up to ±128, then 12 real ones, gives 558,940 trials with 0 hits; ±16 then 6 real ones gives 71,424 trials with 0 hits; - blank run: 369 zone walls created to 2e10 (432 to 3.18e10), at depths 1 (307), 2 (53) and 4 (9). No zone wall is alive at any absorption (0/2,238; 0/2,623). Hits: 0.

Non-halting argument now. Halting needs a depth-4 unit. Every hit needs a zone wall alive at a shift, and only absorptions create zone walls (absent earlier hits). So it is enough that (A) the interval law holds forever and (B) under it, every zone wall dissolves within the interval after its creation. Both are counter (2-adic) statements, so this is not Mahler-type arithmetic.

Still open. - (A) Derive the interval law from the conveyor top. Why does each successive top wall add exactly one carry per absorption? Where do the period-32 table and the ν2(b+2) tuples come from (zone P feedback into the wire)? Does a new tuple at ν2 ≥ 7 keep the low depth of creations? This is unseen: the first ν2 = 7 block is near j ≈ 4,060, about 1.2e11 steps. A zoneview run toward 1.3e11 was stopped at 3.18e10 for the time budget, and nothing new appeared up to there. - (B) Prove that under the law no zone wall survives an interval (creation depth ≤ 4 so far; this needs the marker (zone P) positions, which the ν2 pattern of N sets). - The nursery period and the interior-wire lemma are still argued and sampled, as before. - Answered decision moved to decisions/2026-10-10-chain_stage.json. New decision.json: law_stage (recommended), proof_md, park.

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

Question: Spend one more targeted stage deriving the absorption-interval law and the no-survivor zone lemma, start proof.md now with both as lemmas to prove, or park? Answer: law_stage (One targeted stage (at most 2 h): derive the interval law and the zone lemma). auto-applied: Claude's recommendation, under Dennis's standing instruction 'do your recommendations and continuously orchestrate' (2026-10-10, while he was away). Override any time.

Funded stage (2026-10-10, law_stage)

Outcome: confidence stays med; neither lemma closed, and the interval law in its stated form is false from ν2 = 7. Not a cryptid: every new irregularity traces to a binary counter in the zone, not to 3/2 arithmetic. No zone wall is alive at any absorption to 1.93e11 (0/4,820), 0 hits. Scripts are in scripts/deepen5/, numbers in scripts/deepen5/results/summary.json.

1. Longer blank replay (to 1.93e11). deepen3/zoneview.py on the C core (stopped for the time budget), then deepen4/nstruct.py: - 1,812/1,812 record intervals reproduced exactly by the unit model, 4,820 absorptions; the zone automaton equals the real zone at 1,812/1,812 record groups. - First ν2 = 7 block (b = 126) seen. New tuple (−4, 4, −1, −5, −5, −1, 0); the ν2 = 6 tuple was (−4, 4, −1, −5, −5, 5, −1). - 8 violations of the period-32 table, all at j = 4065..4072 (block 127, residues 1..8, right after the ν2 = 7 block): g = −1, 2, −4, 2, −4, 2, −4, 1 instead of 0, −3, −2, −4, −6, 3, 1, −1. So at ν2 = 7 the irregular window grew from 7 residues (26..0) to 15 (26..8). Up to ν2 = 6 there were 0 violations. - The prediction N = 2^12 at j = 4046 = 2^12 − 50 (between 4089 = 2^12 − 7 and 4100) held. - Zone walls: 792 created, depths 1 (659), 2 (113), 3 (1), 4 (19); alive at an absorption 0/4,820; hits 0.

2. Where the law comes from (partly derived). - Conveyor top (toptrace.py). When the last wall is absorbed, the next wall's wire is w + L/3 (w = its own wire, L = the absorbed wall's wire when it became last). The conveyor wires grow ×1.5 per level, so w ≈ 2L/3 is the fixed point. In record interval 802 all 5 walls absorbed had L = 724, 723, 725, 724, 724, and N ≈ 3L. That is why consecutive N differ by only a few carries. - Periodic input. Within a level, the number of carries fed at the bottom of the top-K part per record interval is constant for each group type: 729, 810, 1,095, 1,215, 1,644, 1,821, 2,466, 2,733 (K = 3) and 2,043, 3,063, 4,593, 6,888 (K = 6), ×3/2 per level. - The zone holds a counter of the 32-block index (zcount.py). At the start of step j = 32b + r, the zone digits above digit position 6 read exactly b+1 for r = 0..17 (68/68 blocks at each residue; at r = 3 they read b), and b+2 for r = 28..31. The increment happens in r = 18..27. - Low part (lowform.py). The units below digit 6 have exactly one form per residue for r = 1..18 (68/68 blocks). At r = 18 the low part is all zero, so the absorption shift lands in the counter at its lowest 1. The forms then branch by ν2 class (34/17/9/… blocks) for r = 19..0 and merge again at r = 1. This is why the irregular tuples sit at residues 26..0 and are typed by ν2(b+2): ν2(b+2) is the length of the increment's carry chain. - Not derived: the +1-per-absorption trend, the values of the period-32 table, and why the window lengthens at ν2 = 7. These need the conveyor top and the zone treated as one closed system with the periodic input above. Taking N as an external law is not enough.

3. Lemma B under weaker hypotheses (exact zone automaton driven by synthetic N; lawdrive.py, lawdrive_rand.py, hdrive.py, randdrive.py): - Law + each observed tuple for every ν2 ≥ 7, to j = 3e5: 6/6 runs with 0 alive and 0 hits, creation depth ≤ 5. - Law + random tuples (±8): for ν2 ≥ 7, 20/20 runs to j = 1e5; for every ν2, 20/20 runs to j = 2e4; 0 alive, 0 hits in all. - H = table on residues 1..25 plus independent random values on residues 26..0 of every block: ±8, ±16 and ±32 give 300/300 runs to j = 2e4 with 0 alive and 0 hits, creation depth ≤ 7. - Longer random windows break this: with the table only on 9..25 (15 random residues, ±16), 2/100 runs have a zone wall alive at an absorption (0 hits); with the table only on 13..25, 1/100 runs, creation depth up to 11. With no table (±8 on every residue), 2/100 runs alive and creation depth up to 12; randdrive.py ±8 gives a hit in 1/20 runs. - Reading: B is safe for a 7-residue irregular window at every block, but not for a random 15-residue window. The real ν2 = 7 window has 15 residues. So B cannot be proved from a bounded-window hypothesis; it needs the exact N, including how the window grows with ν2. This answers the decision's exit question ("can a tuple lift the creation depth?"): not in the real run (max depth 4), but a longer window could in principle.

Still open. - (A) Derive N from the closed top system: the last frozen level, the growing top wire and the zone, driven by the constant per-interval input. A proof would likely be an induction over 32-blocks, with the zone counter b+1 symbolic and the ν2 class of b+2 as the case split. It must explain the window length per ν2 (7 residues up to ν2 = 6, 15 at ν2 = 7). - (B) Then show no survivors by the same block induction. The real run gives 0/4,820 and the synthetic law runs give 0, but B depends on the exact window values. - The nursery period and the interior-wire lemma are still argued and sampled, not proved. - Answered decision moved to decisions/2026-10-10-law_stage.json. New decision.json: top_system (recommended), proof_md, park.

Decision (2026-10-11)

Question: Spend one more stage deriving the intervals from the closed conveyor-top + zone system and proving the zone lemma by induction over 32-blocks, start proof.md now with both open, or park? Answer: top_system (One stage (at most 2 h): derive N from the closed top system, then the zone lemma by block induction). Dennis: go with recommendations (2026-10-11).

Funded stage (2026-10-10, top_system)

Outcome: confidence stays med, but the gap is much narrower. N is no longer an external law: the conveyor top and the zone close into one autonomous zone automaton with a single period-8 constant. Its block map takes the canonical state for b to the one for b+1 (or b+2, b+3, … for deep ruler classes) with a closed-form delay, and no zone wall is alive at any absorption in any test. Not a cryptid. The stop rule does not fire: the window does grow with ν2, linearly, but it has a closed form. Scripts are in scripts/deepen6/, numbers in scripts/deepen6/results/summary.json.

1. Top relation (new rule, exact). Let A_j be the P units that leave the zone bottom during step j (the N_j carries), and D_j the P units that left before step j. Then

N_j = 3*A_j + D_j + p(j mod 8),   p = (47, 48, 48, 47, 48, 47, 48, 47)  for j mod 8 = 0..7

2. Closed system (topsys.py). State = (zone, D, j mod 8). Step j: feed D_j + p(j mod 8) carries, add 3 for every P that drops, then the absorption shift. - Reproduces the blank run's N for 4,819/4,819 steps (792 zone walls, 0 alive, 0 hits). - Run to j = 4.2e6 (131,250 blocks, ν2(b+2) up to 17, 49 s): 690,078 zone walls created, 0 alive at an absorption, 0 hits, zone ≤ 27 units, D − j always in [−5, −1]. - Canonical block state (canon.py): at j = 32b + 17 the zone is S1 0 1 1 1 1 followed by the binary digits of b+1 (LSB first), with D = j − 1. This holds at 131,250/131,250 blocks (b = 0..131,249).

3. Block map and window per ν2. - symb.py starts from the canonical state C(b) for random b (up to 2^120 and 2^400) with ν2(b+2) = k and runs whole blocks: - k = 0..40, 20 b each (820 runs): C(b) → C(b+1) for every k ≤ 22. For k = 23..40, C(b+1) is skipped and C(b+2) is reached. Within one class (k ≥ 2) the g sequence is the same for every b. - k = 0..260, 2 b each (522 runs): the next canonical state comes after exactly 1 + ⌊(k+9)/32⌋ blocks (thresholds k = 23, 55, 87, …, 247). - All 1,342 runs: 0 alive, 0 hits. - Mechanism. At r = 18 the low part is all zero, and the absorption shift lands on the counter's lowest 1, at height 6 + ν2(b+2). That unit becomes a P marker. Carries pass through it, and it sinks about one unit per step (one drop per step). The irregular g window ends when the marker leaves the bottom. - Window in the 4.2e6 run (irregular offsets from 32b): - k = 0: 26; k = 1: 27–28; k = 2, 3, 4, 6: 27–32; k = 5: 27–30. - k = 7..14: 27–40; k = 15..17: 27–48. - tuple(k+8) = tuple(k) shifted by 8 offsets after a common prefix (k = 6..9 against 14..17). - So the window grows linearly with ν2. That is why the period-32 table broke at ν2 = 7, and why a bounded random window (law stage) was the wrong hypothesis.

Non-halting argument now. Halting needs a depth-4 unit, which needs a hit, which needs a zone wall alive at an absorption. Given (1), the right end is the closed system in (2). By induction over blocks, C(b) leads to C(b + 1 + ⌊(ν2(b+2)+9)/32⌋), the steps between have no zone wall alive at an absorption, and the classes of the blocks it skips are the small ruler values ν2(t), t < 2^k. That covers every b, given a uniform version of item 3.

Still open. - (A) Write the top relation as a proved lemma (conservation sketch above). The constant p needs the nursery period. - (B) The block map for all k needs a marker-descent lemma uniform in the marker height: a P marker at height h above canonical low forms sinks one unit per drop, and nothing below it changes until it reaches the low part. It is checked for k ≤ 260 with random high bits, and exhaustively for b ≤ 131,249, but not proved. - The nursery period and the interior-wire lemma are still argued and sampled, as before. - Answered decision moved to decisions/2026-10-10-top_system.json. New decision.json: marker_stage (recommended), proof_md, park.

Decision (2026-10-12)

Question: Spend one more stage proving a marker-descent lemma uniform in the marker height (the block map for every ruler class), start proof.md now with it open, or park? Answer: marker_stage (One stage (at most 2 h): the marker-descent lemma, then proof.md). Dennis: apply recommendations (2026-10-12).

Funded stage (2026-10-10, marker_stage)

Outcome: confidence stays med, with a much smaller gap. The marker-descent lemma is now proved symbolically, uniformly in the marker height. The block map is proved for every ruler class k = ν2(b+2) < 32,759 (o ≥ 3). The stop rule does not fire, because the computation below the marker does not depend on the height h. It does depend on the time since planting, through a number w ≈ off, but in an affine way. There is one new structural item: the end of a deep descent can plant a second, nested marker of height ν2(k+9)+1. Not a cryptid. Scripts are in scripts/deepen7/, numbers in scripts/deepen7/results/summary.json. (deepen7's run-length printer had a bug in its first version, fixed before any result below.)

1. Descent lemma (symbolic, symdesc.py + rundesc.py). Let b = o·2^k − 2 with o = 2q+1 and k = ν2(b+2), let j = 32b + off, and write off = 8m + φ with off ≥ 32. Then the zone is F_φ: - heads_φ at fixed digit positions inside a low word of L = k + λ_φ − off digits, whose value is 2^(L−1) + w_φ(off); - then the marker P; - then 0 1^(off−20) 0 bin(q); - and D = j + d_φ.

phi  heads        lam  w          d        phi  heads        lam  w          d
0    S1@0         24   off-20    -2        4    S1@0 PP@0    24   off-24    -4
1    S1@0         24   off-20    -2        5    S1@2         24   off-21    -2
2    S1@1         24   off-20    -2        6    S1@1 P@1     24   off-24    -3
3    SP@1         25   2off-42   -3        7    S1@0 PP@0    24   off-24    -4

2. Value form (marker transparent). P passes carries unchanged, and a shift lands on the marker only if every digit below it is 0. So the marker is invisible to the digit arithmetic: - Vtot (all digits, with P weightless) = o·2^(k+5) + w_φ(off) − 3·2^(L−1). Phase 3 instead has o·2^(k+6) + 2off − 42 − 3·2^(L−1). - Every decision in a step (head rules, shift landing at bit ≤ 2, drops) reads only the low bits, so this should stay exact after the growth condition fails. This part is argued, not run through the engine. - vtot.py: 300 random (k, o) pairs, 60,509 states from off 32 down to L = 2. It is exact at every L ≥ 3 (60,203/60,203), and at L = 2 for 254/306.

3. Endgame by locality (endgame.py, egread.py, egcheck.py). - Method. Start from the value-form state at L = 4, compress o·2^(k+5) to o·2^G, and run to the next canonical state. If no shift lands at or above digit R, the run depends on k only through k mod 2^R. - k = 65,536..131,071 (all residues mod 2^16): 65,536/65,536 reach C(b + 1 + ⌊(k+9)/32⌋), with 0 alive and 0 hits. Mod 2^12: 8,192/8,192 (o = 3, 5). - Compressed runs match the real run from C(b) in 150/150 random cases: same g sequence, same delay. - Nested marker. The landing digit is ≤ 8, or exactly ν2(k+9) + 1 (65,536/65,536). When k+9 has a high power of 2, the low word wraps as the marker reaches the bottom, and the shift plants a second marker at height ν2(k+9)+1. It sinks over a 1-run (egtrace.py 1015 3 4 40), in a different form from F_φ. Residues with ν2(k+9) ≥ 15 (2 of 65,536) are not covered.

4. Small classes (smallk.py). For k = 0..40, every odd o mod 2^8 was run (2 high-bit variants each). 10,495/10,495 reach C(b + 1 + ⌊(k+9)/32⌋) with 0 alive and 0 hits. The highest landing digit is k+6 (the plant), which is below the locality bound k+13. So the block map holds for every b with ν2(b+2) ≤ 40. For o = 1 (b+2 = 2^k), k = 1..259: the delay formula holds 259/259, with 0 alive and 0 hits.

Coverage. Items 1-4 together give C(b) → C(b + 1 + ⌊(k+9)/32⌋) with no zone wall alive at an absorption and no hit, for every b with k = ν2(b+2) < 32,759 and o ≥ 3. The proof uses the symbolic descent, finite checks and locality. The first class not covered is k = 32,759 (k+9 = 2^15).

Top relation as a conservation lemma (written, not derived). Lemma T: N_j = 3A_j + D_j + p(j mod 8). The argument has three parts: - (i) The last wall j does wire_j + A_j + 1 rounds, and each round sends 3 carries up. - (ii) Carries only move up, so the walls below never see the zone. The quantity 3·wire_j + (in-flight carries) + (carries wall j has emitted) is fixed by the zone-bottom position, and one extra round of wall j−1 costs wall j 2 carries. That gives slope 1 in D. - (iii) The rest depends only on the birth data of walls j−1 and j, which repeat with the 8-wall nursery cycle.

This stage spent its time on the marker, so T is still checked (4,819 steps plus 4,200 random zones in deepen6) but not proved.

Still open. - (B′) Nested-marker lemma. A descent lemma for the second marker (height ν2(k+9)+1, over a 1-run), uniform in its height. Its own end may plant a third marker at about ν2(ν2(k+9)+c), which would make it a ruler of rulers. Without it the block map is proved only for k < 32,759. - The o = 1 entry step, symbolically. - The symbolic engine and the locality argument are written against fastzone.py semantics; nothing is machine-checked. - Lemma T, the nursery period and the interior-wire lemma. - No proof.md: none of these give high confidence. - The answered decision is moved to decisions/2026-10-10-marker_stage.json. The new decision.json has the options nested_stage (recommended), proof_md and park.

Decision (2026-10-12)

Question: Spend one more stage on the nested-marker lemma (and the o = 1 entry), start proof.md now with it open, or park? Answer: nested_stage (One stage (at most 2 h): the nested-marker lemma, then proof.md). Dennis: b (fund all five), 2026-10-12.

Funded stage (2026-10-10, nested_stage)

Outcome: confidence high. The nested marker is the marker-descent lemma one level down, not a new form. The stop rule does not fire: the third marker that a deep enough nested marker plants has the same form again, so the recursion closes by induction on the class. The entry steps are now symbolic for every o, o = 1 included. With this, the block map is covered for every b. The pieces still to be written up as proofs are the ones on the conveyor side: Lemma T, the nursery period and the interior-wire lemma. Not a cryptid. Next: proof.md. Scripts are in scripts/deepen8/, numbers in scripts/deepen8/results/summary.json.

Notation: k + 9 = s·2^v with s odd and v = ν2(k+9); off' = off − (k+9); S = s + U·2^(k+5−v) (odd), Q = (S−1)/2. U is the part above the counter (U = o at level 1).

1. Plant lemma (symbolic in v and Q, symplant.py). The level-1 endgame starts at off' = 12, in phase 4, with marker height 3. There the zone is S1 PP 000 P [1 0 1^(v−5)] X with X = S − 1 = 2Q from digit v up, and D = j − 4. A new engine runs 5 closed-system steps with v and Q symbolic. It allows words of symbolic length v + c with value A·2^(len−1) + x, a high part a·Q + b, and the feed's S·2^v packet, which must arrive exactly at digit v. It reaches exactly

off' = 17:  S1 . LOW2 . P . above,   LOW2 = v−3 digits of value 2^(v−4) − 3,   above = 16Q + 6 = 0 1 1 0 bin(Q),   D = j − 2

2. The nested marker is the level-1 descent of class K' = v − 10 (exact identification). Take the state at off' = 17 and set U' = 32S. It is deepen7's F_1 for class K' and upper part U': - Vtot = U'·2^(K'+5) + w_φ(off') − 3·2^(L2−1), with L2 = K' + 24 − off'; - j = U'·2^(K'+5) − 64 + off', and D = j + d_φ.

So the nested marker sinks by the same 8 symbolic phase steps: - They never use the parity of the upper part or a lower bound on m (deepen7's nonneg is never called). So they hold from off' = 17 (m = 2). - Their growth conditions, read with K = v − 10, hold until L2 ≤ log2(v) + 2.97 (nestgrowth.py; L2 at the first failure is between 4 and 21 for v ≤ 10^6). - After that, the value form takes over, as at level 1.

Checks: - nested.py vform: 400 random (v in 12..300): 60,572/60,572 states from off' = 17 down to L2 = 3 equal the class-K' value form with U' = 32S. 40 more with v in 300..1500: 30,993/30,993. - nested.py ident: 400/400 runs (v in 14..400), plus 40/40 with v in 400..1500, go from L2 = 4 to the next canonical state with the same g sequence and end offset as deepen7's level-1 compressed endgame of class K' (o = 3).

3. Recursion and coverage for every class. - Let PlantRun(v, S) be the run from the off' = 12 state. - Every shift in it lands at digit ≤ v + 1. The plant is the only landing that high, and bit v+1 is fixed symbolically. So the run depends only on S mod 4. - nested.py range 600 2: every v in 10..600, s mod 4 ∈ {1, 3}, o ∈ {3, 5}. 2,364/2,364 runs reach the next canonical state, with 0 alive, 0 hits and max landing v + 1. - For v > 600, items 1-2 reduce PlantRun(v, S) to the class-K' endgame with K' = v − 10 > 590. - That endgame lands only at digits ≤ max(8, ν2(K'+9) + 1) < K' + 5, so it does not see U'. It is therefore deepen7's residue run (egread R16) when ν2(K'+9) ≤ 14. - When ν2(K'+9) ≥ 15, it is PlantRun(ν2(K'+9), ·) again: its start state is the same value form at marker height 3, phase 4. - The class shrinks from K to ν2(K+9) − 10 < K, so induction on the class terminates. The level-1 classes are covered the same way: k ≤ 40 by smallk, ν2(k+9) ≤ 14 by egread, otherwise PlantRun(ν2(k+9), S). - Direct checks of the recursion (deep.py): v = 1025, 1537, 2049, 4097, 8193, 16385, 3 (s, o) each. - Every run reaches the canonical state with 0 alive and 0 hits. - Landings above digit 8 occur only at v + 1 (off' 13) and at ν2(v−1) + 1 (off' = v + 12, the third marker, the same plant one level further down). - Real uncompressed runs from C(b) (realdeep.py): - k = 1015 (o = 3): canonical after 33 blocks. - k = 32,759, the first class deepen7 did not cover, for o = 3 and o = 1: the next canonical state at off 32,817 (delay 1,025), 0 walls alive, 0 hits (859 s and 866 s). Landings above digit 8 occur only at k + 6 (marker 1, off 17) and at 16 = v + 1 (the nested marker, off' 13).

4. Delay correction (not needed for non-halting). - deepen6/7's delay 1 + ⌊(k+9)/32⌋ holds only while ν2(k+9) < 33. Each nested level adds its own term: delay = 1 + ⌊(k+9)/32⌋ + ⌊(v−1)/32⌋ + ⌊(e−1)/32⌋ + …, with v = ν2(k+9) ≥ 10, e = ν2(v−1) ≥ 10, and so on. - It matches in 2,364/2,364 range runs and in all deep runs (v = 1025: +32 blocks; v = 16385: +512). - The induction only needs some later canonical state, so this changes nothing in the argument.

5. Entry steps, symbolic for every o (symentry1.py, symentryq.py). - Why the hand steps needed q ≥ 1: with q = 0 the part above the marker would be −1 at off 19, so the machine keeps the marker as S1 (one pending carry). - The symbolic engine (S = 1, v = k + 5) runs C(2^k − 2) = S1 0 1^(k+4) → 0^(k+6) S1 → S1 0^(k+4) 1 S1 → 0 S1 0^(k+2) 1 P. The last state is exactly E(20) with q = 0, D = j − 2, and the run has 0 walls alive and 0 hits. It holds for every k ≥ 3 (growth checked at V0 = 8). - From E(20) on, deepen7's entry and phase steps apply unchanged. - entry1check.py: 598/598 k in 3..600 match the machine at all 4 states. - entry1forms.py: 45,290/45,290 states (k = 30..300, o = 1) equal E(20..31) and then the value form down to L = 3. - The same engine now also does deepen7's two hand-checked q ≥ 1 steps, with k and q symbolic (symentryq.py): S1 0 1^(k+4) 0 bin(q) → 0^(k+6) S1 bin(q) → E(19) → E(20). It has 0 walls alive and 0 hits for every k ≥ 3. entryqcheck.py: 2,000/2,000 random (k ≤ 500, q < 2^60) match the machine at all 4 states. So the entry is symbolic for every o.

Non-halting argument now. - Halting needs a depth-4 unit, which needs a hit, which needs a zone wall alive at an absorption. - Given Lemma T, the right end is the closed zone system (deepen6). - For every b, C(b) leads to a later canonical state C(b′), with no zone wall alive at any absorption in between. The cases: - the symbolic entry (every o, item 5); - the symbolic descent; - the value form; - the endgame by locality: small classes, the 2^16 residues, and the nested recursion by induction on the class (items 1-3). - Base: the closed system started from the blank run's zone is canonical at every block b = 0..131,249 (deepen6 canon.py).

Still open (proof.md work, not new mechanism). - Lemma T, the top relation. Checked on 4,819 blank steps and 4,200 random zones; the conservation argument is still a sketch. - The nursery period and the interior-wire lemma (argued and sampled, as before). - The value form below the growth range and the locality principle are argued, and checked by 60,203 + 91,565 states and by the residue and range runs. - The symbolic engines run against the fastzone semantics, which were checked against the machine. - Nothing is machine-checked in Rocq yet. proof.md is not written; it is the next stage. - The answered decision is moved to decisions/2026-10-10-nested_stage.json. No new decision.json: confidence is high, and per CLAUDE.md work goes on to proof.md without blocking.

Informal proof stage (2026-10-12)

Outcome: proof.md written; status OPEN. Not a complete proof: three conveyor lemmas are stated exactly and checked but not proved. Not a cryptid. check_proof.py quick (30 s) and full (2.5 min) both pass.

Proved in this stage. - Unit lemmas by oracle simulation: run the machine on one unit's cells only, with the rest of the word replaced by the induction hypothesis (head steps onto the rest only in B, comes back in C). This is a finite computation for each unit, so it is a proof. Exact chains and step constants: D1 4+4, P 5+5, W 6/11/11/6 (κ 34), 111 κ 25, 101 κ 14, 1111 κ 27, 1101 κ 16, first-cell-0 rule 1 step. Depth-4 heads 11111 and 11101 fail it (state E walks onto the rest). - Theorem U (machine arrival = inc on unit words, cells and exact step counts) by strong induction; checked on 38,415 exhaustive words (up to 4 units of 14 kinds) + 20,000 random, 0 mismatches. - Initial segment: blank to the X record at 203,465 (zone D0 D0 D1 D1 D1 D1, the closed system's start).

Corrected. The interior-wire statement must exclude the first unit of the unit word: Y records start with W W inside the nursery (195 of 523 records to 3e8). With that exclusion, 0 violations in 1,022 records to 2e9.

Found. No static cell boundary separates the nursery from the conveyor: at every cell within 120 of the left edge, the head crosses in E/F/A rightward and D/E leftward within one cycle (walls pass through every cell). So Lemma N cannot be closed as a finite oracle computation like the unit lemmas; it needs a symbolic conveyor model.

Still open (next stage). - Lemma N (nursery 8-record cycle), Lemma I (interior wires), Lemma T (N_j = 3A_j + D_j + p(j mod 8)): proofs. A likely route is a symbolic conveyor state (wall states and wire lengths) driven by the left gadget, with T as a conservation identity. - The symbolic zone engines are executable models, checked against the machine but not machine-checked; the locality principle and the value-form continuation are argued.

Skeptic round 1 revision (2026-10-12)

Outcome: status OPEN. The two fatal gaps (Lemmas N and T) are now proved, and the invariant is restated. The only major gap left is the zone layer (§6, Theorem B), which is still executable-model computation plus argued locality and value form. Not a cryptid. New code: scripts/proof2/lemma_nt.py; check_proof S5/S6 rewritten. quick and full both pass.

Lemma N by a moving-boundary window. Run the head cell and the gadget explicitly, with the rest R opaque. The W unit lemma holds for any left context. So when the window's last six cells read 111000 and B enters them, apply it: R gets 3 arrivals, then the shift pops R's first unit, which is P by Lemma C1 (inc^3 of a P/S1/SP/W-led word starts with P), into the window. With only this rule, all 8 record types succeed and close the cycle: - XE: 3 W-rule uses, F = W W P SP; - YE: 12 uses, F = W P W P P SP P P P P SP; - ZE: 2 uses, F = P SP; - the C/D records are single steps.

The earlier "no static boundary" finding is explained: a W straddling a static boundary touches R in state E. Machine cross-check: next record = G' F (pop o inc^3)^k (U), cells, state and exact steps, at 1,021/1,021 transitions to 2e9.

Index frame. In U_0's index frame, F lands at fixed indices every cycle. So the 8 births per cycle have fixed (index, state): (2,SP) (0,W) (-1,W) from XE; (10,SP) (5,SP) (2,W) (0,W) from YE; (1,SP) from ZE. The net units per cycle are 0. U grows at the zone top, which slides up about one index per absorption.

Lemma T = flux identity. A wall sits at b + floor((R+s)/2). Wall j-1 receives H_(j-1) carries before wall j's birth and then only wall j's emissions. Absorption j-1 is its (z - b_(j-1))-th firing. This gives

N_j = 3A_j + D_j + [z0 - 3b_j + 2b_(j-1) + s_(j-1) + H_(j-1)]

with z0 = 43 and H = 0 / 36 / 6 / 9 (same record / after XE / after YE / after ZE). The bracket reproduces p = (47,48,48,47,48,47,48,47) exactly, including j = 1..6 with U_0's walls.

FIFO means wall j is the j-th born, through every level-up. S6 checks this (1,192 absorptions, conveyor walls 6 -> 14). Round-1 review's objection, that a level-up shifts the birth index against j, mixes up the pairing with the time slot inside a cycle.

Unit-level run. The right part driven by the proved cycle from U_0 equals the machine at every S5 record. Its zone after absorption 0 is Z_1, and the closed system from Z_1 gives the same N_j. The stored machine replay agrees on the overlap.

Still open. Theorem B (zone layer): machine-check the symbolic engines (Rocq: lia/nia on 2^k), prove locality and the value form as closed-system lemmas, and make the class recursion a well-founded induction.

Skeptic round 2 revision (2026-10-12)

Outcome: status OPEN. One major gap is fixed (the invariant) and one is narrowed to two named lemmas. All four minor gaps are fixed. Not a cryptid. New code is in scripts/proof3/ (invariant.py, locality.py, results/), and check_proof S3/S6/S10/S10s are updated.

Invariant (major): fixed. Inv(n, J) now pins the configuration. The gadget row, base(n mod 8), born(n), the birth tables, the carry chain (R_youngest = 0, R_(w−1) = H + 3⌊(R_w+s_w)/2⌋), the zone feed m from the top wall's emissions, zone = inc^m(CS_J), z = 43 + D_J + drops, and an all-P conveyor determine U_n from (n, J). - S6 rebuilds U_n from (n, J) at every record of the unit-level run: 481 (quick) / 1,201 (full) records, 0 mismatches. - It rejects all 483 perturbations (one P less, one P more, top wall moved up) for every J′ in J±4. - Closure is Lemma N plus the Lemma T algebra. The absorption comes at the closed system's least fixed point, because earlier triple boundaries have m ≤ c + 3A − 3.

Lemma L (locality): new, proved. It compares two closed-system runs with feeds differing by Δ ≡ 0 mod 2^R. - Proof: upward flow; after T0 carries the low part is clean, so it is a counter; value bookkeeping H_(t+1) = (H_t/2^a + Δ)/2^b, with the cut following ν2(κ). - Representative runs check (H0)-(H2) and κ = 1 at the end. - Endgame: 65,534/65,534 residues mod 2^16 (1 min; the 2 with ν2(k+9) ≥ 15 go nested). - Nested range: v ≤ 600, both s mod 4: 1,182/1,182 (1.5 min). - Small classes: k ≤ 40, o mod 16: 328/328 representatives + 327/327 direct runs. - This proves the endgame, the compression, the S-mod-4 claim and the small classes, given VF. - Found: a fixed cut fails, because every endgame step loses one digit, so the cut must follow ν2(κ). The o = 1 block b = 2^k − 2 is not in its class: its k+6 marker gets no carry, so it is run directly.

Class recursion. E(K): VF_4(K, U) reaches a canonical state for every U. It is proved by strong induction on K, with base ν2(K+9) ≤ 600 (no hypothesis used); v > 600 uses the plant lemma, VF for K′ = v − 10 < K, and E(K′).

Minor gaps fixed. - U-term: now an induction on the wall count (S3 checks walls(inc w) ≤ walls(w)). - FIFO placement table: 17 / 3 / 5 / 5 against ≤ 10 / 1 / ≤ 2 / ≤ 2 (S6 checks every birth). - Absorption definition: a top-wall firing with no move up. - §6.7 split.

Still open (major, the only one). Two lemmas of the zone layer: - VF: the value form from C(b) down to marker height 3, at level 1 and from the plant's off′ = 17 state. Today it rests on the entry/descent engines, whose growth conditions are recorded but not discharged, plus a prose argument checked on about 150,000 states. - Plant for v > 600: a symbolic engine, not machine-checked.

Proposed route. Extend Lemma L so that Y may contain the marker P and members may have different L. Each descent step then follows from finitely many one-step representatives: the landings are at digit ≤ 2, and the bookkeeping (H + Δ)/2 matches the next form because w has slope 1. The 3 entry steps and the 5 plant steps would be checked by hand on their closed forms.

Decision (2026-10-12)

Question: #14's proof is down to one major gap (lemma VF and the plant step for v > 600): fund one more revision round to close it, or park #14? Answer: vf_round (Close lemma VF, about 2 h). Dennis 2026-10-12: "go with recommendations".

Funded stage (2026-10-10, vf_round)

Outcome: both open zone lemmas are closed, and confidence stays high. No new engine was needed, so the stop rule did not fire. - proof.md §6.1-§6.3, §6.5, §6.7, §7, §9 and §10 are updated, with a review-log entry. - New code is scripts/proof4/vf.py, with results in scripts/proof4/results/. - New check section S11 in check_proof.py. Quick and full both pass (numbers below). - Not a cryptid. Next: skeptic round 3 on proof.md, then the Rocq formalization.

1. Lemma L′ (one-step locality with the marker above the cut). This is Lemma L for one step, with one change: Y and Y′ may each hold one P unit, at different digit positions. - Why the P is harmless: - it passes carries and has no weight; - (H1) keeps every landing in X; - it never reaches the bottom while X keeps a digit unit (checked: r_end ≥ 1); - X's landings move it down a + b digit positions. - Result: a member's next zone is X_next · Y′_next, with value V0_next + (H/2^a + Δ)/2^b.

2. Lemma VF by one-step representatives (cut R = 8, T0 = 2^12). The value form VF(k, Ω, off) is the binary word of Vtot = μΩ + w(off) − 3·2^(L−1), with the heads and the marker at their places, j = Ω − 64 + off and D = j + d. - It uses the entry table for off 20..31 at level 1 and the phase table otherwise. μ = 2 for the λ = 25 forms. - Each step VF(off) → VF(off+1) needs L(off) ≥ 5, which holds before off_end. It is one of: - (E) off 20..31: 24 representatives (k0 = 41, o0 = 1 and 3); - (A) L ≥ 9: one representative per off mod 256 (L0 = 11), 256 in all; - (B) 5 ≤ L ≤ 8: one per (L, off mod 256), 1,024 in all. - All 1,304/1,304 representatives satisfy (H0′)-(H2) and give exactly the next form, with 0 alive walls and 0 hits. Max landing digit 3; X keeps ≥ 6 digits. - The member conditions are Ω ≡ 0 (mod 2^8) and the same off mod 2^8, with L ≥ 9 for both, or the same L. Then H and Δ are 0 mod 2^8. - The next value follows from two identities per representative, both checked: - (μ/2^a + 1)/2^b = μ′ and (wa/2^a + 1)/2^b = wa′; - L′ − L = −(a + b). - (a, b) is (0, 1) for every step except (0, 0) at phase 2 and off 20, 24, and (1, 1) at phase 3 and off 21, 25. - Members at level 2 have the upper part Ω = S·2^v = 32S·2^(K′+5), so their "o" is the even number 32S. That is fine: only Ω mod 2^8 enters. - This removes the growth conditions entirely. The value form is the definition, and no claim about the size of the low word is used. - R = 6 also works (24 + 64 + 128 representatives). Negative controls: R = 3 gives landings in Y, and a wrong w at phase 5 is rejected by 320 representatives.

3. Lemma E (entry, by hand). The forms at off 17..20: - off 17: C(b) = S1 D0 D1^(k+4) D0 bin(q) - off 18: D0^(k+6) S1 bin(q) - off 19: S1 D0^(k+4) D1 P D1 bin(q−1) (q ≥ 1), or S1 D0^(k+4) D1 S1 (q = 0) - off 20: D0 S1 D0^(k+2) D1 P D0 D0 bin(q), which is VF(k, o·2^(k+5), 20)

The feeds are o·2^(k+5), o·2^(k+5) + 1 and o·2^(k+5). Each step is one S1 event and binary addition. Checked on 2,000/2,000 random (k ≤ 1,500, o up to 400 bits, 405 with o = 1).

4. Lemma P (plant, by hand, every v ≥ 9, Q ≥ 1). With n = v − 3, the six forms at off′ 12..17 are written out in proof.md §6.5. The key event comes at 13 → 14: - the marker-turned-SP fires; - its 3 carries wrap [2^n − 3]_n to zero; - its shift lands on bit 1 of 4Q + 2, at digit v + 1, which becomes the new marker.

The off′ = 17 state is VF(v − 10, S·2^v, 17) at level 2 (identification by algebra). Checked on 3,000/3,000 random (v ≤ 2,998, S up to 600 bits), with all six forms and the identification.

5. Chains and members (S11, beyond the proof). - Real runs from C(b), random k in 41..400 and random o: entry forms and then VF at every offset to off_end, 300/300 runs, 68,308 states. - From the plant start, v in 12..400: plant forms and then level-2 VF to off_end, 300/300 runs, 62,723 states. - Random members (k ≤ 3,000, o up to 300 bits, both levels), one real step: 2,969/2,969.

6. check_proof.py. - New S11: the representatives, entry, plant, chains and members. - quick: ALL PASS (S11 in 5 s). - full: ALL PASS (7.6 min; S11 42 s). - S9 (the old symbolic engines) still runs, as a cross-check only.

7. Figure. img/lprime_step_R8_off33.png (scripts/proof4/fig_lprime.py; a folded card figure, observe.json diagram 7) shows one representative step at phase 1 and two of its members, with marker heights 11, 35 and 60. Left of the cut the before-rows match across all three, and so do the after-rows.

Still open. - Skeptic round 3 on the revised §6. - The Rocq formalization (§10). VF becomes Lemma L′ plus vm_compute of 1,304 one-step representatives; E and P are 8 closed-form steps for lia/nia. - Nothing in the informal argument is open.

Informal proof stage, round-3 self-review (2026-10-12)

Outcome: proof.md revised into a complete informal proof; status OPEN (stage informal_proof), confidence high. One real gap found and closed (below); nothing in the informal argument is open. Not a cryptid. New code: scripts/proof5/z1.py; check_proof.py gets S12, an S7 landing check and an S4 transition-table check.

Added. A Machine section with the transition table (A1 marked as the halting transition) and a Rule table (summary) comment block listing every rule the proof uses (sweeps, unit lemmas, Theorem U, the 8 window runs, C1/C2, Lemma T, the zone lemmas) with parameters, domains and proof method. S4 checks that the printed table equals the holdout string and that A1 is the only undefined entry.

Gap found: absorption shift on an S1. - §1 counts a shift landing on S1 as a hit, but the old Lemma Z0 argued only about wall shifts. - The zone model's hit counter (deepen4 fastzone) counts landings on SP, W and stacked heads, not on S1. An S1 landing would have surfaced only later, as an alive 00 head, an undefined step or a wrong next form. So the "0 hits" of S7 did not by itself exclude it. - Fixed by Lemma Z1 (structural): after a carry phase with feed c ≥ 1, the first non-D0 unit is never an S1. Take the last event among step start, a drop, or the S1's creation. After it, the units below the S1 are a pure counter that ends at 0 without carrying out, so it received no carries. But a step start gives c ≥ 1 carries, a drop gives ≥ 3, and the creation leaves the emitter's P below, which must drop later. - Lemma Z0 is restated for defined runs, with "alive" covering every head outside {ε, 0, 1}. - Checks (S12): every shift of the orbit from Z_1 to j = 32·131,250 classified by kind and target. Only D1 and P occur: absorption shifts 3,509,921 on D1 and 690,078 on P, wall shifts 690,078 on D1 and 480,973 on P. Lemma Z1 holds on every zone of ≤ 6 units over D0/D1/S1/P/SP/W with every feed 1..40 (1,866,200 phases) and on 200,000 random zones. The c = 0 negative control finds S1, as it should. In the blank-run orbit every zone wall born at an absorption dissolves on a D1 in the next step (wall→D1 count = abs→P count).

Smaller corrections. - Lemma VF level 2 was stated for v ≥ 9, but Lemma VS needs the feed c ≥ T0 = 2^12, which fails for v ≤ 10 with small S. It is now stated for v ≥ 12; the recursion only uses v > 600. - Lemma VS step 4: after a step with a + b landings the X-part is the digits below 8 − a − b, and the member/representative values differ by a multiple of 2^(8−a−b) (not 2^8). The conclusion is unchanged. - "Halting unreachable" now lists the initial segment too.

Re-derived by hand, no change. Lemma T's bracket for all 8 birth phases and for the U_0 walls j = 1..6 (gives p exactly); Lemma E's feeds; Lemma P step 13 → 14 digit by digit; the off′ = 17 identification value; Lemma L instances (members, Δ, cuts, T0); invariant clauses.

Still open (not informal-proof work). Dennis's Checkpoint B read of proof.md. The Rocq formalization (proof.md §10) is large: zone layer with Lemma L/L′ as two-run statements and about 68,000 vm_compute representative runs.

Rocq plan: a smaller split (proof.md §10). With Lemmas P and VF (level 2) proved for every v ≥ 12, the class recursion can use the induction hypothesis from v > 50 (K′ = v − 10 ≥ 41). Then the endgame needs only the cut R = 12 (4,094 residue runs; locality.py endgame 12 52 15, 4,094/4,094, now in S10) and the nested range 11 ≤ v ≤ 50 (80 runs). That is 4,829 representative runs instead of 67,371. The written proof keeps the larger split.

check_proof.py. quick ALL PASS (46 s); full ALL PASS (8.6 min, 70 checks, 0 failures). Scratch files now go to a per-run temp dir instead of fixed /tmp/cp_* names, so concurrent check runs cannot clash.

Skeptic round 1 on the complete proof (2026-10-13)

Outcome: the skeptic found proof.md sound, with 5 minor gaps (no fatal, no major). All 5 are fixed and re-checked; status CHECKPOINT_B (stage informal_proof), confidence high. Not a cryptid.

1. Absorption at the least fixed point (§5, §7). The missing step was "no fixed point lies between triple boundaries". - Let r ∈ {0,1,2} be the carries of wall j's triple still to come at absorption j−1. Lemma T's items give c = 3(z0 + D_j − b_j − f) + r, so c ≡ r (mod 3). - Triple boundaries of interval j are exactly m ≥ r, m ≡ r (mod 3). A fixed point m = c + 3A(m) has m ≡ c ≡ r and m ≥ c ≥ 47 > r. - New S6 check (f): r_j read off the unit-level run (wall j's received carries at absorptions j−1 and j). r_j ∈ {0,1,2}, c_j ≡ r_j (mod 3), wall j fires z_j − b_j times: 1,191/1,191 absorptions (full), r = 0/1/2 occur 397/393/401 times.

2. Strict (H0), (H1), (H0′). Now "at most r − 1 digit units below" for non-digit units and for every landing target. vf.py already tested this. locality.py now flags any landing target (digit or not) with more than r − 1 digit units below it. All Lemma L runs redone: endgame R = 16 65,534/65,534, R = 12 4,094/4,094, nested v ≤ 600 1,182/1,182, small classes 328 + 327. Stored artifacts in scripts/proof3/results and scripts/proof5/results regenerated.

3. Normal form. Unit words without trailing D0 (D0 0^inf = 0^inf); bin(0) empty; q = 0 forms spelled out. z1.py orbit checks no zone ends in D0: 0 cases to j = 4.2e6.

4. Head order. §6.2 legend: X@p has p digit units below; heads at one position listed bottom to top; marker never shares a position with a head.

5. Theorem B. The b′ formula is dropped; only b′ > b (canonical state at a later j). The formula stays as an unproved observation for k ≤ 130 (S8).

check_proof.py. quick ALL PASS (42 s, 70 checks); full ALL PASS (8.2 min, 71 checks).

Next. Dennis's Checkpoint B read (non-blocking), then the Rocq formalization (proof.md §10, smaller split).

Kill