1RB---_1LC1RE_1LD0LC_1LE1LC_1RF0RE_1RA0RB never halts

The tape of this machine is a binary counter that is fed at its left end. Every time the head reaches the left edge in state C, it walks right as B, and that walk is one carry. The carry runs through a word of short blocks called units until a unit absorbs it. Then C walks back to the left edge.

Most units are passive, but one kind, the wall, is a rotor. A wall absorbs every second carry it receives. On the other carries it sends three carries further right and then moves one unit to the right. So each wall forwards 3/2 as many carries as it receives.

The left end (the nursery, a short gadget word) is exactly periodic. Once per period it puts 8 new walls into the unit word, and it touches the unit word only by acting as a wall itself. The walls ride a conveyor of P blocks, in order. At the right end they are absorbed one by one into a zone, a binary counter with a few marker units.

When a wall fires, it leaves one extra 0 cell above it, its shift. The machine can halt only if a shift lands directly on another wall-like unit. The proof shows that this never happens:

• in the conveyor, because three carries always turn the unit above a firing wall into P (Lemmas C1, C2);
• in the zone, because the zone input is a fixed closed system (Lemma T), and that system never keeps a zone wall alive across an absorption (Theorem B).

Machine and status

• Machine: 1RB---_1LC1RE_1LD0LC_1LE1LC_1RF0RE_1RA0RB, viewer https://bbchallenge.org/1RB---_1LC1RE_1LD0LC_1LE1LC_1RF0RE_1RA0RB
• A BB(6) holdout: line 301 of the 740-machine list (line 322 of the 778-machine list). Spreadsheet class "Structural counter + counter".
• The proof is written for the string itself, with no mirror and no renaming.
• Template: none in busycoq applies.
• The nearest is verify/CounterCmp_v1.v, Module TM1 (1RB0LD_1RC0RE_0LA0RC_1LB1LD_0LF1RE_---1LA). Its table differs from this one in 11 of 12 transitions, and its rules do not hold here.
• The .v follows only the counter pattern of busycoq's verify/Example.v: unit lemmas proved by execution, with the arrival on the rest of the tape as a hypothesis.
• New here: walls that fire on every second carry, a nursery whose window runs touch the rest of the tape only through the wall rule, a closed counter system for the zone, and a conveyor invariant.
• Status: formalized. The accompanying .v (4,422 lines) proves Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9). It imports only Individual62 and the Coq standard library.
• Print Assumptions nonhalt: Closed under the global context.
• It compiles in about 5 minutes (315.6 s) with -native-compiler yes, and coqchk re-checks it in about 5 minutes (299.9 s).
• Checks: the labels S1–S12 in the text refer to the numerical checks of §10. They are evidence only; the result rests on the .v.

The transition table, with the start 0^inf A> 0^inf:

     0    1
A   1RB  ---        the only undefined transition: A reads 1
B   1LC  1RE
C   1LD  0LC
D   1LE  1LC
E   1RF  0RE
F   1RA  0RB

Where each part lives in the .v

The .v is split into 32 numbered sections, each opened by a comment banner. §9 explains where the .v takes a different route from the text.

A comment at the end of the .v restates the rules in busycoq's closing-comment style. §11 below has the same kind of table.

Summary

The proof has seven steps.

1. Units and carries (§1, §2). The tape right of the left gadget is read as a word of units. One walk of B to the right and C back is one carry. Theorem U says that it acts on the unit word as a recursive increment, inc.

2. Conveyor (§3). Three carries always turn the unit above a firing wall into a P. So the walls on the conveyor move up in order and never hit each other (Lemmas C1, C2).

3. Nursery (§4). The left end runs an exact cycle of 8 left records (Lemma N). Its window runs touch the unit word only through the wall rule, and they add 8 walls per cycle, below all older walls.

4. Top relation (§5). A flux identity (Lemma T) gives the carries that enter the zone between two absorptions. They depend only on the absorption number mod 8 and on the drops so far, so the zone follows a fixed closed system.

5. Zone (§6). From every canonical state C(b) the closed system reaches a later canonical state, with every step defined (Theorem B). With Lemmas Z0 and Z1, no shift in the zone is a hit.

6. Invariant (§7). At every left record the configuration is fixed by the record number n and the number J of absorptions so far. This invariant is closed under one record step, and each record step terminates.

7. Start (§8). The machine reaches the first record of the cycle after 203,465 steps.

§9 maps the argument to the .v, §10 lists the numerical checks, and §11 gives the rules at a glance.

1. Notation

Tape notation follows busycoq: 0^inf, B> (head in state B reading the cell to its right), <C (head in state C reading the cell to its left). Words are written left to right.

Units. A unit is a cell word h 1000, where the head h is a 0/1 word with no 000 inside it, or the 0 digit 0000.

Unit words. A unit word is a finite concatenation of units followed by 0^inf. Since D0 0^inf = 0^inf, trailing D0 units are part of the blank. So we always take a unit word in normal form: its last unit is not D0 (the empty word is the blank).

• In normal form the tokenisation is unique: read zeros in groups of 4 as D0, and the leftover zeros (0 to 3 of them) join the head of the next unit.
• Unit indices, digit positions and equality of zones are all read in normal form.
• A written form that ends in D0 units stands for its normal form, with those D0 units removed. For example ... D0 bin(q) with q = 0, where bin(0) is the empty word.

L_gap is the set of unit words whose heads are all in {ε, 0, 1, 01, 11}, that is, only the six units above. Deeper heads, such as 001, 011, 111, 101, 0111, 1111, 0101 and 1101, are called stacked.

Shift. When a W fires it leaves one extra 0 cell above it. Re-tokenised, that 0 passes over any D0 units and prepends a 0 to the head of the first other unit above it. We say the shift lands on that unit:

• on D1 it gives S1, and on P it gives SP; both are in L_gap;
• on S1, SP or W it gives the heads 00, 001 or 011. This is a hit, and it leaves L_gap;
• if only D0 units and the blank lie above, the 0 merges into the blank.

inc. inc(w) is the unit word after one carry enters w at its left end (§2.3).

Indices. inc keeps the normal form. A carry turns a unit into D0 only when it passes the carry on upward, so the last unit is never left as D0. A carry that passes the last unit appends a D1. A shift only prepends a 0 to a head, or merges into the blank.

• So, in normal form, inc never changes the number of units of a word, except that a carry reaching the blank top appends one D1.
• Every unit therefore keeps a fixed integer index for as long as it exists. Units added at the left end (§4) get smaller indices.
• S12 checks the normal form at every step of the closed-system orbit: no zone ever ends in D0.

2. Rules

2.1 Base macros

Each sweep is proved by induction on n, with one use of the induction hypothesis (S1).

  SR    B> (11000)^n        -->  (10111)^n B>        5n     B1 E1 E0 F0 A0 per block
  SR6   B> (111000)^n       -->  (100111)^n B>       6n
  KB    B> (1000)^n         -->  (1111)^n B>         4n     B1 E0 F0 A0 per block
  SL'   (10111)^n <C        -->  <C (11000)^n        5n     C1 C1 C1 C0 D1 per block
  SL    (11110)^n <C        -->  <C (00011)^n        5n
  KC    1^n <C              -->  <C 0^n              n      C1
  EdgeL 0^inf <C            -->  0^inf 1 0 B> 1      4      C0 D0 E0 F1

2.2 Unit lemmas

Arrival. Write Arr(w) = w' (in s steps) for

l B> w 0^inf   -->(s)   l <C w' 0^inf

for every left context l. The head never moves left of w's first cell until the last step, and the last step moves it off w to the left in state C.

Oracle proof. Each unit lemma below is proved by running the machine on the unit's own cells alone, with the rest r of the word replaced by an oracle:

• When the head steps onto r's first cell, it must be in state B. The hypothesis Arr(r) = r' then returns the head to the unit's last cell in state C, with r replaced by r'.
• Any other contact with r, or a halt, fails the lemma.

These are finite computations (S2). Here are the chains:

unit lemmas: unit . r  -->  unit' . r'     (r' = result of the nested arrivals Arr(r), Arr(Arr(r)), ...)

  Z   first cell 0 (D0, S1, SP, and every 0-led head; also the blank top):
        B> 0 x      -->  <C 1 x                                   1          B0
  D1    B> 1000 r   -->  1111 B> r  ~Arr~>  1111 <C r'  -->  <C 0000 r'                         4 + 4
  P     B> 11000 r  -->  10111 B> r ~Arr~>  10111 <C r' -->  <C 11000 r'                        5 + 5      (SR, SL')
  W     B> 111000 r -->  100111 B> r  ~Arr~>  100111 <C r'  -->  000111 B> r'                   6, 11
                    ~Arr~> 000111 <C r''  -->  101111 B> r''  ~Arr~>  101111 <C r'''  -->  <C 110000 r'''     11, 6
        i.e. W r --> P . shift(inc^3 r)                                                          kappa = 34

  stacked heads (needed only to show what a hit does; never reached, section 6):
  111   B> 1111000 r  --> 1000111 B> r ~> 1000111 <C r' --> 1101111 B> r' ~> 1101111 <C r'' --> <C 0110000 r''
        i.e. 111 . r --> SP . shift(inc^2 r)                                                     kappa = 25
  101   101 . r   --> SP . shift(inc r)                                                          kappa = 14
  1111  1111 . r  --> 111 . shift(inc^2 r)                                                       kappa = 27
  1101  1101 . r  --> 111 . shift(inc r)                                                         kappa = 16
  depth 4: 11111 and 11101 have no oracle proof (state E walks onto r); 01111 -> 11111, 01101 -> 11101 by Z.

Here shift(x) means the extra 0 cell 0 x, re-tokenised as in §1. The cell identity h 1000 0 x = h 1000 . shift(x) is pure re-reading, so no machine step is involved.

The W lemma holds for every left context l, and §4 uses this.

What a hit does (aside, not used). The main argument excludes every hit. A hit on SP or W gives the stacked heads 001 or 011, which have rows above. A hit on S1 gives head 00.

The next carry on 00 meets head 10, which has no unit rule. Its oracle run gives 101000 -> 011100 in 7 steps, which takes a cell from the unit above. A shift that lands on 001 gives 0001, which is not a valid head. So a stacked unit can leave the unit calculus in more than one way, and the proof never lets one arise.

2.3 Theorem U (arrival = inc)

Define the relation Inc(w, w', s) ("one carry turns w into w' in s machine steps") inductively by the table in §2.2:

• Inc(0^inf, D1, 1) (the top case);
• first cell 0: Inc(0 x, 1 x, 1);
• D1: if Inc(r, r', s) then Inc(D1 . r, D0 . r', 8 + s);
• P: if Inc(r, r', s) then Inc(P . r, P . r', 10 + s);
• W: if Inc(r, r1, s1), Inc(r1, r2, s2) and Inc(r2, r3, s3), then Inc(W . r, P . shift(r3), 34 + s1 + s2 + s3);
• the stacked heads 111, 101, 1111 and 1101 follow their rows in the same way (κ = 25, 14, 27, 16).

inc(w) is defined when some (then unique) w', s with Inc(w, w', s) exist. That is, the recursion is finite and never meets a head outside the table.

Theorem U. If Inc(w, w', s), then Arr(w) = w' in exactly s machine steps.

Proof. Induction on the derivation of Inc(w, w', s). The last rule used is the unit lemma of w's first unit (§2.2). Its oracle calls are exactly the premises of that rule, which are smaller derivations.

So the induction hypothesis turns each oracle call into a real machine run, ending on the unit's last cell in state C as the oracle requires. Re-tokenising after a shift is a cell identity. ∎

The induction is on the derivation, not on the cell length of w. W's second and third oracle calls are on inc(r) and inc²(r), which need not be shorter than w.

Lemma U-term (termination). Let w ∈ L_gap have n units, and suppose no W firing inside the recursion for inc(w) is a hit. Then inc(w) is defined.

Proof. We prove a stronger statement by induction on the number of walls (SP and W units) of w:

If w ∈ L_gap and no W firing inside the recursion for inc(w) is a hit, then inc(w) is defined, inc(w) ∈ L_gap, and inc(w) has at most as many walls as w.

1. No wall creation. The rows never raise the wall count. SP becomes W on a carry. W becomes P when it fires, and its shift turns at most one unit above into a wall (P into SP); on D1 or the blank it makes none. D1, D0, P and S1 never become walls by a carry.

2. Base: w has no wall. Its units are D0, D1, P and S1. Each forwards at most one carry (D1, P) or stops it (D0, S1). So an arrival is one upward path of at most n + 1 unit steps, and the top step appends a D1. inc(w) is in L_gap and has no wall.

3. Step: w has walls. Write w = x · V · y, where V is the lowest wall and x is wall-free.

• The carry climbs x as in the base case. It stops in x, or it reaches V.
• If V = SP, it becomes W and the carry stops.
• If V = W, the row needs inc(y), inc(inc(y)) and inc³(y). Here y has fewer walls than w, so inc(y) is defined, lies in L_gap, and has no more walls than y (induction hypothesis).
• The same holds for inc(y) and then for inc²(y). These nested recursions are part of the recursion for inc(w), so they have no hit either.
• The shift then lands on D1 (making S1), on P (making SP) or on the blank. A hit is excluded by assumption.
• In every case inc(w) ∈ L_gap, and its wall count is at most that of w (item 1). ∎

A carry can leave a wall above the old top of the word. For example, one arrival on W W SP gives P SP P SP D0 D0 D1 (237 machine steps). The induction on walls needs no claim about that region. S3 checks the wall-count bound on every L_gap word it runs.

S3 also compares the machine and inc, cells and exact step counts, on every unit word of up to 4 units over 14 unit kinds, and on 20,000 random words with long P runs: 0 mismatches.

Corollary U′. Let w ∈ L_gap, and suppose no W firing inside the recursion for inc(w) is a hit. Then inc(w) is defined and inc(w) ∈ L_gap.

Proof. The L_gap rows produce only L_gap heads, except for the shift. A shift lands on D1 (giving S1), on P (giving SP), on the blank, or is a hit. Termination is Lemma U-term. ∎

So the machine halts only after a hit. The halting transition A1 is never used by any unit lemma: in every oracle proof, state A reads 0.

3. The conveyor cannot be hit (Lemmas C1 and C2)

Lemma C1. If the first unit of x is P, S1, SP or W, then inc³(x) starts with P.

Proof. What happens to the first unit depends only on that unit, because its carries and its shift go to the units above.

• P stays P.
• S1 becomes P after one carry.
• SP becomes W, then fires and becomes P.
• W fires and becomes P.

A P then stays P. ∎ (S5 also runs the four cases.)

Lemma C2 (no hit below the zone). A W firing whose unit directly above is P, S1, SP or W is not a hit. Its shift lands on that unit, which is P after the 3 carries (C1), so it becomes SP: the wall has moved up one unit.

Moreover, a prefix of a unit word made of P, SP and W units stays so under inc, and can only grow. These units only turn into P, SP or W, and a zone unit above can only join by becoming P. ∎

So a hit needs a firing W whose unit directly above is a digit. The conveyor (§4) has no digits. In particular, a W directly followed by S1, SP or W is harmless.

4. The nursery (Lemma N)

Left records and gadgets. A left record is a time at which the head stands on a cell never visited before, at the left end. From step 203,465 on, the records come in a fixed cycle of 8, XC XD XE YC YD YE ZD ZE (record group, then state). At a record the tape is

0^inf <q G U 0^inf

Here the gadget G is the first three 1-runs after the head cell together with the 3 cells after them. U is the rest, read as a unit word.

The window computation. Run the machine on the head cell and G only. The rest R (initially U) is opaque. The run may touch it only through two proved rules:

• (arr) The head steps onto R's first cell in state B. By Theorem U, R becomes inc(R) and the head is back on the window's last cell in state C.
• (W) The head stands in state B on the first of the window's last six cells, and they read 111000. The W lemma (valid for every left context) applies with r = R: R receives three carries, the six cells become 110000, and the trailing 0 is the shift.
• In case (W), Lemma C1 gives that inc³(R) starts with P if R's first unit was not a digit. So the shift makes that P an SP. Its five cells 11000 move from R into the window (a pop), and R loses its first unit.

Any other contact with R, or a halt, would fail the computation. The run ends when the head steps onto a new cell left of the window, which is the next left record.

The window's cells after the new gadget must then read as units in {P, SP, W}. Call them F; they are put in front of R.

Lemma N. For each of the 8 record types the window computation succeeds as tabulated, and the 8 computations form a closed cycle (from XC back to XC with the same gadget). Only rule (W) is ever used.

record  gadget G                       next   W-rule uses   F (put in front of R)            window steps
XC      111111 0000 11 0000 11 000     XD     0             -                                1
XD      1111111 0000 11 0000 11 000    XE     0             -                                1
XE      11111111 0000 11 0000 11 000   YC     3             W W P SP                         334
YC      1101111 0000 11 000            YD     0             -                                1
YD      11101111 0000 11 000           YE     0             -                                1
YE      111101111 0000 11 000          ZD     12            W P W P P SP P P P P SP          1,785
ZD      11111 0000 11 000 111 000      ZE     0             -                                1
ZE      111111 0000 11 000 111 000     XC     2             P SP                             155

So, with Φ_k := (pop ∘ inc³)^k, one cycle maps the right part as

U  -->  F_XE . Phi_3(U)  -->  F_YE . Phi_12( . )  -->  F_ZE . Phi_2( . )

and the gadgets repeat exactly. The machine steps of an excursion are the window steps plus the steps of all arrivals (Theorem U).

Side condition. Each pop needs R's first unit to be P, S1, SP or W just before the three carries (Lemma C1). Let c(U) be the number of leading units of U in {P, SP, W}.

inc never decreases c (Lemma C2), a pop decreases it by 1, and F adds |F|. Per excursion, (pops, |F|) = (3, 4), (12, 11) and (2, 2). U_0 has c = 43 (§8), so c ≥ 42 at every record and c ≥ 30 inside every excursion. The side condition always holds.

Proof of Lemma N. The 8 window runs are finite computations (S5 prints them). By induction over records, the tape at the n-th record is 0^inf <q_n G_n U_n 0^inf, with (q_n, G_n) the (n mod 8)-th row and c(U_n) ≥ 42.

Each step is the window run, whose contacts with R are justified by Theorem U, the W lemma and Lemma C1. ∎

Cross-check (S5). At every left record to 2e9 (1,021 transitions), the machine's next record equals G' F Φ_k(U) in cells and state. The step difference equals the window steps plus the inc step counts exactly. Every record is in L_gap and has c ≥ 42.

Why the boundary moves. No static cell boundary separates the nursery from the conveyor. Walls cross every cell near the left edge, and a W that straddles a static boundary touches R in state E.

Rule (W) is the moving boundary: a firing wall at the top of the window pulls the next P into the window.

Births. The walls of F are the new conveyor walls, 8 per cycle. Use the index frame of U_0 (its first unit has index 0). Then F always lands at the same indices:

• XE puts W W P SP at −1..2;
• YE puts W P W P P SP P P P P SP at 0..10;
• ZE puts P SP at 0..1.

In absorption order (highest first), the births of one cycle are:

birth phase   from   index b   born as   s
0             XE      2        SP        0
1             XE      0        W         1
2             XE     -1        W         1
3             YE     10        SP        0
4             YE      5        SP        0
5             YE      2        W         1
6             YE      0        W         1
7             ZE      1        SP        0

A wall, once in U, moves only by inc. It is never popped, because a pop removes a P (Lemma C1). By Lemma C2, walls never overtake or hit each other.

FIFO also needs placement. Every newborn wall must sit below all existing walls. At a birth record the previous lowest wall is the youngest wall of the previous group. It has received exactly H carries since its birth (H as in §5: 36, 6 or 9), so it sits at b + ⌊(H + s)/2⌋:

So the walls stay in birth order along the word and are absorbed in birth order (FIFO). S6 checks the placement at every birth of its run.

5. The top relation (Lemma T) and the closed zone system

Zone and absorptions. The top wall is the highest conveyor wall. The zone bottom z is the index of the first unit above it that is not P. The units from z up form the zone Z, and the P units between the top wall and z form its wire.

Absorption j (j = 0, 1, 2, …) is a firing of the top wall after which the wall does not move up. That is, after the three carries the unit directly above the wall is not P. Then the wall was at z − 1, and its shift lands in the zone:

• on a digit at or above z (a D1 directly above the wall becomes S1; this is the most common case), or
• on a zone P above some D0 units (it becomes SP, a zone wall).

If instead the three carries turn the unit above into P (a drop, z += 1), the shift lands on that P and the wall moves up one unit.

Counts. Let N_j be the number of carries that enter the zone between absorptions j−1 and j. Let A_j be the number of P units that leave the zone bottom in that interval (the drops; each one is z += 1). Let D_j = A_1 + … + A_(j−1). Nothing else moves z, so z = z_0 + (drops so far).

Lemma T. For every j ≥ 1:

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

Proof. Number the walls in birth order. The 6 walls of U_0 come first; they count as born at the step-203,465 record, with b their index there and s = 1 for W. The births of §4 follow. By FIFO, absorption j removes wall number j.

For a wall w let b_w be its birth index, s_w ∈ {0, 1} its birth state (SP or W), and R_w(t) the carries it has received since birth. A wall fires on every second carry, so it has fired ⌊(R_w + s_w)/2⌋ times and sits at index b_w + ⌊(R_w + s_w)/2⌋.

1. Wall j exists before absorption j−1. Wall j is born at the same record as wall j−1, or at the end of the next excursion. Before then, wall j−1 receives only that excursion's carries (at most 36). Its absorption needs 2(z − b_(j−1)) − s ≥ 2·33 − 1 carries, since z ≥ 43 and b ≤ 10.

2. Wall j−1's carries. Let H_(j−1) be the carries wall j−1 received before wall j's birth. After that, every carry it receives comes from wall j, because carries only move up and wall j is the next wall below it. With E_j(t) the carries wall j has emitted since its birth, R_(j−1) = H_(j−1) + E_j.

3. At absorption j−1. Wall j−1 fires from index z(t_(j−1)) − 1. That is its (z(t_(j−1)) − b_(j−1))-th firing, so R_(j−1) = 2(z(t_(j−1)) − b_(j−1)) − s_(j−1).

• This firing happens inside a triple of wall j. Say wall j has fired f times (this triple included), with r ∈ {0, 1, 2} carries of the triple still to come. Then E_j = 3f − r.

4. Interval j. Wall j is now the top wall, so every carry that enters the zone comes from it: the r leftover carries, then 3 per further firing.

• Wall j is absorbed when it fires from z(t_j) − 1, after z(t_j) − b_j firings in all. So N_j = r + 3(z(t_j) − b_j − f).

5. Substitute 3f − r from items 2 and 3, and use z(t_j) − z(t_(j−1)) = A_j and z(t_(j−1)) = z(t_0) + D_j:

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

The bracket depends only on the birth data of walls j and j−1. By §4 these repeat with the birth phase, and FIFO fixes the birth phase as j mod 8 plus a constant. The values are:

• z(t_0) = 43 (no drop in the partial interval 0);
• H = 0 for two walls born at the same record;
• H = 36 for the last XE wall (the next excursion, YE, makes 12 W-rule uses), 6 for the last YE wall (ZE), and 9 for the ZE wall (XE).

With the table of §4 the bracket is 47 or 48, exactly as p says.

For j = 1..6 the walls of U_0 enter, with indices 32, 20, 12, 7, 3, 1, H = 0 between them, and H = 9 for the pair (U_0's SP at 1, XE's SP at 2). The formula gives 48, 48, 47, 48, 47, 48 = p(1..6). ∎

Level-ups play no role. A level-up adds one wall to the conveyor. That lengthens the time from a wall's birth to its absorption. It does not change which wall absorption j removes (FIFO), so p stays indexed by j mod 8.

With FIFO the pairing of absorption j with wall j is fixed. What a level-up shifts is only the time slot inside a cycle at which absorption j happens.

Checks (S6). A unit-level run of the right part, driven by the cycle of §4 from U_0 (150 cycles, 1,192 absorptions, conveyor wall count 6 → 14, so 8 level-ups):

• it equals the machine at every left record of S5 (cells);
• the wall absorbed at j is wall number j (FIFO);
• Lemma T and the bracket identity hold for every j ≥ 1;
• the zone right after absorption 0 is Z_1 below, with N_0 = 33;
• the closed system started from that zone reproduces every N_j, with no zone wall alive at an absorption and no hit;
• a stored machine replay (4,820 absorptions, to step 1.93e11) agrees on the overlap.

The closed system (definition). The state is (Z, D, j): Z is a zone word, and D, j are integers. One step is:

1. Feed c = D + p(j mod 8) carries at the bottom of Z, each by Theorem U.

2. Whenever the bottom unit of Z is P, remove it (a drop). Each drop adds 3 to the carries still to be fed.

3. Apply the absorption shift at the bottom of Z: the first non-D0 unit gets a 0 prepended to its head. D1 becomes S1, and P becomes SP (a zone wall is born). Landing on anything else is a hit.

4. D += (drops in this step), j += 1.

This is exactly the real interval. A P passes carries unchanged, so the zone after interval j is inc^(N_j) of the zone, with leading P units moved to the wire, whatever the order.

Write A(m) for the number of drops after m carries of the interval. Steps 1-2 stop at the least m ≥ c with m = c + 3A(m) (a fixed point).

• The real absorption comes at a triple boundary of the top wall (the moment its three carries of one firing have all entered the zone) at which m = c + 3A(m). A drop caused by the last triple makes the top wall move up instead of being absorbed; that is the "3 more" of step 2.
• At every earlier triple boundary m < c + 3A(m) (§7, Closure).

No fixed point lies between triple boundaries. Let r ∈ {0, 1, 2} be the number of carries of the top wall's triple still to come at absorption j − 1 (r and f as in item 3 of the proof of Lemma T). The triple boundaries of interval j are exactly the m ≥ r with m ≡ r (mod 3): first the r leftover carries, then 3 per firing.

Items 2, 3 and 5 of that proof give

c = D_j + p(j mod 8) = 3*(z(t_0) + D_j - b_j - f) + r,     so  c ≡ r (mod 3).

A fixed point has m ≡ c ≡ r (mod 3) and m ≥ c ≥ 47 > r, so it is a triple boundary.

So the least fixed point is the first triple boundary that is a fixed point, which is the real absorption. S6 reads r off the unit-level run at every absorption and checks r ∈ {0, 1, 2} and c ≡ r (mod 3); all three values of r occur.

So, by Lemma T, the zone read at its absorptions is this system, started from

Z_1 = S1 D0 D1 D1 D1 D0 D1,   D = 0,   j = 1

which is the zone D0 D0 D1 D1 D1 D1 of the step-203,465 record after the partial interval j = 0 (33 carries, then the absorption shift).

Where the 3/2 arithmetic goes. Lemma T is where the 3/2 conveyor enters, and it enters only through the constant vector p. That is why the zone stays a 2-adic counter problem rather than Mahler-type 3/2 arithmetic.

6. The zone never gets a hit (Theorem B)

Alive walls. A zone wall is alive at an absorption if, just before an absorption shift, Z contains a unit whose head is not ε, 0 or 1. That is a unit other than D0, D1, S1 and P. This includes SP, W, the head 00 and every stacked head.

A step is defined if every carry of its carry phase meets a head that has a row (§2.3). A run that reaches a canonical state (below) is defined at every step.

Two facts about single carries are used below.

• (F1) A non-digit unit never becomes a digit unit: every row maps a head to a nonempty head, and a shift only prepends a 0. A non-digit unit leaves Z only by a drop.
• (F2) An S1 that receives a carry becomes P. Only a shift landing on a D1 makes a new S1.

Lemma Z1 (the absorption shift never lands on S1). Take a defined step of the closed system with feed c ≥ 1. At the end of its carry phase, the first non-D0 unit of Z is not an S1.

Proof. Suppose the first non-D0 unit u is an S1 at the end. By (F2), u has received no carry since it became an S1. Let E be the last of these events in the step: its start, the creation of u (if u is created during the step), or a drop.

• By (F1), a non-digit unit below u after E would still be below u at the end, where only D0 units are. So after E every unit below u is a digit unit. They form a counter of some r digits at the bottom of Z, with value x right after E.
• Every carry fed after E enters this counter, and none reaches u. With t such carries, x + t < 2^r, and the counter ends at 0. So x = t = 0.

Each choice of E contradicts this:

• E is the start of the step. Then t = c ≥ 1.
• E is a drop. A drop raises the number of carries the phase feeds by 3, and when it happens the carries fed so far do not exceed the old number. So t ≥ 3.
• E is the creation of u. A wall's shift made u, and that wall is P right after it fires, below u. By (F1) this P must leave Z by a drop later, so E was not the last event.

The feed is c = D + p ≥ 47, so the lemma applies to every step. ∎

Lemma Z0 (no alive wall, no hit). Take a run of the closed system in which every step is defined and no zone wall is alive at any absorption. Then no shift of the run is a hit, and every head stays in L_gap.

Proof.

• Absorption shifts. By hypothesis the first non-D0 unit is D1, S1 or P (or there is none, and the shift merges into the blank). By Lemma Z1 it is not S1. So the shift makes an S1 or an SP, or it merges into the blank.
• At most one wall. Right after an absorption at most one unit lies outside {D0, D1, S1, P}: the SP just born, if the shift landed on a P. Carries never turn D0, D1, S1 or P into a wall. A wall's shift that lands on a P only moves that same wall up. So there is never a second wall.
• Wall shifts. The single wall's shift lands on the first non-D0 unit above it, after its 3 carries:
• on a P: the same wall moves up one unit;
• on a D1: it becomes S1, and the wall is dissolved;
• on the blank: the wall is dissolved;
• on an S1: the head 00 appears. If it then receives a carry it becomes 10, which has no row, so the step is not defined. Otherwise it is still there at the next absorption, where it is alive. Both are excluded.
• SP and W cannot be landed on, because the only wall is the emitter, and a shift lands above its emitter. ∎

In the runs of Lemmas L and L′ (§6.3, §6.4), a wall shift landing on an S1 would also violate (H2): the zone would not be clean after the first T0 carries.

S12 classifies every shift of the closed-system orbit from Z_1 to j = 32·131,250. Every one lands on a D1 or a P. S12 also tests Lemma Z1 directly, on every zone of at most 6 units over D0, D1, S1, P, SP and W with every feed c = 1..40, and on 200,000 random zones with any number of walls. None ends its carry phase with an S1 as the first non-D0 unit. With c = 0, the negative control does find S1 there.

Canonical states. For b ≥ 0, let C(b) be the state at j = 32b + 17 with

Z = S1 D0 D1 D1 D1 D1 bin(b+1),   D = j − 1

where bin(x) lists the binary digits of x, least significant first, as D0/D1 (bin(0) is the empty word). Write b + 2 = o·2^k with o odd, k = ν2(b+2) the class, and q = (o−1)/2. Then

Z(C(b)) = S1 D0 D1^(k+4) D0 bin(q)

When q = 0 this ends in D0 and stands for its normal form S1 D0 D1^(k+4) (§1).

Base (S7). From Z_1, the closed system passes through C(b) for every b = 0..131,249. On the way it creates 690,078 zone walls, with 0 alive at an absorption and 0 hits. In particular, C(0) is reached at j = 17.

Theorem B (block map). For every b ≥ 0, the closed system goes from C(b) to C(b′) for some b′ > b, with every step defined and no zone wall alive at any absorption in between.

Here b′ > b holds because every piece below ends in a canonical state reached after at least one step: C(b′) sits at j′ = 32b′ + 17 > j = 32b + 17. The value of b′ is not used.

Observation (not used, not proved). The random runs of S8 (every class k ≤ 130, so ν2(k+9) ≤ 7, with random b) all give b′ = b + 1 + ⌊(k+9)/32⌋. We make no claim about b′ in general.

The proof splits by the phase offset off = j − 32b (the block starts at off = 17). Every piece is a run of the closed system:

• The entry (§6.1) and the plant (§6.5) are short hand computations on closed forms.
• The value form (§6.2) is carried from the entry down to marker height 3 by Lemma VF (§6.3). Its proof is a one-step version of Lemma L that lets the marker sit above the cut (Lemma L′), plus 1,304 one-step representative runs.
• The endgame, the small classes, the nested range and the class recursion follow from Lemma L (§6.4–§6.6).

6.1 Entry: off 17 → 20 (Lemma E)

Let b + 2 = o·2^k with o = 2q + 1 odd and k ≥ 3. At offset off the step number is

j = 32b + off = o*2^(k+5) - 64 + off

and the feed is c = D + p(off mod 8). Write bin(x) for the digits of x, least significant first; bin(0) is the empty word.

For q = 0 the forms at off 17 and 20 end in D0 units and stand for their normal forms (§1): S1 D0 D1^(k+4) and D0 S1 D0^(k+2) D1 P.

Lemma E. The run from C(b) passes through these states, with no zone wall alive at an absorption and no hit:

off   zone                                         D - j
17    S1 D0 D1^(k+4) D0 bin(q)                     -1        (this is C(b))
18    D0^(k+6) S1 bin(q)                           -1
19    S1 D0^(k+4) D1 P D1 bin(q-1)     (q >= 1)    -2
      S1 D0^(k+4) D1 S1                (q = 0)     -2
20    D0 S1 D0^(k+2) D1 P D0 D0 bin(q)             -2

Proof. In each step the bottom S1 (if there is one) absorbs one carry and becomes P. A P at the bottom drops and adds 3 carries. Everything else is binary addition, and the absorption shift lands on the lowest D1.

• 17 → 18. c = (j − 1) + 48 = o·2^(k+5). The S1 absorbs one carry and drops (A = 1), so the digits receive o·2^(k+5) + 2.
• Their value was V(C(b)) = o·2^(k+5) − 2, so it becomes o·2^(k+6): the word D0^(k+6) D1 bin(q).
• The shift lands on that D1, at digit k + 6.
• 18 → 19. c = (j − 1) + 48 = o·2^(k+5) + 1, and nothing drops. The k + 6 zero digits end at 2^(k+5) + 1 and pass q carries up.
• If q ≥ 1, the S1 absorbs the first of them and becomes P (the marker). The other q − 1 turn bin(q) into bin(2q − 1) = D1 bin(q−1).
• If q = 0, nothing reaches the S1.
• The shift lands on digit 0.
• 19 → 20. c = (j − 2) + 47 = o·2^(k+5). The S1 absorbs one carry and drops (A = 1). The k + 5 digits D0^(k+4) D1 (value 2^(k+4)) receive o·2^(k+5) + 2. They end at 2^(k+4) + 2 and pass 2q + 1 carries up.
• If q ≥ 1, these cross the marker and turn bin(2q − 1) into bin(4q) = D0 D0 bin(q).
• If q = 0, the one carry is absorbed by the top S1, which becomes the marker P.
• The shift lands on digit 1.

No SP or W unit occurs, so no wall is alive and nothing is hit. ∎

S11 checks the four forms against the closed system on 2,000 random (k, o): k up to 1,500, o up to 400 bits, 405 of them with o = 1. All 2,000 match.

6.2 The value form (definition)

The marker is transparent to the digit arithmetic: a P passes carries and has no weight. So the zone during the descent is described by one number, the value of all its digits.

For a class k, an offset off and an integer Ω (the upper part: Ω = o·2^(k+5) at level 1), the value-form state VF(k, Ω, off) is:

zone:  the binary word of   Vtot = mu*Omega + w(off) - 3*2^(L-1),      L = k + lam - off
       with the heads at fixed digit positions and the marker P at digit position L
j = Omega - 64 + off,     D = j + d

Here (heads, λ, w, d) come from two tables below, and μ = 2 when λ = 25, else μ = 1. The legend for the heads:

• "X@p" puts the units X directly below the digit unit at position p, so they have exactly p digit units below them. "S1@1" is an S1 just above digit 0; "PP@0" is a run of two P units just below digit 0.
• Heads at the same digit position are listed bottom to top. So S1@0 PP@0 is the word S1 P P below digit 0, and S1@2 P@2 is S1 P between digits 1 and 2.
• The marker never shares a position with a head: the heads sit at positions ≤ 3, the marker at L ≥ 3, and L = 3 occurs only in phase 4, whose heads are at 0.

Entry table (used at level 1 for 20 ≤ off ≤ 31):

off  heads            lam  w    d        off  heads            lam  w    d
20   S1@1             24   0   -2        26   S1@0 PPP@1       24  -4   -5
21   SP@1             25   0   -3        27   S1@0 PPP@0       24   1   -5
22   S1@0 PP@0        24  -2   -4        28   S1@0             24   8   -2
23   S1@3             24   0   -2        29   S1@2             24   8   -2
24   S1@2 P@2         24  -4   -3        30   S1@1 P@1         24   6   -3
25   SP@2 P@2         25  -4   -4        31   S1@0 PP@0        24   7   -4

Phase table (used for every other offset, by φ = off mod 8):

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

Two facts used below:

• At off = 20 the state of Lemma E is VF(k, o·2^(k+5), 20). Its heads are S1@1, its marker sits at L = k + 4, and Vtot = 2^(k+3) + q·2^(k+6) = o·2^(k+5) − 3·2^(k+3).
• In the phase table, w has slope 1 in off, except slope 2 at φ = 3.

End offset. off_end(k) is k + 20, or k + 21 when k + 20 ≡ 3 (mod 8). There the marker height is 4, or 3 in phase 4. This is the start state of the endgame (§6.4) and of the nested range and the plant (§6.5). Every offset before it has L ≥ 5.

We write VF_L(k, U) for VF(k, U·2^(k+5), off) at the offset where the marker height is L.

6.3 Lemma VF

Lemma VF.

• Level 1. For every class k ≥ 41 and odd o, the run from C(b) passes through VF(k, o·2^(k+5), off) for every off from 20 to off_end(k).
• Level 2. For every v ≥ 12 and odd S ≥ 3, the run from the plant's off′ = 17 state (§6.5) passes through VF(v − 10, S·2^v, off′) for every off′ from 17 to off_end(v − 10). Level 2 uses the phase table at every offset.

There is no zone wall alive at an absorption and no hit anywhere on the way.

The class recursion uses level 2 only for large v (v > 600 in §6.5, or v > 50 in its smaller split). For v ≤ 10 and small S the feed can be below T0 = 2^12, so Lemma VS does not apply there; v ≥ 12 is a round margin.

The proof is an induction on the offset. One step is Lemma VS below, which follows from a one-step locality lemma.

Lemma L′ (one-step locality, marker above the cut). Let s = (Z, D, j) be a representative and s′ = (Z′, D′, j′) a member, with cut R ≥ 3. Suppose:

• (M1′) j′ ≡ j (mod 8), and the feeds differ by Δ = c′ − c ≡ 0 (mod 2^R).
• (M2′) Z = X·Y and Z′ = X·Y′. X runs up to and including the digit unit at position R − 1. Each of Y and Y′ consists of digit units and at most one P unit, possibly at different digit positions.
• (M4′) c′ ≥ T0.

Suppose also that the representative's step satisfies:

• (H0′) every non-digit unit of Z, except one single P, has at most R − 1 digit units below it, so it lies in X;
• (H1) as in Lemma L (§6.4), with r starting at R: every shift landing in the step is on a unit with at most r − 1 digit units below it, so on a unit of X;
• (H2) T0 ≤ c, the zone is clean (D0, D1, P only) after the first T0 carries, no digit unit is lost after T0, and X keeps at least one digit unit.

Let a and b count the landings on a D1 among the first T0 carries and at the absorption shift. Then the member's step has the same wall firings, landings, drops, alive walls and hits as the representative's. It ends with Z′_next = X_next · Y′_next, where:

• X_next is the X-part of the representative's next zone;
• the P of Y′ (if any) has moved down a + b digit positions;
• V(Z′_next) − V(Z_next) = (H/2^a + Δ)/2^b, with H = V(Z′) − V(Z).

Proof. This is items 1-5 of the proof of Lemma L, for one step. The only new point is the P in Y and Y′:

• A P passes carries (its Inc row), so Y and Y′ are still counters, and the P has no weight in V.
• No shift lands on it, by (H1). It starts with at least R = r digit units below it, and each landing on a D1 (in X, below it) lowers both that count and r by one, so it always has at least r.
• It is never at the bottom, because X keeps a digit unit below it. Digit units are never dropped; only a landing turns a D1 into an S1.
• Landings in X remove a + b digit units below it, and nothing else changes the number of digits below it. ∎

Lemma VS (one descent step). Take R = 8 and T0 = 2^12. Let (k, Ω, off) satisfy Ω ≡ 0 (mod 2^8) and c ≥ 2^12, and one of:

• (E) level 1, 20 ≤ off ≤ 31, and L ≥ 9;
• (A) the phase table, and L ≥ 9;
• (B) the phase table, and 5 ≤ L ≤ 8.

Then one closed-system step takes VF(k, Ω, off) to VF(k, Ω, off + 1), with no zone wall alive at the absorption and no hit.

Proof. Pick the representative of the case:

• (E) the same off, with k0 = 41 (o0 = 1 and o0 = 3 are both run);
• (A) off0 ≡ off (mod 2^8), with off0 in 32..287 and L0 = 11;
• (B) off0 ≡ off (mod 2^8), with off0 in 32..287 and L0 = L.

In each case Ω0 = 3·2^(k0+5).

1. Member conditions. Write δΩ = Ω − Ω0, δo = off − off0 and δM = 2^(L−1) − 2^(L0−1). Then

H = mu*dOmega + wa*do - 3*dM, Delta = dOmega + do,

where wa is the slope of w (0 for the entry table, whose members have δo = 0).

• δΩ ≡ 0 (mod 2^8) and δo ≡ 0 (mod 2^8) by the choice of the representative.
• δM ≡ 0 (mod 2^8), because L, L0 ≥ 9 in (E) and (A), and L = L0 in (B).
• So the digits below position 8 agree, and the heads are the same, since they depend only on off (E) or φ (A, B).
• The marker is in Y (E, A) or at the same place (B), and c′ ≥ 2^12 = T0.
• j′ ≡ j (mod 8), since j = Ω − 64 + off. So both runs read the same p, and Δ is the feed difference of (M1′).

2. The representative. S11 runs each representative's step under the checks of Lemma L′. All 24 + 256 + 1,024 steps satisfy (H0′)-(H2) and end exactly in VF(k0, Ω0, off0 + 1), with no alive wall and no hit.

• The highest landing is at digit 3, and X keeps at least 6 digit units.
• The landing counts (a, b) depend only on the form: (0, 1) for every step except (0, 0) at phase 2 and at off 20 and 24, and (1, 1) at phase 3 and at off 21 and 25.

3. Algebra. By Lemma L′ the member's next value differs from the representative's by

(H/2^a + Delta)/2^b = [(mu/2^a + 1)/2^b]*dOmega + [(wa/2^a + 1)/2^b]*do - 3*dM/2^(a+b).

S11 checks that (μ/2^a + 1)/2^b = μ′ and (wa/2^a + 1)/2^b = wa′ at every representative, where μ′ and wa′ belong to the next form, and that L(off + 1) − L(off) = −(a + b). So the difference is exactly Vtot(k, Ω, off + 1) − Vtot(k0, Ω0, off0 + 1).

4. The next state. The member's next zone has:

• the representative's X_next, which holds the next form's heads;
• its marker at L − a − b = L(k, off + 1);
• digit value Vtot(k, Ω, off + 1).

After the step, X_next covers the digit positions below 8 − a − b, since the landings removed a + b digit units from X.

• The representative's X_next is the part of VF(k0, Ω0, off0 + 1) below that position (S11 compares the whole unit list).
• VF(k, Ω, off + 1) has the same part there. Its heads depend only on the form and lie at digit positions ≤ 3.
• Its value differs from the representative's next value by (H/2^a + Δ)/2^b, which is a multiple of 2^(8 − a − b) because H and Δ are multiples of 2^8.
• Above that position, a zone is fixed by its digits and the digit position of its one P.

So the member's next zone is VF(k, Ω, off + 1). The value D − j moves by A − 1, as in the representative. ∎

Proof of Lemma VF. Level 1 starts from VF at off 20 (Lemma E). Level 2 starts from VF at off′ = 17 (the plant lemma, §6.5). Every step from there to off_end has L ≥ 5, so it is case (E), (A) or (B) of Lemma VS. The conditions hold:

• At level 1, Ω = o·2^(k+5) with k ≥ 41. So c ≥ 2^46 − 64, and L ≥ 34 at every off ≤ 31.
• At level 2, Ω = S·2^v = 32S·2^(K′+5) with K′ = v − 10. Since v ≥ 12, Ω ≡ 0 (mod 2^8), and c = Ω − 64 + off′ + d + p ≥ 3·2^12 − 64 + 17 − 5 + 47 > 2^12. At off′ = 17 the marker height is L = v − 3 ≥ 9. ∎

Checks beyond the proof (S11):

• Real runs from C(b), with random k in 41..400 and random o, equal the forms of Lemma E and then VF at every offset to off_end: 300 runs, 68,308 states.
• From the plant start, with random v in 12..400, the run equals the plant forms and then level-2 VF to off_end: 300 runs, 62,723 states.
• 2,969 random members, with k up to 3,000 and o up to 300 bits, at both levels: one real step from VF(off) gives VF(off + 1).
• Negative controls: with a cut R = 3 the checker reports landings in Y, and with a wrong w at phase 5 it rejects 320 representatives.

6.4 Endgame by locality (Lemma L)

Digit positions and value. In a zone, D0 and D1 are the digit units. The digit position of a unit is the number of digit units below it. V(Z) is the sum of 2^(position) over the D1 units; P, S1, SP and W carry no weight. Above the top of a zone the blank reads as D0 digits.

Members. Let s = (Z, D, j) be a closed-system state, the representative, and let R ≥ 5 and Δ ≡ 0 (mod 2^R). A state s′ = (Z′, D′, j′) is an (R, Δ)-member of s if:

• (M1) j′ − j = D′ − D = Δ. Then the feeds differ by c′ − c = Δ at every step, since p depends on j mod 8.
• (M2) Z = X·Y and Z′ = X·Y′, where X runs up to and including the digit unit at position R − 1, and Y, Y′ consist of digit units only.
• (M3) V(Z′) − V(Z) = Δ.
• (M4) At every step, the member's feed c′ is at least T0, a bound fixed with the representative.

Lemma L (locality). Run the representative with κ_0 = 1. At the start of step t, set the cut r_t = R + min(0, ν2(κ_t)) digit units. Suppose that at every step:

• (H0) every non-digit unit of Z has at most r_t − 1 digit units below it. So it lies in X, the part of Z up to and including the digit unit at position r_t − 1.
• (H1) every shift landing in the step (wall shifts and the absorption shift), on a digit or on a non-digit unit alike, is on a unit with at most r − 1 digit units below it. Such a unit lies at or below a digit unit of X, so every landing is on a unit of X.
• Here r starts at r_t and drops by one at each landing on a D1, because that D1 becomes an S1 and X has one digit unit fewer.
• (H2) T0 ≤ c, and after the first T0 carries of the step, the zone has no unit other than D0, D1 and P.

(H0) and (H1) are meant in this strict sense: "at most r − 1 digit units below", not "at most r". The checks S10 and S11 test exactly this, for digit and non-digit targets alike.

Update κ_(t+1) = (κ_t / 2^a + 1) / 2^b, where a counts the landings on a D1 among the first T0 carries and b counts the landings on a D1 at the absorption shift. Suppose also that the representative reaches a canonical state C(β) with κ = 1.

Then every (R, Δ)-member reaches C(β + Δ/32) at the same step. Its run has the same units below the cut at every step, the same zone walls and the same landings. In particular, it has no zone wall alive at an absorption and no hit if the representative has none.

Proof.

1. Upward flow. In the Inc recursion each unit's row depends only on its own head, and the nested arrivals act on the units above it. A shift lands on the first non-D0 unit above its emitter.

• So if no shift lands in Y, then inc^n(X·Y) = X_n · inc^(e_n)(Y), with X_n and e_n depending only on X and n. This is an induction on the Inc derivation.

2. The first T0 carries. Both runs get at least T0 carries (H2, M4). By item 1 and (H1), X evolves identically in both runs, and Y and Y′ get the same carries.

• All wall firings and all drops of the step happen here. After T0 there is no wall left, so there are no more shifts.
• The bottom unit, once the leading P units are dropped, is a digit and stays a digit, so there are no more drops either.

3. The rest of the carry phase. A P passes carries, so dropping leading P units commutes with feeding. The carry phase is therefore inc^m, where m is the least m ≥ c with m = c + 3A(m), and A(m) is the number of P units dropped after m carries.

• A is constant from T0 on, so m = c + 3A and m′ = c′ + 3A = m + Δ.
• After T0, X is a counter of r′ = r_t − a digit units (P units pass carries) that receives m − T0 or m′ − T0 carries.
• Since Δ ≡ 0 (mod 2^R) and r′ ≤ R, X ends the same in both runs, and Y′ gets exactly Δ / 2^(r′) more carries than Y.

4. Absorption. The shift lands in X (H1), on the same unit in both runs.

5. Values. The difference H = V(Z′) − V(Z) has all its weight above the cut.

• A landing on a D1 below the cut removes one digit position, so everything above moves down one position: H → H/2.
• Identical carries change V and V′ by the same amount. The Δ extra carries add Δ.
• So H_(t+1) = (H_t / 2^a + Δ) / 2^b, which is H_t = κ_t·Δ.

6. The next step. X agrees in both runs. Y′ − Y, as numbers, is H_(t+1) / 2^(cut), which is divisible by 2^(ν2(H_(t+1)) − cut).

• So the two zones agree on every digit position below ν2(H_(t+1)) ≥ R + ν2(κ_(t+1)) ≥ r_(t+1).
• With (H0), every non-digit unit lies in the new X. So (M1)-(M3) hold again with the cut r_(t+1) and the same Δ.

7. The end. With κ = 1, V(Z′) = V(Z) + Δ. Z = C(β) has V = 30 + 32(β+1), and the two zones agree below digit position R ≥ 5.

• So Z′ = S1 D0 D1⁴ bin(β + 1 + Δ/32). Also D′ = j′ − 1, and j′ ≡ 17 (mod 32).
• Walls and landings lie in X, so they are the same in both runs. ∎

The locality check (S10) runs a representative and checks (H0)-(H2), κ and the canonical end at every step. A failed hypothesis fails the run.

The endgame instance. Take a class k ≥ 41 and an upper part U ≥ 1, and start from VF_4(k, U) (or VF at the next offset if that one is phase 3).

• The representative is k0 = 2^16 + (k mod 2^16), with o = 3 and the upper part compressed to 3·2^56.
• The member is the real state. Then Δ = U·2^(k+5) − 3·2^56 + (k − k0) ≡ 0 (mod 2^16).
• (M3) holds because w has slope 1 in off and both states have L = 4.
• (M4) holds with T0 = 2^19, because c′ ≥ 2^45 when k ≥ 41.

S10 runs all 65,536 residues. The 65,534 with ν2(k0+9) ≤ 14 satisfy Lemma L and reach the canonical state, with landings at digit ≤ 15. The 2 residues with ν2(k+9) ≥ 15 go to §6.5.

So for ν2(k+9) ≤ 14, VF_4(k, U) reaches a canonical state with no wall alive and no hit, for every U: the compressed and the real upper part alike.

6.5 Nested marker, plant, and the class recursion

Write k + 9 = s·2^v with s odd and v ≥ 9. Let off′ = off − (k+9), S = s + U·2^(k+5−v) and Q = (S−1)/2.

Nested range v ≤ 600 (Lemma L). Start from VF at off′ = 12 (marker height 3, phase 4). Note S ≡ s (mod 4).

• The representative is s0 ∈ {1, 3}, with U = 3 and the upper part compressed to 3·2^(v+64).
• The members are every class k with ν2(k+9) = v and s ≡ s0 (mod 4), and every U. So R = v + 2, and Δ = U·2^(k+5) − 3·2^(v+64) + 2^v(s − s0) ≡ 0 (mod 2^(v+2)).
• T0 = 2^(v+5) ≤ 2^(k+4) ≤ c′.

S10: 1,182/1,182 representatives (every v in 10..600, both s0) satisfy Lemma L. The highest landing is digit v+1, below the cut v+2. So in this range the outcome depends only on S mod 4.

Plant lemma (Lemma P). Let v ≥ 9 and n = v − 3, and let S = 2Q + 1 ≥ 3 be odd. At off′ the step number is j = S·2^v − 64 + off′. Write [x]_n for the n-digit word of x, where 0 ≤ x < 2^n.

The start is the value form at off_end(k) = k + 21, in phase 4 with marker height 3, where k + 9 = s·2^v. There Vtot = Ω + s·2^v − 24 = S·2^v − 24. The run from it passes through:

off'  zone                                              D - j
12    S1 P P D0 D0 D0 P [2^n - 3]_n bin(2Q)               -4
13    D0 D0 D0 SP [2^n - 3]_n bin(4Q + 1)                 -2
14    D0 S1 D0 P [2^n - 3]_n D0 P bin(2Q - 1)             -3
15    S1 P D0 P [2^n - 5]_n D0 P bin(4Q)                  -4
16    S1 P [2^n - 6]_n D0 P bin(8Q + 2)                   -3
17    S1 [2^(n-1) - 3]_(n-1) D0 P bin(16Q + 6)            -2

There is no zone wall alive at an absorption and no hit. The feed is c = S·2^v + (off′ − 64 + d + p), where d is the D − j of the row.

Proof.

• 12 → 13. c = S·2^v − 8. The S1 absorbs one carry and becomes P. With the P P above it the bottom is three P units, which drop (A = 3, +9 carries).
• The digits receive S·2^v. Their value was 8(2^n − 3) + 2Q·2^v, and it becomes 2^(v+1) − 24 + Q·2^(v+2).
• That reads D0 D0 D0, then [2^n − 3]_n, then bin(4Q + 1).
• The shift crosses the three D0 units and lands on the marker P, which becomes SP: a zone wall is born at the absorption.
• 13 → 14. c = S·2^v − 6, and nothing drops. The three low digits pass every 8th carry to the SP.
• The 8th carry makes it W. The 16th fires it: its three carries turn [2^n − 3]_n into [0]_n and carry one into bin(4Q + 1), giving bin(4Q + 2).
• Its shift crosses the n zero digits and the 0 at digit v, and lands on the D1 at digit v + 1, which becomes S1. The wall is now P.
• The remaining c − 16 = S·2^v − 22 carries leave the low digits at 2 and pass S·2^n − 3 up. Those leave [2^n − 3]_n and pass 2Q up, which leaves the digit at v at 0 and passes Q to the new S1.
• The S1 absorbs one of them and becomes P (Q ≥ 1): this is the new marker. The other Q − 1 give bin(2Q − 1).
• No wall is left before the absorption, and the shift lands on digit 1.
• 14 → 15. c = S·2^v − 5, and nothing drops.
• The first two carries turn digit 0 back to 0 and the S1 into P.
• The remaining S·2^v − 7 leave the two low digits at 1 and 0, the word at [2^n − 5]_n, and the digit below the new marker at 0. They pass S across the new marker, giving bin(4Q).
• The shift lands on digit 0.
• 15 → 16. c = S·2^v − 6. The S1 becomes P, and with the P above it the bottom P P drops (A = 2, +6).
• The digits receive S·2^v − 1: digit 0 becomes 1, the word becomes [2^n − 6]_n, and 2S crosses the new marker, giving bin(8Q + 2).
• The shift lands on digit 0.
• 16 → 17. c = S·2^v − 4. The S1 becomes P and the bottom P P drops (A = 2, +6).
• The digits receive S·2^v + 1: the word becomes [2^n − 5]_n, and 4S crosses the new marker, giving bin(16Q + 6).
• The shift lands on digit 0 of the word, which is odd, and leaves [2^(n−1) − 3]_(n−1).

The only zone wall is the SP born at 12 → 13. It fires inside step 13 → 14, before that step's absorption, and its shift lands on a D1. So no wall is alive at an absorption and nothing is hit. The steps need n ≥ 6 (so the words stay in range) and Q ≥ 1. ∎

S11 checks the six forms against the closed system on 3,000 random (v, S), with v up to 2,998 and S up to 600 bits. All 3,000 match.

Identification. The off′ = 17 state is VF(v − 10, S·2^v, 17) at level 2:

• the heads are S1@0;
• L = (v − 10) + 24 − 17 = v − 3 = n;
• Vtot = (2^(n−1) − 3) + (16Q + 6)·2^n = S·2^v − 3 − 3·2^(v−4);
• D = j − 2.

So K′ = v − 10 and U′ = 32S, since S·2^v = 32S·2^(K′+5). This is algebra on the two closed forms, and S11 also checks it on every plant instance.

Class recursion (well-founded induction on K). Let E(K) say:

for every upper part U ≥ 1, the run from the value form at off_end(K) (that is VF_4(K, U), or VF_3(K, U) in phase 4) reaches a later canonical state, with no zone wall alive at an absorption and no hit.

We prove E(K) for every K ≥ 41 by strong induction on K. Let v = ν2(K+9).

• v ≤ 14: the endgame instance of §6.4. No induction hypothesis is used.
• 15 ≤ v ≤ 600: since v ≥ 3, off_end(K) = K + 21 is off′ = 12, the start of the nested range above, which finishes it. No induction hypothesis is used.
• v > 600: the start is off′ = 12. Lemma P takes the run to off′ = 17, which by the identification is VF(K′, 32S·2^(K′+5), 17) at level 2, with K′ = v − 10.
• Lemma VF (level 2) carries it to the value form at off_end(K′), with upper part U′ = 32S.
• Since K′ ≤ log2(K+9) − 10 < K, the induction hypothesis E(K′) finishes it.

Base. Every K with ν2(K+9) ≤ 600 is settled without the hypothesis. The first K that uses it is K = 2^601 − 9.

A smaller split (the one the .v uses). Lemmas P and VF (level 2) hold for every v ≥ 12. So the recursion can hand over to the induction hypothesis from v > 50 instead of v > 600, since then K′ = v − 10 ≥ 41 and E(K′) is in range.

• The endgame then needs only the cut R = 12, which covers ν2(k+9) ≤ 10: 4,094 residue runs (S10 runs all 4,094).
• The nested range shrinks to 11 ≤ v ≤ 50: 80 representative runs.
• Together with the small classes this is 4,094 + 80 + 655 representative runs.

6.6 Small classes (Lemma L)

Take k = ν2(b+2) ≤ 40, so b + 2 = o·2^k with o odd, and fix o mod 16 = o0.

• o = o0. This is a single block, run directly from C(b).
• It is not a member of the others: for o = 1 the S1 marker at height k+6 gets no carry in its first step, but it does for every larger o.
• o = o0 + 16t with t ≥ 1. These are members of the representative o0 + 16, which has the smallest feed of them, so T0 = c.
• The cut is R = k + 9.
• Δ = 32·2^k·16(t−1) satisfies (M1), and (M3) holds because V(C(b)) = 30 + 32(b+1).

S10: 327/327 direct runs and 328/328 representatives satisfy Lemma L and reach the next canonical state, with no alive wall and no hit.

6.7 Assembly (Theorem B)

Fix b, and let k = ν2(b+2).

• k ≤ 40: §6.6.
• k ≥ 41: Lemma E (§6.1) and Lemma VF at level 1 (§6.3) carry C(b) to the value form at off_end(k). Then E(k) of §6.5 applies. It is proved by well-founded induction from Lemma L, Lemma P and Lemma VF at level 2.

So Theorem B holds. Each piece is defined at every step and has no zone wall alive at its absorptions. So by Lemma Z0 (with Lemma Z1 for the absorption shifts) the zone never has a hit.

Random huge b give an independent check (S8). For every k ≤ 130, with b < 2^400, the run from C(b) reaches C(b + 1 + ⌊(k+9)/32⌋) (the observation after Theorem B), with 0 alive walls and 0 hits.

7. Invariant, coverage, progress, halting unreachable

Invariant. The induction runs over the left records n ≥ 0, counted from the step-203,465 record. It carries one ghost number J, the number of absorptions so far. Indices are in the U_0 frame. Inv(n, J) says:

1. Gadget. The tape is 0^inf <q_n G_n U_n 0^inf, where (q_n, G_n) is row n mod 8 of the table in §4. U_n starts at index base(n mod 8): that is 0 at XC, XD, XE, ZD, ZE and −1 at YC, YD, YE.

2. Live walls. They are walls J, J+1, …, born(n) − 1, where born(n) = 6 + 8⌊n/8⌋ + 3·[n mod 8 ≥ 3] + 4·[n mod 8 ≥ 6] counts the births so far.

3. (b) Birth data. Wall w has the fixed birth data (b_w, s_w): from U_0's table (indices 32, 20, 12, 7, 3, 1 and states W W W SP W SP) for w < 6, and otherwise the phase table of §4 at phase (w − 6) mod 8.

• H_w is 0, 36, 6 or 9 as in §5; U_0's SP at index 1 plays the ZE wall (H = 9).

4. (c) Carries. No triple is in progress at a record, and the youngest wall has R = 0. Walls born earlier satisfy

R_(w−1) = H_(w−1) + 3*floor((R_w + s_w)/2).

Wall w sits at b_w + ⌊(R_w + s_w)/2⌋, and it is W if R_w + s_w is odd, SP if even.

5. (d) Zone feed. The zone has received m carries since absorption J − 1, where

m = 3*floor((R_J + s_J)/2) − [2(43 + D_J − b_(J−1)) − s_(J−1) − H_(J−1)] (J ≥ 1) m = 3*floor((R_0 + s_0)/2) (J = 0)

and 0 ≤ m < N_J. Here D_J and N_J are the closed system's D and carry count at its step J (N_0 = 33).

6. (a) Zone. Let CS_J be the closed-system zone at the start of its step J, started from Z_1 (CS_0 = D0 D0 D1⁴, D_0 = 0).

• The zone Z_n is inc^m(CS_J) with its leading P units removed; say A_cur of them.
• The zone bottom is z = 43 + D_J + A_cur.

7. Conveyor. Every index from base to z − 1 is P, except the live walls at the positions in item 4.

8. No hit in the orbit. The closed-system orbit up to step J + 1 has no zone wall alive at an absorption and no hit (Theorem B, Lemmas Z0 and Z1; the S7 base run for steps 1..17).

Inv(n, J) fixes the configuration. Items 2-7 determine U_n from (n, J) alone. For instance, a top wire with one P too few violates item 6 or 7.

S6 builds U_n from (n, J) and compares it with the unit-level run, which equals the machine at every S5 record. All 1,201 records match, over 150 cycles and 8 level-ups. All 1,203 perturbed words (one P less in the top wire, one P more, or the top wall moved up one unit) match no reconstruction for any J′ in J−4..J+4.

Closure: Inv(n, J) ⇒ Inv(n+1, J′), with J′ = J plus the number of absorptions in the step.

• Window. Lemma N runs the window from record n to n+1. Its contacts with R are arrivals (Theorem U) and pops of a P (Lemma C1). Item 1 follows, and the excursion sends 3 carries into R per W-rule use.
• Carries flow upward. By item 7 every unit between the bottom of R and the youngest wall is P, so the nursery's carries all reach the youngest wall.
• Between consecutive live walls there are only P units, so wall w − 1 receives exactly the 3 carries per firing of wall w. That keeps item 4 at the next record.
• Births. After an excursion the new walls are placed below the old youngest wall (§4, placement table). They have R = 0, and the old youngest has received exactly H carries (36, 6 or 9). That is item 4 with H.
• Top wall J. All its emissions go into its wire and then the zone, since the wire is P (item 7). A P passes carries, so the zone receives them as inc on Z, and leading P units become wire. Item 6 is kept with m increased, and z increases by the drops.

Absorption. By item 4 the top wall fires from z − 1 exactly when 3⌊(R_J + s_J)/2⌋ − E_then = 3(z − b_J) − E_then. Here E_then is the bracket in item 5, the carries wall J had emitted at absorption J − 1. Substituting z = 43 + D_J + A, this is m = 3A + D_J + p(J mod 8) = c + 3A, which is the closed system's stopping value.

• At each earlier triple boundary m the wall has fired f times and sits at b_J + f ≤ z(m) − 1, where z(m) = 43 + D_J + A(m) is the zone bottom then.
• So m = 3f − E_then ≤ 3(z(m) − 1 − b_J) − E_then = c + 3A(m) − 3 < c + 3A(m). No earlier triple boundary is a fixed point.
• No fixed point lies between triple boundaries. From c + 3A = 3(z − b_J) − E_then we get c ≡ −E_then (mod 3).
• Wall J had emitted E_then = 3f_0 − r carries at absorption J − 1, with r ∈ {0, 1, 2} carries of its triple still to come, so −E_then ≡ r (mod 3).
• The triple boundaries of the interval are exactly the m ≥ r with m ≡ r (mod 3). Every fixed point has m ≡ c ≡ r (mod 3), and m ≥ c ≥ 47 > r, so it is a triple boundary.
• So the real absorption comes exactly at the least fixed point m = c + 3A(m) that the closed system computes. Its shift is the closed system's absorption shift: the first non-D0 unit at or above z.
• After it, wall J + 1 is the top wall. In-flight carries of its triple go to the zone, and item 5 holds for J + 1, because R_J at that moment is 2(z − b_J) − s_J = H_J + (emissions of wall J+1).

This is the Lemma T algebra of §5, run from the invariant clauses instead of from the history of the run.

• No hit. Every arrival in the step is defined. In the conveyor this is Lemma C2. In the zone the arrivals are steps of the closed-system orbit, which has no hit (item 8; Theorem B and Lemmas Z0, Z1). The recursion is finite by Lemma U-term.
• Item 8 moves from J + 1 to J′ + 1 by Theorem B.

Coverage. Inv(0, 0) holds by §8. Inv(n, J) ⇒ Inv(n+1, J′) as above.

Progress. Each record step is a finite window run plus finitely many arrivals, and each arrival terminates (Lemma U-term). The step ends on a new left cell. So there are infinitely many records, strictly increasing in time.

Halting unreachable. The only undefined transition is A1.

• The initial segment (§8) is a finite run without A1 (S4).
• The 8 window runs are finite runs without A1 (S5).
• In every unit lemma used (D0, D1, P, S1, SP, W and the first-cell-0 rule), state A reads only 0.
• No stacked head ever arises, because there is no hit.

Conclusion. The machine never halts. Every lemma in the chain is proved: the machine layer, the conveyor and the invariant (§2-§5, §7), and Theorem B for the zone (§6.7).

8. Initial segment

0^inf A> 0^inf   -->(203,465)   0^inf <C G_X U_0 0^inf      (<C reads the last 0 of 0^inf, just left of G_X)
G_X = 111111 0000 11 0000 11 000
U_0 = P SP P W P^3 SP P^4 W P^7 W P^11 W P^10 D0 D0 D1 D1 D1 D1

This is a finite run (S4 compares the gadget cells as well as the unit word). The state at the record is C. The conveyor of U_0 has 43 units, and its zone D0 D0 D1 D1 D1 D1 starts the closed system (§5).

Before step 203,465 there is nothing to prove: it is a finite run that does not halt.

9. The proof in Coq

The .v follows the argument above, with a few changes of route. Each one makes a statement easier to formalize; none changes the mathematics.

Hits are not unit words. The .v's unit type has only the six L_gap units. Its shift returns no word when it would land on S1, SP or W, and Inc has rows only for the six units.

• So a hit, or a head without a row, makes the carry relation fail, and the stacked-head rows of §2.2 are not needed.
• Lemmas Z0 and Z1 become unnecessary as separate lemmas. The .v proves that every step of the closed-system orbit exists (zone_forever, CS_next), and an existing step has no hit.
• Lemma U-term likewise becomes the statement that the pops of every record step exist, which is what AbsDefined asks for.

Reduction. nonhalt_of_abs combines init with busycoq's progress_nonhalt_cond. Here init is the 203,465-step run, checked by busycoq's cconfig_evstep_dec_spec and vm_compute.

The progress relation is Reach on pairs (record type t, unit word U). Its step is the lemma window:

Pops (rk t) U U'   ->   rcfg t U  -->+  rcfg (rnext t) (rF t ++ U')

Window runs. wrun is an executable runner on a finite window, with the rest of the tape an opaque unit word touched only by the W rule (Inc3Pop). wrun_spec proves it sound, and the 8 runs of Lemma N are checked by computation inside window.

Closed system. cs_step states one step of §5 as a relation, with the least fixed point written out: m = D + p(j) + 3A, and no smaller m′ is a fixed point. csf is an executable step with csf_sound, and C0_reach runs it from Z_1 to C(0) at j = 17.

Lemma L as cut steps and families. The .v does not state Lemma L as a lemma about two runs. It proves its items for one step (cutstep):

• the first T0 carries act on the part below the cut alone (upward flow, IncX_flow, XN);
• after that the low part is a clean counter (XN_clean), and the absorption shift lands below the cut.

An affine family (X, y, ay, D, j, aD) stands for the states with zone X ++ bin(y + ay·u), D + aD·u and j + aD·u, for every u ≥ 0. The runner frun steps a family as a whole, and frun_sound proves that one successful run covers every member. The representative runs of §6.4–§6.6 are family runs checked by vm_compute:

• small classes: 327 direct runs and 328 families (sc_all, small_classes);
• endgame: 4,094 families, k mod 2^12 with cut 12 (eg_all, endgame);
• nested range 11 ≤ v ≤ 50: 80 families, s mod 4 with cut v + 2 (ns_all, nested).

This is the smaller split of §6.5, so E_low covers ν2(K+9) ≤ 50, and EK uses the plant, VF2 and the induction hypothesis above that.

Lemma VS. astep is one closed-system step with a concrete low part and an arbitrary counter word above the cut (Lemma L′). vs_gen is the descent step symbolic in Ω, off and the marker height. It is checked by computation on the 12 entry rows (en_all) and on 256 × 5 phase classes, off mod 256 times L ∈ {5, 6, 7, 8, ≥ 9} (ph_all). VF1 and VF2 are the descents at the two levels.

Lemmas E and P. The steps of §6.1 and §6.5 are E1 to E3 and P12 to P16, proved on closed forms with lia and nia. LemmaE and LemmaP chain them.

E_id and P_id are the identifications with the value forms. The .v states Lemma P for n ≥ 7, which is all the recursion needs.

Conveyor and invariant. The .v does not write Inv(n, J) with the explicit formula for m. It describes the word above a position p as a relation WdR w p R u, by recursion on the wall number w, oldest wall first:

• if wall w is live, u is a run of P units, then the wall (SP or W by the parity of R + s_w), then the word above it;
• if wall w is absorbed, u is the zone of the current interval seen from p (ZoneR): a reachable closed-system state, m carries into its step, and no fixed point below m;
• the zone of interval 0 is the counter bin(60 + m) (Zone0).

The one-carry lemma cascade is proved by induction on w. Its cases are an SP turning into W, a W firing and moving up, and the top wall being absorbed exactly at the least fixed point. The last case uses the bracket of Lemma T (bracket, bracket_small, wdata_period), here in a frame shifted by one: positions are U_0 indices plus 1.

The record invariant RInv t U says that U is WdR of its youngest wall, at the record's base position, with the birth phase matching the record type. RInv_step proves closure for all 8 record types, RInv_U0 gives the start, and AbsDefined_proof then gives nonhalt.

10. Numerical checks

These are evidence only; the result rests on the .v. Every claim of §1–§8 was also tested numerically, with simulators that are independent of the .v.

In S12 the orbit has 3,509,921 absorption shifts on a D1 and 690,078 on a P, and 690,078 wall shifts on a D1 and 480,973 on a P. Nothing else occurs.

Beyond these, third-level runs go to v = 16,385, and real uncompressed runs at k = 32,759 agree with the forms of §6.

11. Rule table (summary)

The block lists every rule the proof uses, with its parameters, its domain and how it is proved. Sections 2–6 give the exact statements and the proofs.

(*  machine layer (section 2): exact tape rewrites, proved by induction or by oracle simulation
  SR    B> (11000)^n        --> (10111)^n B>         5n        n >= 0, ind n
  SR6   B> (111000)^n       --> (100111)^n B>        6n        n >= 0, ind n
  KB    B> (1000)^n         --> (1111)^n B>          4n        n >= 0, ind n
  SL'   (10111)^n <C        --> <C (11000)^n         5n        n >= 0, ind n
  SL    (11110)^n <C        --> <C (00011)^n         5n        n >= 0, ind n
  KC    1^n <C              --> <C 0^n               n         n >= 0, ind n
  EdgeL 0^inf <C            --> 0^inf 1 0 B> 1       4
  Z     B> 0 x              --> <C 1 x               1         every x (first cell 0: D0, S1, SP, the blank)
  D1    B> 1000 r           --> <C 0000 inc(r)       8 + s     oracle, one arrival on r
  P     B> 11000 r          --> <C 11000 inc(r)      10 + s    oracle, one arrival on r
  W     B> 111000 r         --> <C 11000 . shift(inc^3 r)   34 + s1 + s2 + s3   oracle, three arrivals on r
  Thm U l B> w 0^inf        --> l <C inc(w) 0^inf    exact     every l, every w with inc(w) defined; ind on Inc
  carry model (section 2.3): inc on unit words, one carry; a W fires on every second carry it receives
  nursery (section 4): 8 window runs  0^inf <q G R  -->  0^inf <q' G' F (pop o inc^3)^k R,  k = 0, 0, 3, 0, 0, 12, 0, 2
  conveyor (section 3): C1  inc^3 x starts with P if x starts with P, S1, SP or W;  C2  no hit below the zone
  top (section 5): Lemma T  N_j = 3A_j + D_j + p(j mod 8), p = (47,48,48,47,48,47,48,47);  closed system (Z, D, j)
  zone (section 6): Z1 the absorption shift never lands on S1;  Z0 no alive wall => no hit;
                    C(b) --> C(b') with b' > b, no alive wall (Theorem B: Lemmas E, VF, L, L', P, class recursion)
*)

AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).