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

1RB---_1LC1RE_1LD0LC_1LE1LC_1RF0RE_1RA0RB: never halts (informal proof, complete; Rocq formalization not started)

Machine

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

The start is 0^inf A> 0^inf. The machine halts only if state A reads a 1. Every rule of this proof is an exact run in which state A reads only 0 (§7, "Halting unreachable").

Rule table (summary)

The block below 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)
*)

0. What the machine does

The tape 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 (an "arrival"). The carry runs through a word of short blocks called units until a unit absorbs it, and 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. It touches the unit word only by acting as a wall itself. The walls ride a conveyor of P blocks, in order, and at the right end they are absorbed one by one into a zone. The zone is a binary counter with a few marker units.

The machine can halt only if a wall's "shift" (a one-cell lattice offset that a wall leaves behind when it moves) 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).

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.

name cells head h role
D0 0000 (0 digit) counter digit 0
D1 1000 ε counter digit 1
P 11000 1 pass block (wire)
S1 01000 0 shifted digit
SP 011000 01 wall, state W0 (absorbs the next carry)
W 111000 11 wall, state W1 (forwards 3 carries)

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 (for example ... D0 bin(q) with q = 0, where bin(0) is the empty word) stands for its normal form, with those D0 units removed.

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 (001, 011, 111, 101, 0111, 1111, 0101, 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 (S1)

(*  sweeps; all proved by ind n with one IH use; checked for n = 0..40 and 10-40 random n in 100..5000, random context
  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 (S2: proofs by oracle simulation)

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, where 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. check_proof.py S2 runs all of them, and the chains are printed below.

(*  unit lemmas: unit . r  -->  unit' . r'          (r' = result of the f 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, §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. Its next carry meets head 10, which has no unit rule (oracle: 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) (S3)

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 earlier version inducted on the cell length of w. That fails: 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). ∎

The earlier proof claimed that the region above the old top holds only digits. That is false: one arrival on W W SP gives P SP P SP D0 D0 D1 (237 machine steps), with an SP above the old top. The induction on walls does not need that claim. S3 checks the wall count bound on every L_gap word it runs (walls(inc w) ≤ walls(w)).

Check S3 compares the machine and inc, cells and exact step counts, on every unit word of up to 4 units over 14 unit kinds (quick mode: 3 units) and on 20,000 random words with long P runs: 0 mismatches. A RecursionError in the model now counts as a failure.

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. 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.

Lemma C2 replaces the earlier "interior wires" Lemma I. That statement was wrong: a W directly followed by S1, SP or W is harmless.

4. The nursery (Lemma N; proved by a finite window computation, S5)

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. By Lemma C1, 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 3e8 (quick, 522 transitions) or 2e9 (full, 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 earlier attempt failed. It looked for a static cell boundary and found none. That is right: 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, and 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⌋:

birth record previous lowest wall (b, s, H) its index newborn indices
after YE last XE wall (−1, W, 36) −1 + ⌊37/2⌋ = 17 ≤ 10
after ZE last YE wall (0, W, 6) 0 + ⌊7/2⌋ = 3 1
after XE the ZE wall (1, SP, 9) 1 + ⌊9/2⌋ = 5 ≤ 2
first XE after step 203,465 U_0's SP (1, SP, 9) 1 + 4 = 5 ≤ 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 (180 quick / 450 full).

5. The top relation (Lemma T; proved by a flux identity, S6) 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.

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 (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. Round-1 review read a level-up as shifting the birth index against j. With FIFO that pairing is fixed; what shifts is 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 (60 cycles quick, 150 full: 474 / 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; - the stored machine replay (deepen5/results/N_final.json, 4,820 absorptions to 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).

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. Check S12 classifies every shift of the closed-system orbit from Z_1 to j = 32·131,250 (full; 32·20,000 quick). Every one lands on a D1 or a P. S12 also tests Lemma Z1 directly: - exhaustively, on every zone of at most 6 units over D0, D1, S1, P, SP and W with every feed c = 1..40 (46,655 zones, 1,866,200 carry phases; quick: 5 units, c ≤ 32); - on 200,000 random zones with any number of walls (quick 20,000).

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 (full mode; quick mode b < 20,000). 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.

Status: every piece is proved. - 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).

The symbolic engines of earlier stages (entry, descent, plant) are no longer used by the proof. check_proof S9 still runs them as an independent cross-check.

6.1 Entry: off 17 → 20 (Lemma E; proved by hand, S11)

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, 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. - The constructor of the checks builds the forms in exactly this order, and S11 compares whole unit lists.

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.

The 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 (proved: Lemma L′ plus finitely many one-step representatives, S11)

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. (The class recursion uses only v > 600. 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.)

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

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; proved, S10)

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. 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. Such a unit lies at or below a digit unit of X, so every landing is on a unit of X. - (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 (locality.py, vf.py) 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. ∎

scripts/proof3/locality.py 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.

locality.py endgame 16 56 19: 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. That took about 1 minute (S10 full; quick reruns R = 8 and checks the stored R = 16 result). 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. The earlier "k mod 2^R" argument, and its unchecked compression, are replaced by this.

6.5 Nested marker, plant, and the class recursion (S10, S11)

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; proved). 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′.

locality.py nested 600: 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. This is the "depends only on S mod 4" claim, now a lemma. S10 full reruns it in about 1.5 minutes; quick reruns v ≤ 60 and checks the stored result.

Plant lemma (Lemma P; proved by hand, S11). 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 level-ℓ 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.

Checks beyond the proof. Third-level runs to v = 16,385 (deep.py). Real uncompressed runs at k = 32,759 (realdeep.py).

6.6 Small classes (Lemma L; proved, S10)

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).

locality.py smallk 40 4: 327/327 direct runs and 328/328 representatives satisfy Lemma L and reach the next canonical state, with no alive wall and no hit. (S10 full runs k ≤ 40, quick runs k ≤ 12.)

6.7 Assembly (Theorem B)

Fix b, and let k = ν2(b+2). - k ≤ 40: §6.6. This is proved. - 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 ≤ 60 (quick) or ≤ 130 (full), with b < 2^200 or 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. Round 2 showed that the old invariant, with its existential wall data, admits a top wire with one P too few. That configuration violates item 6 or 7 here.

scripts/proof3/invariant.py builds U_n from (n, J). S6 compares it with the unit-level run, which equals the machine at every S5 record: - Quick: 481 of 481 records match: the walls, every R, m and the zone. 483 of 483 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. - Full: 1,201 of 1,201 records match, over 150 cycles and 8 level-ups. 1,203 of 1,203 perturbed words are rejected.

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. - 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 checked by direct simulation (S4), which now 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. Evidence and gaps

piece statement status check
sweeps §2.1 proved (ind n, one IH) S1: n ≤ 40 exhaustive, random n ≤ 5000
unit lemmas §2.2 proved (finite oracle computations) S2
Theorem U §2.3 proved (induction on the Inc derivation) S3: 2,743 (quick) / 38,415 (full) exhaustive words + 2,000 / 20,000 random, cells and steps
termination Lemma U-term proved (induction on the wall count) S3: walls(inc w) ≤ walls(w) on every L_gap word run
Lemmas C1, C2 §3 proved (4 cases) S5
Lemma N §4, nursery cycle proved (8 finite window runs, side condition c ≥ 42) S5: the proof run; cross-check at every record to 3e8 / 2e9 (cells, state, exact steps)
FIFO placement §4 proved (4-row table from H) S6: every birth
Lemma T §5, top relation; absorption at the least fixed point proved (flux identity, FIFO; fixed points are triple boundaries since c ≡ r (mod 3)) S6: identity and T for every j ≥ 1 of a 60 / 150-cycle run that equals the machine at every S5 record; r_j ∈ {0, 1, 2} and c_j ≡ r_j (mod 3) at every absorption; stored replay to 1.93e11
initial segment §8 proved (finite run) S4
invariant §7 proved closed (explicit in (n, J); closure = Lemma N + Lemma T algebra), given Theorem B S6: reconstruction equals the run at 481 / 1,201 records; all perturbations rejected
Lemma Z1 the absorption shift never lands on S1 proved (last-event argument on the counter below the S1) S12: every zone of ≤ 6 units, c ≤ 40 (1,866,200 phases); 200,000 random zones, any walls; c = 0 negative control
Lemma Z0 no alive wall ⇒ no hit proved (one wall at a time, Z1 for absorptions) S12: every shift of the orbit from Z_1 to j = 32·131,250 lands on D1, P or the blank; S7: every absorption shift lands on D1 or P
canonical base C(b), b ≤ 131,249 proved (finite run of the closed system) S7
entry §6.1, Lemma E proved (3 steps by hand on closed forms, q ≥ 1 and q = 0) S11: 2,000 random (k, o), 405 with o = 1
value form §6.2-§6.3, Lemma VF proved (Lemma L′ + 24 + 256 + 1,024 one-step representatives at R = 8, induction on off; level 1 every k ≥ 41, level 2 every v ≥ 12) S11: every representative; 68,308 + 62,723 states of real chains (both levels, v from 12); 2,969 random members
locality §6.4, Lemma L; §6.3, Lemma L′ proved (upward flow + counter arithmetic + value bookkeeping; L′ lets one P sit above the cut) hypotheses checked by locality.py / vf.py in every representative run, in the strict reading (every non-digit unit and every landing target has at most r − 1 digit units below it)
endgame §6.4 proved (Lemma L, all 65,536 residues mod 2^16) S10: R = 8 (quick) / R = 16 (full, rerun)
nested range §6.5, v ≤ 600 proved (Lemma L, S mod 4) S10: v ≤ 60 (quick) / v ≤ 600 (full, rerun)
plant §6.5, Lemma P proved (5 steps by hand on closed forms, every v ≥ 9) and identification (algebra) S11: 3,000 random (v, S), v ≤ 2,998
old engines entry, descent, plant no longer used by the proof; kept as a cross-check S9
recursion §6.5 proved (well-founded induction on K, base ν2(K+9) ≤ 600) —
small classes §6.6 proved (Lemma L, o mod 16, plus direct runs) S10: k ≤ 12 (quick) / ≤ 40 (full)

What is still open. Nothing in the informal argument. The next steps are Dennis's Checkpoint B read and the Rocq formalization (§10).

How the last gap was closed (VF round). - VF. Lemma L′ is Lemma L for one step, with one P allowed above the cut. A P passes carries, weighs nothing, is never landed on (H1), and never reaches the bottom while X keeps a digit unit. - So each descent step transfers from a representative to every member whose digits agree below the cut. That includes members with a different marker height. - The value bookkeeping (H/2^a + Δ)/2^b gives exactly the next form's difference, because w has slope 1 (2 at phase 3, which comes with a = b = 1 on the way out). - This removes the growth conditions of the old descent engine: the value form is the definition, and nothing about the size of the low word is used. - Entry and plant. These are 3 and 5 steps of binary addition with a few unit events at fixed places, done by hand on the closed forms.

Not a cryptid. 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.

10. Lemma plan for Rocq (no template applies)

The nearest template is none: CounterCmp_v1 TM1 does not apply (11 of 12 transitions differ). The plan below is a sketch of size, not a schedule.

  1. Units and arrival (routine). Use an inductive unit type (D0, D1, P, S1, SP, W, plus the 4 stacked heads with rows), a unit_word -> list sym encoding, and Inc as an inductive relation. - Prove the unit lemmas with es / execute on the unit cells, with the IH as a hypothesis forall l, l {{B}}> r -->* l <{{C}} r'. This is the counter pattern of Example.v, with two or three IH uses. - Theorem U by induction on the Inc derivation; termination by induction on the wall count.
  2. Nursery (routine now). The 8 window runs are fixed finite executions, each with at most 12 uses of the W lemma as a hypothesis about the opaque rest. Write them as 8 lemmas G_tau . R --> G_tau' . F_tau . Phi_k(R) by es, with the W lemma and Lemma C1 as rewriting steps.
  3. Conveyor, Lemma T and the invariant (moderate). Represent the conveyor by the wall records of §7 (birth table, the clause-(c) carry chain). Inv(n, J) is a function of (n, J), and closure is the Lemma T algebra (lia) plus Lemma N.
  4. Zone (large). Define the closed system as a function on lists of units with D and j. - Lemmas Z1 and Z0 are short structural inductions over one step (the last-event argument and the one-wall argument), stated for any defined step. - Lemma L is a statement about two runs. Its proof is the upward-flow induction plus counter arithmetic mod 2^r. The representative runs become vm_compute checks of (H0)-(H2) and κ: 65,534 + 1,182 + 655 runs as written in §6, each tens of steps. - A smaller split for Rocq. Since Lemmas P and VF (level 2) hold for every v ≥ 12, the class recursion can hand over to the induction hypothesis from v > 50 instead of v > 600: then K′ = v − 10 ≥ 41, so E(K′) is in range. The endgame can then use the cut R = 12, which covers ν2(k+9) ≤ 10, and the nested range only 11 ≤ v ≤ 50. That is 4,094 + 80 + 655 representative runs instead of 67,371. S10 checks the R = 12 endgame (4,094/4,094); the nested runs for v ≤ 50 are part of S10's v ≤ 60 / v ≤ 600 runs. - VF: Lemma L′ (the one-step Lemma L with one P above the cut) plus vm_compute of the 1,304 one-step representatives and the per-form identities (μ/2^a + 1)/2^b = μ′, (wa/2^a + 1)/2^b = wa′. - Entry and plant (Lemmas E, P): 8 steps on closed forms, each a binary addition with lia / nia on 2^k terms. - The class recursion is a well-founded induction on K (§6.5). - Run CTL/parameter searches natively and let Coq check only the winners (rocq-notes: ~10 GB RSS otherwise).
  5. Assembly. Use progress_nonhalt_cond over the record family with Inv (§7), plus init by es (203,465 steps; use the shift-rule acceleration, or chain the 13 junction types).

Review log