\addbibresource

source.bib

Skelet #17 and the fifth Busy Beaver number

(Date: July 3, 2024)

1. Description

1.1. Introduction

The busy beaver function BB(n)BB𝑛\text{BB}(n)BB ( italic_n ) is defined to be the maximum number of moves a halting n𝑛nitalic_n-state 2222-symbol Turing machine makes before it halts. Although there is no general algorithm to compute BB(n)BB𝑛\text{BB}(n)BB ( italic_n ) in general, researchers have long conjectured that BB(5)=47,176,870BB547,176,870\text{BB}(5)=\text{47,176,870}BB ( 5 ) = 47,176,870, perhaps most recently by Aaronson [bbfrontier].

A massive undertaking by The Busy Beaver Challenge team [bbchallenge] has narrowed down the determination of BB(5)BB5\text{BB}(5)BB ( 5 ) to showing non-halting of approximately 30 “holdout” machines [bbchallengeholdouts]. Of those machines, there is significant overlap with a different list of 43 holdouts for which Georgi “Skelet” Georgiev claimed to find in 2003 [skelethomepage]: the machine dubbed Skelet #17 [skelet17] is the focus of our paper.

Although most of the 30 holdouts can be grouped into well-known categories, analysis of Skelet #17 has eluded all known attempts at classification. Members of [bbchallenge] are in general agreement that Skelet #17, along with Skelet #1, comprise the two most difficult holdouts to analyze. In this paper, we show that Skelet #17 does not halt (Theorem 1.3).

1.2. Skelet #17

By [savask], is known that Skelet #17 can be described by the following process: begin with the state S=(0,2,4,0)𝑆0240S=(0,2,4,0)italic_S = ( 0 , 2 , 4 , 0 ). Let P(S)𝑃𝑆P(S)italic_P ( italic_S ) be the next state after S𝑆Sitalic_S. P(S)𝑃𝑆P(S)italic_P ( italic_S ) is defined by the following rules:

  • Overflow: If S=(2a+1,2a1,,2a0)𝑆2subscript𝑎12subscript𝑎12subscript𝑎0S=(2a_{\ell}+1,2a_{\ell-1},\dots,2a_{0})italic_S = ( 2 italic_a start_POSTSUBSCRIPT roman_ℓ end_POSTSUBSCRIPT + 1 , 2 italic_a start_POSTSUBSCRIPT roman_ℓ - 1 end_POSTSUBSCRIPT , … , 2 italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ), transition to P(S)=(0,2a+2,2a1,,2a0)𝑃𝑆02subscript𝑎22subscript𝑎12subscript𝑎0P(S)=(0,2a_{\ell}+2,2a_{\ell-1},\dots,2a_{0})italic_P ( italic_S ) = ( 0 , 2 italic_a start_POSTSUBSCRIPT roman_ℓ end_POSTSUBSCRIPT + 2 , 2 italic_a start_POSTSUBSCRIPT roman_ℓ - 1 end_POSTSUBSCRIPT , … , 2 italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ).

  • Halt: If S=(0,0,2a2,,2a0)𝑆002subscript𝑎22subscript𝑎0S=(0,0,2a_{\ell-2},\dots,2a_{0})italic_S = ( 0 , 0 , 2 italic_a start_POSTSUBSCRIPT roman_ℓ - 2 end_POSTSUBSCRIPT , … , 2 italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ), halt.

  • Zero: If S=(2a,2a1,,2a0)𝑆2subscript𝑎2subscript𝑎12subscript𝑎0S=(2a_{\ell},2a_{\ell-1},\dots,2a_{0})italic_S = ( 2 italic_a start_POSTSUBSCRIPT roman_ℓ end_POSTSUBSCRIPT , 2 italic_a start_POSTSUBSCRIPT roman_ℓ - 1 end_POSTSUBSCRIPT , … , 2 italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ) and (a1,a2)(0,0)subscript𝑎1subscript𝑎200(a_{1},a_{2})\neq(0,0)( italic_a start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_a start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ) ≠ ( 0 , 0 ), transition to P(S)=(0,0,2a+1,2a1,,2a1,2a01)𝑃𝑆002subscript𝑎12subscript𝑎12subscript𝑎12subscript𝑎01P(S)=(0,0,2a_{\ell}+1,2a_{\ell-1},\dots,2a_{1},2a_{0}-1)italic_P ( italic_S ) = ( 0 , 0 , 2 italic_a start_POSTSUBSCRIPT roman_ℓ end_POSTSUBSCRIPT + 1 , 2 italic_a start_POSTSUBSCRIPT roman_ℓ - 1 end_POSTSUBSCRIPT , … , 2 italic_a start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , 2 italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT - 1 ).

  • Halve: If S=(a,,a1,1)𝑆subscript𝑎subscript𝑎11S=(a_{\ell},\dots,a_{1},-1)italic_S = ( italic_a start_POSTSUBSCRIPT roman_ℓ end_POSTSUBSCRIPT , … , italic_a start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , - 1 ), transition to P(S)=(a,,a1)𝑃𝑆subscript𝑎subscript𝑎1P(S)=(a_{\ell},\dots,a_{1})italic_P ( italic_S ) = ( italic_a start_POSTSUBSCRIPT roman_ℓ end_POSTSUBSCRIPT , … , italic_a start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ).

  • Increment: If S=(a,,a1,a0)𝑆subscript𝑎subscript𝑎1subscript𝑎0S=(a_{\ell},\dots,a_{1},a_{0})italic_S = ( italic_a start_POSTSUBSCRIPT roman_ℓ end_POSTSUBSCRIPT , … , italic_a start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ) is not in the form specified by any of the above rules, find the rightmost index aisubscript𝑎𝑖a_{i}italic_a start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT of S𝑆Sitalic_S with an odd value. Transition to P(S)=(a,ai+2,ai+1+1,ai,,a1,a01).𝑃𝑆subscript𝑎subscript𝑎𝑖2subscript𝑎𝑖11subscript𝑎𝑖subscript𝑎1subscript𝑎01P(S)=(a_{\ell},a_{i+2},a_{i+1}+1,a_{i},\dots,a_{1},a_{0}-1).italic_P ( italic_S ) = ( italic_a start_POSTSUBSCRIPT roman_ℓ end_POSTSUBSCRIPT , italic_a start_POSTSUBSCRIPT italic_i + 2 end_POSTSUBSCRIPT , italic_a start_POSTSUBSCRIPT italic_i + 1 end_POSTSUBSCRIPT + 1 , italic_a start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT , … , italic_a start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT - 1 ) .

Remark 1.1.

Note that the conventions of [savask] are slightly different from ours: the precise correspondence is as follows:

  • (E1) and (E2) in [savask] correspond to Zero here.

  • (E3) in [savask] corresponds to Halt here.

  • (O1) in [savask] corresponds to Zero \circ Overflow here.

  • (O2), (O3), (O4) and (O5) in [savask] correspond to Increment here.

  • (O6) in [savask] corresponds to Halve \circ Increment here.

Definition 1.2.

Given two states S𝑆Sitalic_S and T𝑇Titalic_T, say that STmaps-to𝑆𝑇S\mapsto Titalic_S ↦ italic_T if Pk(S)=Tsuperscript𝑃𝑘𝑆𝑇P^{k}(S)=Titalic_P start_POSTSUPERSCRIPT italic_k end_POSTSUPERSCRIPT ( italic_S ) = italic_T for some k𝑘k\in\mathbb{N}italic_k ∈ blackboard_N. In this case, define ST𝑆𝑇S\to Titalic_S → italic_T to be the sequence of transition rules that were applied from S𝑆Sitalic_S to obtain T𝑇Titalic_T.

The goal of this paper is to show that the above process never terminates. In particular, we will establish the following theorem:

Theorem 1.3.

We have (0,2,4,,22k,0)(0,2,4,,22k+2,0)maps-to024superscript22𝑘0024superscript22𝑘20(0,2,4,\dots,2^{2k},0)\mapsto(0,2,4,\dots,2^{2k+2},0)( 0 , 2 , 4 , … , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT , 0 ) ↦ ( 0 , 2 , 4 , … , 2 start_POSTSUPERSCRIPT 2 italic_k + 2 end_POSTSUPERSCRIPT , 0 ) for all k𝑘k\in\mathbb{N}italic_k ∈ blackboard_N. Moreover, during this, we use exactly one Overflow rule. As a result, Skelet #17 never halts.

1.3. Formalization

The author originally wrote up a sketch of this paper in 2023. Recently, “Mxdys” has adapted its contents to a formal proof of Skelet #17’s nonhalting [formalproof17], along with formalizing everything else in the BB(5)BB5\text{BB}(5)BB ( 5 ) program [formalproof]. As a result, we are able to conclude:

Theorem 1.4.

We have BB(5)=47,176,870BB547176870\text{BB}(5)=47,176,870BB ( 5 ) = 47 , 176 , 870.

2. Basics

2.1. State variables

For r𝑟r\in\mathbb{R}italic_r ∈ blackboard_R, let rdelimited-⟨⟩𝑟\left<r\right>⟨ italic_r ⟩ denote the nearest integer to r𝑟ritalic_r, where we round up if r𝑟ritalic_r is a half-integer (e.g 1.5=2delimited-⟨⟩1.52\left<1.5\right>=2⟨ 1.5 ⟩ = 2).

Definition 2.1.

For n𝑛n\in\mathbb{N}italic_n ∈ blackboard_N, the Gray code of n𝑛nitalic_n is defined to be GrayCode(n):=a3a2a1a0assignGrayCode𝑛subscript𝑎3subscript𝑎2subscript𝑎1subscript𝑎0\text{GrayCode}(n):=\cdots a_{3}a_{2}a_{1}a_{0}GrayCode ( italic_n ) := ⋯ italic_a start_POSTSUBSCRIPT 3 end_POSTSUBSCRIPT italic_a start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT italic_a start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT, where each digit ai{0,1}subscript𝑎𝑖01a_{i}\in\{0,1\}italic_a start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ∈ { 0 , 1 } equals the mod 2222 reduction of n/2idelimited-⟨⟩𝑛superscript2𝑖\left<n/2^{i}\right>⟨ italic_n / 2 start_POSTSUPERSCRIPT italic_i end_POSTSUPERSCRIPT ⟩.

For a state S=(a,,a0)𝑆subscript𝑎subscript𝑎0S=(a_{\ell},\dots,a_{0})italic_S = ( italic_a start_POSTSUBSCRIPT roman_ℓ end_POSTSUBSCRIPT , … , italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ), introduce the following notation, which is specified in order to capture the most important properties of Skelet #17:

  • Let n:=n(S)assign𝑛𝑛𝑆n:=n(S)italic_n := italic_n ( italic_S ) denote the number GrayCode1(a¯a1¯a1¯)superscriptGrayCode1¯subscript𝑎¯subscript𝑎1¯subscript𝑎1\text{GrayCode}^{-1}(\overline{a_{\ell}}\overline{a_{\ell-1}}\dots\overline{a_% {1}})GrayCode start_POSTSUPERSCRIPT - 1 end_POSTSUPERSCRIPT ( over¯ start_ARG italic_a start_POSTSUBSCRIPT roman_ℓ end_POSTSUBSCRIPT end_ARG over¯ start_ARG italic_a start_POSTSUBSCRIPT roman_ℓ - 1 end_POSTSUBSCRIPT end_ARG … over¯ start_ARG italic_a start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT end_ARG ). Here we let ai¯:=aimod2assign¯subscript𝑎𝑖modulosubscript𝑎𝑖2\overline{a_{i}}:=a_{i}\bmod 2over¯ start_ARG italic_a start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT end_ARG := italic_a start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT roman_mod 2, and note that we are not considering a0subscript𝑎0a_{0}italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT in the formation of n𝑛nitalic_n.

  • Let :=(S)assign𝑆\ell:=\ell(S)roman_ℓ := roman_ℓ ( italic_S ) denote the number one less than the size of S𝑆Sitalic_S, i.e. |S|1𝑆1|S|-1| italic_S | - 1.

  • Let σ:=σ(S){1,+1}assign𝜎𝜎𝑆11\sigma:=\sigma(S)\in\{-1,+1\}italic_σ := italic_σ ( italic_S ) ∈ { - 1 , + 1 } be +11+1+ 1 if i=0aisuperscriptsubscript𝑖0subscript𝑎𝑖\sum_{i=0}^{\ell}a_{i}∑ start_POSTSUBSCRIPT italic_i = 0 end_POSTSUBSCRIPT start_POSTSUPERSCRIPT roman_ℓ end_POSTSUPERSCRIPT italic_a start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT is odd, and 11-1- 1 if i=0aisuperscriptsubscript𝑖0subscript𝑎𝑖\sum_{i=0}^{\ell}a_{i}∑ start_POSTSUBSCRIPT italic_i = 0 end_POSTSUBSCRIPT start_POSTSUPERSCRIPT roman_ℓ end_POSTSUPERSCRIPT italic_a start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT is even.

  • In addition to the three state variables above, let ai:=ai(S)assignsubscript𝑎𝑖subscript𝑎𝑖𝑆a_{i}:=a_{i}(S)italic_a start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT := italic_a start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_S ) denote the value aisubscript𝑎𝑖a_{i}italic_a start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT of the ithsuperscript𝑖𝑡i^{th}italic_i start_POSTSUPERSCRIPT italic_t italic_h end_POSTSUPERSCRIPT index of S𝑆Sitalic_S, for i[0,].𝑖0i\in[0,\ell].italic_i ∈ [ 0 , roman_ℓ ] .

Under the transition rules, we may write down how the first three state variables change for each rule that is applied. In particular, one can verify the following table (where the substitutions in a given rule’s row are performed going left to right):

Rule n𝑛nitalic_n \ellroman_ℓ σ𝜎\sigmaitalic_σ
Overflow 210maps-tosuperscript2102^{\ell}-1\mapsto 02 start_POSTSUPERSCRIPT roman_ℓ end_POSTSUPERSCRIPT - 1 ↦ 0 +1maps-to1\ell\mapsto\ell+1roman_ℓ ↦ roman_ℓ + 1 +11maps-to11+1\mapsto-1+ 1 ↦ - 1
Empty 021maps-to0superscript210\mapsto 2^{\ell}-10 ↦ 2 start_POSTSUPERSCRIPT roman_ℓ end_POSTSUPERSCRIPT - 1 +2maps-to2\ell\mapsto\ell+2roman_ℓ ↦ roman_ℓ + 2 1111-1\to-1- 1 → - 1
Halve nn/2maps-to𝑛𝑛2n\mapsto\lfloor n/2\rflooritalic_n ↦ ⌊ italic_n / 2 ⌋ 1maps-to1\ell\mapsto\ell-1roman_ℓ ↦ roman_ℓ - 1 σσmaps-to𝜎𝜎\sigma\mapsto-\sigmaitalic_σ ↦ - italic_σ
Increment nn+σmaps-to𝑛𝑛𝜎n\mapsto n+\sigmaitalic_n ↦ italic_n + italic_σ maps-to\ell\mapsto\ellroman_ℓ ↦ roman_ℓ σσmaps-to𝜎𝜎\sigma\mapsto\sigmaitalic_σ ↦ italic_σ
Halt 0N/Amaps-to0N/A0\mapsto\text{N/A}0 ↦ N/A N/Amaps-toN/A\ell\mapsto\text{N/A}roman_ℓ ↦ N/A 1N/Amaps-to1N/A-1\mapsto\text{N/A}- 1 ↦ N/A

The above table does more than just specify how the state variables change with each rule: it also restricts what (n,,σ)𝑛𝜎(n,\ell,\sigma)( italic_n , roman_ℓ , italic_σ ) can be immediately before a given rule is applied. For instance, if S𝑆Sitalic_S is a state for which we Overflow out of, then we must necessarily have n(S)=2(S)1𝑛𝑆superscript2𝑆1n(S)=2^{\ell(S)}-1italic_n ( italic_S ) = 2 start_POSTSUPERSCRIPT roman_ℓ ( italic_S ) end_POSTSUPERSCRIPT - 1 and σ(S)=+1𝜎𝑆1\sigma(S)=+1italic_σ ( italic_S ) = + 1.

2.2. Increments

Define the function

dj(a,b)subscript𝑑𝑗𝑎𝑏\displaystyle d_{j}(a,b)italic_d start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_a , italic_b ) :=|a2jb2j|.assignabsentdelimited-⟨⟩𝑎superscript2𝑗delimited-⟨⟩𝑏superscript2𝑗\displaystyle:=\left|\left<\frac{a}{2^{j}}\right>-\left<\frac{b}{2^{j}}\right>% \right|.:= | ⟨ divide start_ARG italic_a end_ARG start_ARG 2 start_POSTSUPERSCRIPT italic_j end_POSTSUPERSCRIPT end_ARG ⟩ - ⟨ divide start_ARG italic_b end_ARG start_ARG 2 start_POSTSUPERSCRIPT italic_j end_POSTSUPERSCRIPT end_ARG ⟩ | .

The next proposition states how a state’s coordinates change under a series of increments:

Proposition 2.2.

Suppose we have states S𝑆Sitalic_S and Ssuperscript𝑆S^{\prime}italic_S start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT where SSmaps-to𝑆superscript𝑆S\mapsto S^{\prime}italic_S ↦ italic_S start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT, such that SS𝑆superscript𝑆S\to S^{\prime}italic_S → italic_S start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT consists of rules of the form Increment. Denote n:=n(S)assign𝑛𝑛𝑆n:=n(S)italic_n := italic_n ( italic_S ), n:=n(S)assignsuperscript𝑛𝑛superscript𝑆n^{\prime}:=n(S^{\prime})italic_n start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT := italic_n ( italic_S start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) and σ:=σ(S)=σ(S)assign𝜎𝜎𝑆𝜎superscript𝑆\sigma:=\sigma(S)=\sigma(S^{\prime})italic_σ := italic_σ ( italic_S ) = italic_σ ( italic_S start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ). Then for each i[0,]𝑖0i\in[0,\ell]italic_i ∈ [ 0 , roman_ℓ ] we have

ai(S)subscript𝑎𝑖superscript𝑆\displaystyle a_{i}(S^{\prime})italic_a start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_S start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) ={ai(S)+di(n,n)i1ai(S)di(n,n)i=0.absentcasessubscript𝑎𝑖𝑆subscript𝑑𝑖𝑛superscript𝑛𝑖1subscript𝑎𝑖𝑆subscript𝑑𝑖𝑛superscript𝑛𝑖0\displaystyle=\begin{cases}a_{i}(S)+d_{i}(n,n^{\prime})&i\geq 1\\ a_{i}(S)-d_{i}(n,n^{\prime})&i=0.\end{cases}= { start_ROW start_CELL italic_a start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_S ) + italic_d start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_n , italic_n start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) end_CELL start_CELL italic_i ≥ 1 end_CELL end_ROW start_ROW start_CELL italic_a start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_S ) - italic_d start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_n , italic_n start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) end_CELL start_CELL italic_i = 0 . end_CELL end_ROW
Proof.

For i=0𝑖0i=0italic_i = 0, we have di(n,n)=|nn|subscript𝑑𝑖𝑛superscript𝑛superscript𝑛𝑛d_{i}(n,n^{\prime})=|n^{\prime}-n|italic_d start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_n , italic_n start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) = | italic_n start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - italic_n |, which is precisely the number of Increment rules in SS𝑆superscript𝑆S\to S^{\prime}italic_S → italic_S start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT. Since a0subscript𝑎0a_{0}italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT decreases after an Increment rule, the claim d0(n,n)=a0(S)a0(S)subscript𝑑0𝑛superscript𝑛subscript𝑎0𝑆subscript𝑎0superscript𝑆d_{0}(n,n^{\prime})=a_{0}(S)-a_{0}(S^{\prime})italic_d start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ( italic_n , italic_n start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) = italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ( italic_S ) - italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ( italic_S start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) follows immediately. For i>0𝑖0i>0italic_i > 0, note that by Definition 2.1, the value di(n,n)subscript𝑑𝑖𝑛superscript𝑛d_{i}(n,n^{\prime})italic_d start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_n , italic_n start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) quantifies how much aisubscript𝑎𝑖a_{i}italic_a start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT increases when incrementing the Gray code of n𝑛nitalic_n to the Gray code of nsuperscript𝑛n^{\prime}italic_n start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT. ∎

3. The speedup

3.1. Conventions

From this section onwards, fix k𝑘k\in\mathbb{N}italic_k ∈ blackboard_N and let Sk:=(0,2,22,,22k,0)assignsubscript𝑆𝑘02superscript22superscript22𝑘0S_{k}:=(0,2,2^{2},\dots,2^{2k},0)italic_S start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT := ( 0 , 2 , 2 start_POSTSUPERSCRIPT 2 end_POSTSUPERSCRIPT , … , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT , 0 ). From now on, every state E𝐸Eitalic_E we will consider will satisfy SkEmaps-tosubscript𝑆𝑘𝐸S_{k}\mapsto Eitalic_S start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT ↦ italic_E, but not Sk+1Emaps-tosubscript𝑆𝑘1𝐸S_{k+1}\mapsto Eitalic_S start_POSTSUBSCRIPT italic_k + 1 end_POSTSUBSCRIPT ↦ italic_E. For E=(a,,a1,a0)𝐸subscript𝑎subscript𝑎1subscript𝑎0E=(a_{\ell},\dots,a_{1},a_{0})italic_E = ( italic_a start_POSTSUBSCRIPT roman_ℓ end_POSTSUBSCRIPT , … , italic_a start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ) and i[0,]𝑖0i\in[0,\ell]italic_i ∈ [ 0 , roman_ℓ ], denote E[i]:=(a,,ai+1,ai+2,ai1,,a0)assign𝐸delimited-[]𝑖subscript𝑎subscript𝑎𝑖1subscript𝑎𝑖2subscript𝑎𝑖1subscript𝑎0E[i]:=(a_{\ell},\dots,a_{i+1},a_{i}+2,a_{i-1},\dots,a_{0})italic_E [ italic_i ] := ( italic_a start_POSTSUBSCRIPT roman_ℓ end_POSTSUBSCRIPT , … , italic_a start_POSTSUBSCRIPT italic_i + 1 end_POSTSUBSCRIPT , italic_a start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT + 2 , italic_a start_POSTSUBSCRIPT italic_i - 1 end_POSTSUBSCRIPT , … , italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ), which is E𝐸Eitalic_E but with aisubscript𝑎𝑖a_{i}italic_a start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT incremented by +22+2+ 2.

3.2. Empty and embanked states

Definition 3.1.

Call a state E𝐸Eitalic_E empty if n(E)=0𝑛𝐸0n(E)=0italic_n ( italic_E ) = 0 and σ(E)=1𝜎𝐸1\sigma(E)=-1italic_σ ( italic_E ) = - 1, but the next rule applied is not Halt (so in particular the state immediately after E𝐸Eitalic_E is achieved by applying Zero).

If E𝐸Eitalic_E is empty, then let N(E):=TE(E)assign𝑁𝐸subscript𝑇𝐸𝐸N(E):=T_{E}(E)italic_N ( italic_E ) := italic_T start_POSTSUBSCRIPT italic_E end_POSTSUBSCRIPT ( italic_E ) denote the next state after E𝐸Eitalic_E that is empty. Let TEsubscript𝑇𝐸T_{E}italic_T start_POSTSUBSCRIPT italic_E end_POSTSUBSCRIPT denote the sequence of rules EN(E)𝐸𝑁𝐸E\to N(E)italic_E → italic_N ( italic_E ) if N(E)𝑁𝐸N(E)italic_N ( italic_E ) exists, and otherwise let TEsubscript𝑇𝐸T_{E}italic_T start_POSTSUBSCRIPT italic_E end_POSTSUBSCRIPT denote the sequence of rules after E𝐸Eitalic_E.

Definition 3.2.

Let E𝐸Eitalic_E be an empty state.

  1. (1)

    Say that E𝐸Eitalic_E is embanked if the non-Increment rules of TEsubscript𝑇𝐸T_{E}italic_T start_POSTSUBSCRIPT italic_E end_POSTSUBSCRIPT consist of exactly one Zero rule at the start and exactly two Halve rules elsewhere.

  2. (2)

    Say that E𝐸Eitalic_E is weakly embanked if the rules of TEsubscript𝑇𝐸T_{E}italic_T start_POSTSUBSCRIPT italic_E end_POSTSUBSCRIPT consist of one Zero rule at the start and at least two Halve rules (in particular, there may be arbitrarily many), such that all other rules before the second Halve rule are Increment rules.

  3. (3)

    Suppose E𝐸Eitalic_E is weakly embanked. For i{1,2}𝑖12i\in\{1,2\}italic_i ∈ { 1 , 2 }, define hi:=hi(E)assignsubscript𝑖subscript𝑖𝐸h_{i}:=h_{i}(E)italic_h start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT := italic_h start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_E ) (resp. si:=si(E)assignsubscript𝑠𝑖subscript𝑠𝑖𝐸s_{i}:=s_{i}(E)italic_s start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT := italic_s start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_E )) to be the value of n𝑛nitalic_n for the state immediately after (resp. before) the ithsuperscript𝑖𝑡i^{th}italic_i start_POSTSUPERSCRIPT italic_t italic_h end_POSTSUPERSCRIPT Halve rule is applied in TEsubscript𝑇𝐸T_{E}italic_T start_POSTSUBSCRIPT italic_E end_POSTSUBSCRIPT. Let h:=h(E)assign𝐸h:=h(E)italic_h := italic_h ( italic_E ) (resp. s:=s(E)assign𝑠𝑠𝐸s:=s(E)italic_s := italic_s ( italic_E )) denote the tuple (h1(E),h2(E))subscript1𝐸subscript2𝐸(h_{1}(E),h_{2}(E))( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ( italic_E ) , italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ( italic_E ) ) (resp. (s1(E),s2(E))subscript𝑠1𝐸subscript𝑠2𝐸(s_{1}(E),s_{2}(E))( italic_s start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ( italic_E ) , italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ( italic_E ) )). So in particular we have hi=si/2subscript𝑖subscript𝑠𝑖2h_{i}=\lfloor s_{i}/2\rflooritalic_h start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT = ⌊ italic_s start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT / 2 ⌋.

In the course of proving Theorem 1.3, we will in fact see that the vast majority of the empty states we consider are embanked. In the first non-embanked empty state we see, an Overflow rule results, at which point an explicit analysis will yield the desired result. It is in this fact that the reason for the term embanked becomes clear: it signifies that TEsubscript𝑇𝐸T_{E}italic_T start_POSTSUBSCRIPT italic_E end_POSTSUBSCRIPT flows extremely well as we repeatedly apply N()𝑁N(\cdot)italic_N ( ⋅ ), and in particular well enough for us to apply major speedups to the Skelet #17 process.

Example 3.3.

Let E:=(2,2,6,8,18,0)assign𝐸2268180E:=(2,2,6,8,18,0)italic_E := ( 2 , 2 , 6 , 8 , 18 , 0 ). Then E𝐸Eitalic_E is embanked with h(E)=(15,17)𝐸1517h(E)=(15,17)italic_h ( italic_E ) = ( 15 , 17 ). Let us spell out TEsubscript𝑇𝐸T_{E}italic_T start_POSTSUBSCRIPT italic_E end_POSTSUBSCRIPT in detail: n𝑛nitalic_n will start at 31313131 after the first Empty rule, with corresponding state (0,0,3,2,6,8,18,1)003268181(0,0,3,2,6,8,18,-1)( 0 , 0 , 3 , 2 , 6 , 8 , 18 , - 1 ). Here, we have a0=1subscript𝑎01a_{0}=-1italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT = - 1, so we must immediately apply the first Halve rule, which takes n𝑛nitalic_n to 31/2=1531215\lfloor 31/2\rfloor=15⌊ 31 / 2 ⌋ = 15 and σ𝜎\sigmaitalic_σ to +11+1+ 1, with ensuing state (0,0,3,2,6,8,18)00326818(0,0,3,2,6,8,18)( 0 , 0 , 3 , 2 , 6 , 8 , 18 ). A series of Increment rules are applied until n=34𝑛34n=34italic_n = 34, where the state is now (1,1,4,4,11,17,1)114411171(1,1,4,4,11,17,-1)( 1 , 1 , 4 , 4 , 11 , 17 , - 1 ). Then the second Halve rule is applied to yield (n,σ)=(17,1)𝑛𝜎171(n,\sigma)=(17,-1)( italic_n , italic_σ ) = ( 17 , - 1 ), and after a further series of Increment rules we have n=0𝑛0n=0italic_n = 0, which corresponds to the state E=(2,2,6,8,20,0)=E[1]superscript𝐸2268200𝐸delimited-[]1E^{\prime}=(2,2,6,8,20,0)=E[1]italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT = ( 2 , 2 , 6 , 8 , 20 , 0 ) = italic_E [ 1 ]. The reader is highly encouraged to graph the values of n𝑛nitalic_n attained in TEsubscript𝑇𝐸T_{E}italic_T start_POSTSUBSCRIPT italic_E end_POSTSUBSCRIPT to gain an intuition behind this paper.

Proposition 3.4.

Empty state E𝐸Eitalic_E is weakly embanked if and only if the following conditions hold:

  1. (1)

    a0(E)<22k+11subscript𝑎0𝐸superscript22𝑘11a_{0}(E)<2^{2k+1}-1italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ( italic_E ) < 2 start_POSTSUPERSCRIPT 2 italic_k + 1 end_POSTSUPERSCRIPT - 1.

  2. (2)

    a1(E)<322k1subscript𝑎1𝐸3superscript22𝑘1a_{1}(E)<3\cdot 2^{2k}-1italic_a start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ( italic_E ) < 3 ⋅ 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - 1.

Proof.

For E𝐸Eitalic_E to be weakly embanked, the sequence TZero¯(E)subscript𝑇¯Zero𝐸T_{\underline{\text{Zero}}(E)}italic_T start_POSTSUBSCRIPT under¯ start_ARG Zero end_ARG ( italic_E ) end_POSTSUBSCRIPT must have two Halve rules before any non-Increment rule. To guarantee that the first Halve rule occurs before any non-Increment rule, the variable a0subscript𝑎0a_{0}italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT must decrement to 11-1- 1 from a0(Zero¯(E))=a0(E)1subscript𝑎0¯Zero𝐸subscript𝑎0𝐸1a_{0}(\underline{\text{Zero}}(E))=a_{0}(E)-1italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ( under¯ start_ARG Zero end_ARG ( italic_E ) ) = italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ( italic_E ) - 1 before the variable n𝑛nitalic_n decrements to 00 from n(Zero¯(E))=22k+11𝑛¯Zero𝐸superscript22𝑘11n(\underline{\text{Zero}}(E))=2^{2k+1}-1italic_n ( under¯ start_ARG Zero end_ARG ( italic_E ) ) = 2 start_POSTSUPERSCRIPT 2 italic_k + 1 end_POSTSUPERSCRIPT - 1. This is the same as the first condition.

Assume condition (1) holds, and let Esuperscript𝐸E^{\prime}italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT be the state immediately after applying the first Halve rule in TEsubscript𝑇𝐸T_{E}italic_T start_POSTSUBSCRIPT italic_E end_POSTSUBSCRIPT. To guarantee that the second Halve rule occurs before any non-Increment rule, the variable a0subscript𝑎0a_{0}italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT must decrement from a0(E)subscript𝑎0superscript𝐸a_{0}(E^{\prime})italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ( italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) to 11-1- 1 before the variable n𝑛nitalic_n increments from n(E)𝑛superscript𝐸n(E^{\prime})italic_n ( italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) to 22k+21superscript22𝑘212^{2k+2}-12 start_POSTSUPERSCRIPT 2 italic_k + 2 end_POSTSUPERSCRIPT - 1 (after which an Overflow rule would have to be applied). We readily compute

a0(E)subscript𝑎0superscript𝐸\displaystyle a_{0}(E^{\prime})italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ( italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) =a1(E)+d1(22k+11,22k+11a0)absentsubscript𝑎1𝐸subscript𝑑1superscript22𝑘11superscript22𝑘11subscript𝑎0\displaystyle=a_{1}(E)+d_{1}(2^{2k+1}-1,2^{2k+1}-1-a_{0})= italic_a start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ( italic_E ) + italic_d start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ( 2 start_POSTSUPERSCRIPT 2 italic_k + 1 end_POSTSUPERSCRIPT - 1 , 2 start_POSTSUPERSCRIPT 2 italic_k + 1 end_POSTSUPERSCRIPT - 1 - italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT )
n(E)𝑛superscript𝐸\displaystyle n(E^{\prime})italic_n ( italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) =22k+11a0(E)2absentsuperscript22𝑘11subscript𝑎0𝐸2\displaystyle=\left\lfloor\frac{2^{2k+1}-1-a_{0}(E)}{2}\right\rfloor= ⌊ divide start_ARG 2 start_POSTSUPERSCRIPT 2 italic_k + 1 end_POSTSUPERSCRIPT - 1 - italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ( italic_E ) end_ARG start_ARG 2 end_ARG ⌋

so that the desired condition becomes the inequality

a1(E)+d1(22k+11,22k+11a0(E))+1<22k+2122k+11a0(E)2.subscript𝑎1𝐸subscript𝑑1superscript22𝑘11superscript22𝑘11subscript𝑎0𝐸1superscript22𝑘21superscript22𝑘11subscript𝑎0𝐸2\displaystyle a_{1}(E)+d_{1}(2^{2k+1}-1,2^{2k+1}-1-a_{0}(E))+1<2^{2k+2}-1-% \left\lfloor\frac{2^{2k+1}-1-a_{0}(E)}{2}\right\rfloor.italic_a start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ( italic_E ) + italic_d start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ( 2 start_POSTSUPERSCRIPT 2 italic_k + 1 end_POSTSUPERSCRIPT - 1 , 2 start_POSTSUPERSCRIPT 2 italic_k + 1 end_POSTSUPERSCRIPT - 1 - italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ( italic_E ) ) + 1 < 2 start_POSTSUPERSCRIPT 2 italic_k + 2 end_POSTSUPERSCRIPT - 1 - ⌊ divide start_ARG 2 start_POSTSUPERSCRIPT 2 italic_k + 1 end_POSTSUPERSCRIPT - 1 - italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ( italic_E ) end_ARG start_ARG 2 end_ARG ⌋ .

Note that a0(E)subscript𝑎0𝐸a_{0}(E)italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ( italic_E ) is necessarily even (since E𝐸Eitalic_E is empty), so the above inequality becomes

a1(E)+a0(E)2+1subscript𝑎1𝐸subscript𝑎0𝐸21\displaystyle a_{1}(E)+\frac{a_{0}(E)}{2}+1italic_a start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ( italic_E ) + divide start_ARG italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ( italic_E ) end_ARG start_ARG 2 end_ARG + 1 <22k+21(22ka0(E)+22),absentsuperscript22𝑘21superscript22𝑘subscript𝑎0𝐸22\displaystyle<2^{2k+2}-1-\left(2^{2k}-\frac{a_{0}(E)+2}{2}\right),< 2 start_POSTSUPERSCRIPT 2 italic_k + 2 end_POSTSUPERSCRIPT - 1 - ( 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - divide start_ARG italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ( italic_E ) + 2 end_ARG start_ARG 2 end_ARG ) ,

which further simplifies to a1(E)<322k1.subscript𝑎1𝐸3superscript22𝑘1a_{1}(E)<3\cdot 2^{2k}-1.italic_a start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ( italic_E ) < 3 ⋅ 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - 1 . This is exactly condition (2), so we win. ∎

3.3. Speedup

Lemma 3.5.

Let E=(a,,a1,a0)𝐸subscript𝑎subscript𝑎1subscript𝑎0E=(a_{\ell},\dots,a_{1},a_{0})italic_E = ( italic_a start_POSTSUBSCRIPT roman_ℓ end_POSTSUBSCRIPT , … , italic_a start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT ) be an embanked state with h(E)=:(h1,h2)h(E)=:(h_{1},h_{2})italic_h ( italic_E ) = : ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ), s(E)=:(s1,s2)s(E)=:(s_{1},s_{2})italic_s ( italic_E ) = : ( italic_s start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ), and choose i[0,]𝑖0i\in[0,\ell]italic_i ∈ [ 0 , roman_ℓ ] such that E[i]𝐸delimited-[]𝑖E[i]italic_E [ italic_i ] is weakly embanked. Then we have

h(E[i])𝐸delimited-[]𝑖\displaystyle h(E[i])italic_h ( italic_E [ italic_i ] ) ={(h11,h2)i=0(h1,h2+1)i=1(h1,h2)i2.absentcasessubscript11subscript2𝑖0subscript1subscript21𝑖1subscript1subscript2𝑖2\displaystyle=\begin{cases}(h_{1}-1,h_{2})&i=0\\ (h_{1},h_{2}+1)&i=1\\ (h_{1},h_{2})&i\geq 2.\end{cases}= { start_ROW start_CELL ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT - 1 , italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ) end_CELL start_CELL italic_i = 0 end_CELL end_ROW start_ROW start_CELL ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 1 ) end_CELL start_CELL italic_i = 1 end_CELL end_ROW start_ROW start_CELL ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ) end_CELL start_CELL italic_i ≥ 2 . end_CELL end_ROW
s(E[i])𝑠𝐸delimited-[]𝑖\displaystyle s(E[i])italic_s ( italic_E [ italic_i ] ) ={(s12,s2)i=0(s1,s2+2)i=1(s1,s2)i2.absentcasessubscript𝑠12subscript𝑠2𝑖0subscript𝑠1subscript𝑠22𝑖1subscript𝑠1subscript𝑠2𝑖2\displaystyle=\begin{cases}(s_{1}-2,s_{2})&i=0\\ (s_{1},s_{2}+2)&i=1\\ (s_{1},s_{2})&i\geq 2.\end{cases}= { start_ROW start_CELL ( italic_s start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT - 2 , italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ) end_CELL start_CELL italic_i = 0 end_CELL end_ROW start_ROW start_CELL ( italic_s start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 2 ) end_CELL start_CELL italic_i = 1 end_CELL end_ROW start_ROW start_CELL ( italic_s start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ) end_CELL start_CELL italic_i ≥ 2 . end_CELL end_ROW
Proof.

Note that h(E)𝐸h(E)italic_h ( italic_E ) depends on only the indices a1subscript𝑎1a_{1}italic_a start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT and a0subscript𝑎0a_{0}italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT of E𝐸Eitalic_E (this immediately implies h(E[i])=h(E)𝐸delimited-[]𝑖𝐸h(E[i])=h(E)italic_h ( italic_E [ italic_i ] ) = italic_h ( italic_E ) for i2𝑖2i\geq 2italic_i ≥ 2). In particular, a0subscript𝑎0a_{0}italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT influences h1subscript1h_{1}italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT while a1subscript𝑎1a_{1}italic_a start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT influences h2subscript2h_{2}italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT. Thus, if i=0𝑖0i=0italic_i = 0, then, before the first Halve rule of TE[i]subscript𝑇𝐸delimited-[]𝑖T_{E[i]}italic_T start_POSTSUBSCRIPT italic_E [ italic_i ] end_POSTSUBSCRIPT, we must apply the Increment rule two additional times compared to TEsubscript𝑇𝐸T_{E}italic_T start_POSTSUBSCRIPT italic_E end_POSTSUBSCRIPT before the necessary a0=1subscript𝑎01a_{0}=-1italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT = - 1 occurs; it follows that h(E[0])=(h11,h2)𝐸delimited-[]0subscript11subscript2h(E[0])=(h_{1}-1,h_{2})italic_h ( italic_E [ 0 ] ) = ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT - 1 , italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ). A similar analysis for the states preceding the second Halve rule of TE[i]subscript𝑇𝐸delimited-[]𝑖T_{E[i]}italic_T start_POSTSUBSCRIPT italic_E [ italic_i ] end_POSTSUBSCRIPT yields h(E[1])=(h1,h2+1).𝐸delimited-[]1subscript1subscript21h(E[1])=(h_{1},h_{2}+1).italic_h ( italic_E [ 1 ] ) = ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 1 ) .

Proposition 3.6.

Suppose E𝐸Eitalic_E is an embanked state such that N(E)=E[i]𝑁𝐸𝐸delimited-[]𝑖N(E)=E[i]italic_N ( italic_E ) = italic_E [ italic_i ] for some i[0,(E)]𝑖0𝐸i\in[0,\ell(E)]italic_i ∈ [ 0 , roman_ℓ ( italic_E ) ], and suppose N(E)𝑁𝐸N(E)italic_N ( italic_E ) is weakly embanked. Let =(E)𝐸\ell=\ell(E)roman_ℓ = roman_ℓ ( italic_E ), h(E)=(h1,h2)𝐸subscript1subscript2h(E)=(h_{1},h_{2})italic_h ( italic_E ) = ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ) and s(E)=(s1,s2)𝑠𝐸subscript𝑠1subscript𝑠2s(E)=(s_{1},s_{2})italic_s ( italic_E ) = ( italic_s start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ). Then N(E)𝑁𝐸N(E)italic_N ( italic_E ) is in fact embanked, with

N(N(E))𝑁𝑁𝐸\displaystyle N(N(E))italic_N ( italic_N ( italic_E ) ) ={N(E)[ν2(h1)]i=0N(E)[ν2(h2+1)+1]i=1N(E)[i2]i2.absentcases𝑁𝐸delimited-[]subscript𝜈2subscript1𝑖0𝑁𝐸delimited-[]subscript𝜈2subscript211𝑖1𝑁𝐸delimited-[]𝑖2𝑖2\displaystyle=\begin{cases}N(E)[\nu_{2}(h_{1})]&i=0\\ N(E)[\nu_{2}(h_{2}+1)+1]&i=1\\ N(E)[i-2]&i\geq 2.\end{cases}= { start_ROW start_CELL italic_N ( italic_E ) [ italic_ν start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ) ] end_CELL start_CELL italic_i = 0 end_CELL end_ROW start_ROW start_CELL italic_N ( italic_E ) [ italic_ν start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 1 ) + 1 ] end_CELL start_CELL italic_i = 1 end_CELL end_ROW start_ROW start_CELL italic_N ( italic_E ) [ italic_i - 2 ] end_CELL start_CELL italic_i ≥ 2 . end_CELL end_ROW
Proof.

If i2𝑖2i\geq 2italic_i ≥ 2, then by Lemma 3.5, h(N(E))=h(E)𝑁𝐸𝐸h(N(E))=h(E)italic_h ( italic_N ( italic_E ) ) = italic_h ( italic_E ). N(E)𝑁𝐸N(E)italic_N ( italic_E ) is just E𝐸Eitalic_E with aisubscript𝑎𝑖a_{i}italic_a start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT incremented by +22+2+ 2, and the ithsuperscript𝑖𝑡i^{th}italic_i start_POSTSUPERSCRIPT italic_t italic_h end_POSTSUPERSCRIPT index will shift to the (i2)thsuperscript𝑖2𝑡(i-2)^{th}( italic_i - 2 ) start_POSTSUPERSCRIPT italic_t italic_h end_POSTSUPERSCRIPT index upon another application of N𝑁Nitalic_N. Since the indices a1subscript𝑎1a_{1}italic_a start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT and a0subscript𝑎0a_{0}italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT are the same for E𝐸Eitalic_E and N(E)𝑁𝐸N(E)italic_N ( italic_E ), we have TE=TN(E)subscript𝑇𝐸subscript𝑇𝑁𝐸T_{E}=T_{N(E)}italic_T start_POSTSUBSCRIPT italic_E end_POSTSUBSCRIPT = italic_T start_POSTSUBSCRIPT italic_N ( italic_E ) end_POSTSUBSCRIPT, hence N(E)𝑁𝐸N(E)italic_N ( italic_E ) is embanked with N(N(E))=N(E)[i2]𝑁𝑁𝐸𝑁𝐸delimited-[]𝑖2N(N(E))=N(E)[i-2]italic_N ( italic_N ( italic_E ) ) = italic_N ( italic_E ) [ italic_i - 2 ].

The nontrivial cases are i{0,1}𝑖01i\in\{0,1\}italic_i ∈ { 0 , 1 }. If i=1𝑖1i=1italic_i = 1, then Lemma 3.5 implies that, compared to TEsubscript𝑇𝐸T_{E}italic_T start_POSTSUBSCRIPT italic_E end_POSTSUBSCRIPT, the transition TE[1]subscript𝑇𝐸delimited-[]1T_{E[1]}italic_T start_POSTSUBSCRIPT italic_E [ 1 ] end_POSTSUBSCRIPT acquires exactly two additional Increment rules between the first and second Halve rules, as well as one additional Increment rule after the second Halve rule. Let us analyze what happens to the jthsuperscript𝑗𝑡j^{th}italic_j start_POSTSUPERSCRIPT italic_t italic_h end_POSTSUPERSCRIPT index for each j[0,]𝑗0j\in[0,\ell]italic_j ∈ [ 0 , roman_ℓ ]. Let TEsuperscriptsubscript𝑇𝐸T_{E}^{\prime}italic_T start_POSTSUBSCRIPT italic_E end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT denote the transition Zero¯(E)N(E)¯Zero𝐸𝑁𝐸\underline{\text{Zero}}(E)\to N(E)under¯ start_ARG Zero end_ARG ( italic_E ) → italic_N ( italic_E ); this is TEsubscript𝑇𝐸T_{E}italic_T start_POSTSUBSCRIPT italic_E end_POSTSUBSCRIPT but with the first transition removed. By Proposition 2.2, we have

aj(E[1])subscript𝑎𝑗𝐸delimited-[]1\displaystyle a_{j}(E[1])italic_a start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_E [ 1 ] ) ={aj+2(Zero¯(E))+dj+2(21,s1)+dj+1(h1,s2)+dj(h2,0)j1aj+2(Zero¯(E))+dj+2(21,s1)+dj+1(h1,s2)dj(h2,0)j=0,absentcasessubscript𝑎𝑗2¯Zero𝐸subscript𝑑𝑗2superscript21subscript𝑠1subscript𝑑𝑗1subscript1subscript𝑠2subscript𝑑𝑗subscript20𝑗1subscript𝑎𝑗2¯Zero𝐸subscript𝑑𝑗2superscript21subscript𝑠1subscript𝑑𝑗1subscript1subscript𝑠2subscript𝑑𝑗subscript20𝑗0\displaystyle=\begin{cases}a_{j+2}(\underline{\text{Zero}}(E))+d_{j+2}(2^{\ell% }-1,s_{1})+d_{j+1}(h_{1},s_{2})+d_{j}(h_{2},0)&j\geq 1\\ a_{j+2}(\underline{\text{Zero}}(E))+d_{j+2}(2^{\ell}-1,s_{1})+d_{j+1}(h_{1},s_% {2})-d_{j}(h_{2},0)&j=0,\end{cases}= { start_ROW start_CELL italic_a start_POSTSUBSCRIPT italic_j + 2 end_POSTSUBSCRIPT ( under¯ start_ARG Zero end_ARG ( italic_E ) ) + italic_d start_POSTSUBSCRIPT italic_j + 2 end_POSTSUBSCRIPT ( 2 start_POSTSUPERSCRIPT roman_ℓ end_POSTSUPERSCRIPT - 1 , italic_s start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ) + italic_d start_POSTSUBSCRIPT italic_j + 1 end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ) + italic_d start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT , 0 ) end_CELL start_CELL italic_j ≥ 1 end_CELL end_ROW start_ROW start_CELL italic_a start_POSTSUBSCRIPT italic_j + 2 end_POSTSUBSCRIPT ( under¯ start_ARG Zero end_ARG ( italic_E ) ) + italic_d start_POSTSUBSCRIPT italic_j + 2 end_POSTSUBSCRIPT ( 2 start_POSTSUPERSCRIPT roman_ℓ end_POSTSUPERSCRIPT - 1 , italic_s start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ) + italic_d start_POSTSUBSCRIPT italic_j + 1 end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ) - italic_d start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT , 0 ) end_CELL start_CELL italic_j = 0 , end_CELL end_ROW

noting that (1) the indices shift every time a Halve rule is applied, and (2) all djsubscript𝑑𝑗d_{j}italic_d start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT’s are in fact defined, since Zero adds two extra indices to the state. Moreover, define

aj(N(E[1]))superscriptsubscript𝑎𝑗𝑁𝐸delimited-[]1\displaystyle a_{j}^{\prime}(N(E[1]))italic_a start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ( italic_N ( italic_E [ 1 ] ) ) :={aj+2(Zero¯(E[1]))+dj+2(21,s1)+dj+1(h1,s2+2)+dj(h2+1,0)j1aj+2(Zero¯(E[1]))+dj+2(21,s1)+dj+1(h1,s2+2)dj(h2+1,0)j=0,assignabsentcasessubscript𝑎𝑗2¯Zero𝐸delimited-[]1subscript𝑑𝑗2superscript21subscript𝑠1subscript𝑑𝑗1subscript1subscript𝑠22subscript𝑑𝑗subscript210𝑗1subscript𝑎𝑗2¯Zero𝐸delimited-[]1subscript𝑑𝑗2superscript21subscript𝑠1subscript𝑑𝑗1subscript1subscript𝑠22subscript𝑑𝑗subscript210𝑗0\displaystyle:=\begin{cases}a_{j+2}(\underline{\text{Zero}}(E[1]))+d_{j+2}(2^{% \ell}-1,s_{1})+d_{j+1}(h_{1},s_{2}+2)+d_{j}(h_{2}+1,0)&j\geq 1\\ a_{j+2}(\underline{\text{Zero}}(E[1]))+d_{j+2}(2^{\ell}-1,s_{1})+d_{j+1}(h_{1}% ,s_{2}+2)-d_{j}(h_{2}+1,0)&j=0,\end{cases}:= { start_ROW start_CELL italic_a start_POSTSUBSCRIPT italic_j + 2 end_POSTSUBSCRIPT ( under¯ start_ARG Zero end_ARG ( italic_E [ 1 ] ) ) + italic_d start_POSTSUBSCRIPT italic_j + 2 end_POSTSUBSCRIPT ( 2 start_POSTSUPERSCRIPT roman_ℓ end_POSTSUPERSCRIPT - 1 , italic_s start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ) + italic_d start_POSTSUBSCRIPT italic_j + 1 end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 2 ) + italic_d start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 1 , 0 ) end_CELL start_CELL italic_j ≥ 1 end_CELL end_ROW start_ROW start_CELL italic_a start_POSTSUBSCRIPT italic_j + 2 end_POSTSUBSCRIPT ( under¯ start_ARG Zero end_ARG ( italic_E [ 1 ] ) ) + italic_d start_POSTSUBSCRIPT italic_j + 2 end_POSTSUBSCRIPT ( 2 start_POSTSUPERSCRIPT roman_ℓ end_POSTSUPERSCRIPT - 1 , italic_s start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ) + italic_d start_POSTSUBSCRIPT italic_j + 1 end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 2 ) - italic_d start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 1 , 0 ) end_CELL start_CELL italic_j = 0 , end_CELL end_ROW

which agrees with aj(N(E[1])a_{j}(N(E[1])italic_a start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_N ( italic_E [ 1 ] ) if N(E)=E[1]𝑁𝐸𝐸delimited-[]1N(E)=E[1]italic_N ( italic_E ) = italic_E [ 1 ] is embanked, but will still make sense if N(E)𝑁𝐸N(E)italic_N ( italic_E ) is only weakly embanked. Note that N(E)𝑁𝐸N(E)italic_N ( italic_E ) will fail to be embanked if and only if a0(N(E[1]))<0superscriptsubscript𝑎0𝑁𝐸delimited-[]10a_{0}^{\prime}(N(E[1]))<0italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ( italic_N ( italic_E [ 1 ] ) ) < 0; in this case, for TE[1]subscript𝑇𝐸delimited-[]1T_{E[1]}italic_T start_POSTSUBSCRIPT italic_E [ 1 ] end_POSTSUBSCRIPT after the second Halve rule, the quantity a0subscript𝑎0a_{0}italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT decrements to 11-1- 1 before n𝑛nitalic_n can decrement to 00, at which point a third Halve rule has to be applied. From the above expressions, we obtain

aj(N(E[1]))aj(E[1])superscriptsubscript𝑎𝑗𝑁𝐸delimited-[]1subscript𝑎𝑗𝐸delimited-[]1\displaystyle a_{j}^{\prime}(N(E[1]))-a_{j}(E[1])italic_a start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ( italic_N ( italic_E [ 1 ] ) ) - italic_a start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_E [ 1 ] ) ={(dj+1(h1,s2+2)dj+1(h1,s2))+(dj(h2+1,0)dj(h2,0))j1(dj+1(h1,s2+2)dj+1(h1,s2))(dj(h2+1,0)dj(h2,0))j=0absentcasessubscript𝑑𝑗1subscript1subscript𝑠22subscript𝑑𝑗1subscript1subscript𝑠2subscript𝑑𝑗subscript210subscript𝑑𝑗subscript20𝑗1subscript𝑑𝑗1subscript1subscript𝑠22subscript𝑑𝑗1subscript1subscript𝑠2subscript𝑑𝑗subscript210subscript𝑑𝑗subscript20𝑗0\displaystyle=\begin{cases}\left(d_{j+1}(h_{1},s_{2}+2)-d_{j+1}(h_{1},s_{2})% \right)+\left(d_{j}(h_{2}+1,0)-d_{j}(h_{2},0)\right)&j\geq 1\\ \left(d_{j+1}(h_{1},s_{2}+2)-d_{j+1}(h_{1},s_{2})\right)-\left(d_{j}(h_{2}+1,0% )-d_{j}(h_{2},0)\right)&j=0\end{cases}= { start_ROW start_CELL ( italic_d start_POSTSUBSCRIPT italic_j + 1 end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 2 ) - italic_d start_POSTSUBSCRIPT italic_j + 1 end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ) ) + ( italic_d start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 1 , 0 ) - italic_d start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT , 0 ) ) end_CELL start_CELL italic_j ≥ 1 end_CELL end_ROW start_ROW start_CELL ( italic_d start_POSTSUBSCRIPT italic_j + 1 end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 2 ) - italic_d start_POSTSUBSCRIPT italic_j + 1 end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ) ) - ( italic_d start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 1 , 0 ) - italic_d start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT , 0 ) ) end_CELL start_CELL italic_j = 0 end_CELL end_ROW
={dj+1(s2+2,s2)+dj(h2+1,h2)j1dj+1(s2+2,s2)dj(h2+1,h2)j=0absentcasessubscript𝑑𝑗1subscript𝑠22subscript𝑠2subscript𝑑𝑗subscript21subscript2𝑗1subscript𝑑𝑗1subscript𝑠22subscript𝑠2subscript𝑑𝑗subscript21subscript2𝑗0\displaystyle=\begin{cases}d_{j+1}(s_{2}+2,s_{2})+d_{j}(h_{2}+1,h_{2})&j\geq 1% \\ d_{j+1}(s_{2}+2,s_{2})-d_{j}(h_{2}+1,h_{2})&j=0\end{cases}= { start_ROW start_CELL italic_d start_POSTSUBSCRIPT italic_j + 1 end_POSTSUBSCRIPT ( italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 2 , italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ) + italic_d start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 1 , italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ) end_CELL start_CELL italic_j ≥ 1 end_CELL end_ROW start_ROW start_CELL italic_d start_POSTSUBSCRIPT italic_j + 1 end_POSTSUBSCRIPT ( italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 2 , italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ) - italic_d start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 1 , italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ) end_CELL start_CELL italic_j = 0 end_CELL end_ROW
={2dj(h2+1,h2)j10j=0absentcases2subscript𝑑𝑗subscript21subscript2𝑗10𝑗0\displaystyle=\begin{cases}2d_{j}(h_{2}+1,h_{2})&j\geq 1\\ 0&j=0\end{cases}= { start_ROW start_CELL 2 italic_d start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 1 , italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ) end_CELL start_CELL italic_j ≥ 1 end_CELL end_ROW start_ROW start_CELL 0 end_CELL start_CELL italic_j = 0 end_CELL end_ROW

where the first equality is justified by the fact that aj+2(Zero¯(E[1]))=aj+2(Zero¯(E))subscript𝑎𝑗2¯Zero𝐸delimited-[]1subscript𝑎𝑗2¯Zero𝐸a_{j+2}(\underline{\text{Zero}}(E[1]))=a_{j+2}(\underline{\text{Zero}}(E))italic_a start_POSTSUBSCRIPT italic_j + 2 end_POSTSUBSCRIPT ( under¯ start_ARG Zero end_ARG ( italic_E [ 1 ] ) ) = italic_a start_POSTSUBSCRIPT italic_j + 2 end_POSTSUBSCRIPT ( under¯ start_ARG Zero end_ARG ( italic_E ) ) by the definition of E[i]𝐸delimited-[]𝑖E[i]italic_E [ italic_i ], and the third equality is justified by verifying that dj+1(s2+2,s2)=dj(h2+1,h2)subscript𝑑𝑗1subscript𝑠22subscript𝑠2subscript𝑑𝑗subscript21subscript2d_{j+1}(s_{2}+2,s_{2})=d_{j}(h_{2}+1,h_{2})italic_d start_POSTSUBSCRIPT italic_j + 1 end_POSTSUBSCRIPT ( italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 2 , italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ) = italic_d start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 1 , italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ) always holds. We learn aj(N(E[1]))aj(E[1])0superscriptsubscript𝑎𝑗𝑁𝐸delimited-[]1subscript𝑎𝑗𝐸delimited-[]10a_{j}^{\prime}(N(E[1]))-a_{j}(E[1])\geq 0italic_a start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ( italic_N ( italic_E [ 1 ] ) ) - italic_a start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_E [ 1 ] ) ≥ 0, and therefore that N(E)𝑁𝐸N(E)italic_N ( italic_E ) is embanked. Moreover, we have exactly one index j[0,(E)]𝑗0𝐸j\in[0,\ell(E)]italic_j ∈ [ 0 , roman_ℓ ( italic_E ) ] such that N(E[1])=E[1][j]𝑁𝐸delimited-[]1𝐸delimited-[]1delimited-[]𝑗N(E[1])=E[1][j]italic_N ( italic_E [ 1 ] ) = italic_E [ 1 ] [ italic_j ]; this is the index for which dj(h2+1,h2)>0subscript𝑑𝑗subscript21subscript20d_{j}(h_{2}+1,h_{2})>0italic_d start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 1 , italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ) > 0. Such j𝑗jitalic_j is characterized by (h2+1)/2jsubscript21superscript2𝑗(h_{2}+1)/2^{j}( italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 1 ) / 2 start_POSTSUPERSCRIPT italic_j end_POSTSUPERSCRIPT being a half-integer, and this occurs precisely when ν2(h2+1)=j1subscript𝜈2subscript21𝑗1\nu_{2}(h_{2}+1)=j-1italic_ν start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 1 ) = italic_j - 1. The desired claim follows for the i=1𝑖1i=1italic_i = 1 case.

If i=0𝑖0i=0italic_i = 0, a completely analogous analysis occurs: we compute

aj(E[0])subscript𝑎𝑗𝐸delimited-[]0\displaystyle a_{j}(E[0])italic_a start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_E [ 0 ] ) ={aj+2(Zero¯(E))+dj+2(21,s1)+dj+1(h1,s2)+dj(h2,0)j1aj+2(Zero¯(E))+dj+2(21,s1)+dj+1(h1,s2)dj(h2,0)j=0,absentcasessubscript𝑎𝑗2¯Zero𝐸subscript𝑑𝑗2superscript21subscript𝑠1subscript𝑑𝑗1subscript1subscript𝑠2subscript𝑑𝑗subscript20𝑗1subscript𝑎𝑗2¯Zero𝐸subscript𝑑𝑗2superscript21subscript𝑠1subscript𝑑𝑗1subscript1subscript𝑠2subscript𝑑𝑗subscript20𝑗0\displaystyle=\begin{cases}a_{j+2}(\underline{\text{Zero}}(E))+d_{j+2}(2^{\ell% }-1,s_{1})+d_{j+1}(h_{1},s_{2})+d_{j}(h_{2},0)&j\geq 1\\ a_{j+2}(\underline{\text{Zero}}(E))+d_{j+2}(2^{\ell}-1,s_{1})+d_{j+1}(h_{1},s_% {2})-d_{j}(h_{2},0)&j=0,\end{cases}= { start_ROW start_CELL italic_a start_POSTSUBSCRIPT italic_j + 2 end_POSTSUBSCRIPT ( under¯ start_ARG Zero end_ARG ( italic_E ) ) + italic_d start_POSTSUBSCRIPT italic_j + 2 end_POSTSUBSCRIPT ( 2 start_POSTSUPERSCRIPT roman_ℓ end_POSTSUPERSCRIPT - 1 , italic_s start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ) + italic_d start_POSTSUBSCRIPT italic_j + 1 end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ) + italic_d start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT , 0 ) end_CELL start_CELL italic_j ≥ 1 end_CELL end_ROW start_ROW start_CELL italic_a start_POSTSUBSCRIPT italic_j + 2 end_POSTSUBSCRIPT ( under¯ start_ARG Zero end_ARG ( italic_E ) ) + italic_d start_POSTSUBSCRIPT italic_j + 2 end_POSTSUBSCRIPT ( 2 start_POSTSUPERSCRIPT roman_ℓ end_POSTSUPERSCRIPT - 1 , italic_s start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ) + italic_d start_POSTSUBSCRIPT italic_j + 1 end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ) - italic_d start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT , 0 ) end_CELL start_CELL italic_j = 0 , end_CELL end_ROW

and define

aj(N(E[0]))superscriptsubscript𝑎𝑗𝑁𝐸delimited-[]0\displaystyle a_{j}^{\prime}(N(E[0]))italic_a start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ( italic_N ( italic_E [ 0 ] ) ) :={aj+2(Zero¯(E[0]))+dj+2(21,s12)+dj+1(h11,s2)+dj(h2,0)j1aj+2(Zero¯(E[0]))+dj+2(21,s12)+dj+1(h11,s2)dj(h2,0)j=0,assignabsentcasessubscript𝑎𝑗2¯Zero𝐸delimited-[]0subscript𝑑𝑗2superscript21subscript𝑠12subscript𝑑𝑗1subscript11subscript𝑠2subscript𝑑𝑗subscript20𝑗1subscript𝑎𝑗2¯Zero𝐸delimited-[]0subscript𝑑𝑗2superscript21subscript𝑠12subscript𝑑𝑗1subscript11subscript𝑠2subscript𝑑𝑗subscript20𝑗0\displaystyle:=\begin{cases}a_{j+2}(\underline{\text{Zero}}(E[0]))+d_{j+2}(2^{% \ell}-1,s_{1}-2)+d_{j+1}(h_{1}-1,s_{2})+d_{j}(h_{2},0)&j\geq 1\\ a_{j+2}(\underline{\text{Zero}}(E[0]))+d_{j+2}(2^{\ell}-1,s_{1}-2)+d_{j+1}(h_{% 1}-1,s_{2})-d_{j}(h_{2},0)&j=0,\end{cases}:= { start_ROW start_CELL italic_a start_POSTSUBSCRIPT italic_j + 2 end_POSTSUBSCRIPT ( under¯ start_ARG Zero end_ARG ( italic_E [ 0 ] ) ) + italic_d start_POSTSUBSCRIPT italic_j + 2 end_POSTSUBSCRIPT ( 2 start_POSTSUPERSCRIPT roman_ℓ end_POSTSUPERSCRIPT - 1 , italic_s start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT - 2 ) + italic_d start_POSTSUBSCRIPT italic_j + 1 end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT - 1 , italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ) + italic_d start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT , 0 ) end_CELL start_CELL italic_j ≥ 1 end_CELL end_ROW start_ROW start_CELL italic_a start_POSTSUBSCRIPT italic_j + 2 end_POSTSUBSCRIPT ( under¯ start_ARG Zero end_ARG ( italic_E [ 0 ] ) ) + italic_d start_POSTSUBSCRIPT italic_j + 2 end_POSTSUBSCRIPT ( 2 start_POSTSUPERSCRIPT roman_ℓ end_POSTSUPERSCRIPT - 1 , italic_s start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT - 2 ) + italic_d start_POSTSUBSCRIPT italic_j + 1 end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT - 1 , italic_s start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ) - italic_d start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT , 0 ) end_CELL start_CELL italic_j = 0 , end_CELL end_ROW

so that for all j[0,]𝑗0j\in[0,\ell]italic_j ∈ [ 0 , roman_ℓ ], we have

aj(N(E[0]))aj(E[0])superscriptsubscript𝑎𝑗𝑁𝐸delimited-[]0subscript𝑎𝑗𝐸delimited-[]0\displaystyle a_{j}^{\prime}(N(E[0]))-a_{j}(E[0])italic_a start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ( italic_N ( italic_E [ 0 ] ) ) - italic_a start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_E [ 0 ] ) =dj+2(s12,s1)+dj+1(h11,h1)absentsubscript𝑑𝑗2subscript𝑠12subscript𝑠1subscript𝑑𝑗1subscript11subscript1\displaystyle=d_{j+2}(s_{1}-2,s_{1})+d_{j+1}(h_{1}-1,h_{1})= italic_d start_POSTSUBSCRIPT italic_j + 2 end_POSTSUBSCRIPT ( italic_s start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT - 2 , italic_s start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ) + italic_d start_POSTSUBSCRIPT italic_j + 1 end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT - 1 , italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT )
=2dj+1(h11,h1).absent2subscript𝑑𝑗1subscript11subscript1\displaystyle=2d_{j+1}(h_{1}-1,h_{1}).= 2 italic_d start_POSTSUBSCRIPT italic_j + 1 end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT - 1 , italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ) .

As in the i=1𝑖1i=1italic_i = 1 case, the fact that aj(N(E[0]))aj(E[0])0superscriptsubscript𝑎𝑗𝑁𝐸delimited-[]0subscript𝑎𝑗𝐸delimited-[]00a_{j}^{\prime}(N(E[0]))-a_{j}(E[0])\geq 0italic_a start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ( italic_N ( italic_E [ 0 ] ) ) - italic_a start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_E [ 0 ] ) ≥ 0 immediately implies that N(E)𝑁𝐸N(E)italic_N ( italic_E ) is embanked, and in fact aj(N(E[0]))aj(E[0])superscriptsubscript𝑎𝑗𝑁𝐸delimited-[]0subscript𝑎𝑗𝐸delimited-[]0a_{j}^{\prime}(N(E[0]))-a_{j}(E[0])italic_a start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ( italic_N ( italic_E [ 0 ] ) ) - italic_a start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_E [ 0 ] ) positive if and only if h1/2j+1subscript1superscript2𝑗1h_{1}/2^{j+1}italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT / 2 start_POSTSUPERSCRIPT italic_j + 1 end_POSTSUPERSCRIPT is a half-integer, which occurs precisely when ν2(h1)=jsubscript𝜈2subscript1𝑗\nu_{2}(h_{1})=jitalic_ν start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ) = italic_j. This completes the proof. ∎

In light of Proposition 3.6, we are induced to speed up the function N()𝑁N(\cdot)italic_N ( ⋅ ) to a new function N()superscript𝑁N^{\prime}(\cdot)italic_N start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ( ⋅ ):

Definition 3.7.

Define the following terms:

  1. (1)

    For an embanked state E𝐸Eitalic_E such that N(E)=E[i]𝑁𝐸𝐸delimited-[]𝑖N(E)=E[i]italic_N ( italic_E ) = italic_E [ italic_i ], define N(E)superscript𝑁𝐸N^{\prime}(E)italic_N start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ( italic_E ) to be the state

    N(E)superscript𝑁𝐸\displaystyle N^{\prime}(E)italic_N start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ( italic_E ) :=N(i(E)+1)/2(E)assignabsentsuperscript𝑁𝑖𝐸12𝐸\displaystyle:=N^{\lceil(i(E)+1)/2\rceil}(E):= italic_N start_POSTSUPERSCRIPT ⌈ ( italic_i ( italic_E ) + 1 ) / 2 ⌉ end_POSTSUPERSCRIPT ( italic_E )
    ={E[i][i2][3][1]ioddE[i][i2][2][0]ieven,absentcases𝐸delimited-[]𝑖delimited-[]𝑖2delimited-[]3delimited-[]1𝑖odd𝐸delimited-[]𝑖delimited-[]𝑖2delimited-[]2delimited-[]0𝑖even\displaystyle=\begin{cases}E[i][i-2]\cdots[3][1]&i\leavevmode\nobreak\ \text{% odd}\\ E[i][i-2]\cdots[2][0]&i\leavevmode\nobreak\ \text{even},\end{cases}= { start_ROW start_CELL italic_E [ italic_i ] [ italic_i - 2 ] ⋯ [ 3 ] [ 1 ] end_CELL start_CELL italic_i odd end_CELL end_ROW start_ROW start_CELL italic_E [ italic_i ] [ italic_i - 2 ] ⋯ [ 2 ] [ 0 ] end_CELL start_CELL italic_i even , end_CELL end_ROW

    where the second equality holds by Proposition 3.6.

  2. (2)

    Say that an embanked state E𝐸Eitalic_E is rooted embanked if it is the result of applying Nsuperscript𝑁N^{\prime}italic_N start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT to Sksubscript𝑆𝑘S_{k}italic_S start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT some amount of times, i.e. there exists e𝑒e\in\mathbb{N}italic_e ∈ blackboard_N such that E=(N)e(Sk)𝐸superscriptsuperscript𝑁𝑒subscript𝑆𝑘E=(N^{\prime})^{e}(S_{k})italic_E = ( italic_N start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) start_POSTSUPERSCRIPT italic_e end_POSTSUPERSCRIPT ( italic_S start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT ).

  3. (3)

    For i{0,1}𝑖01i\in\{0,1\}italic_i ∈ { 0 , 1 }, say that a rooted embanked state E𝐸Eitalic_E is i𝑖iitalic_i-rooted embanked if E=N1(E)[i]𝐸superscript𝑁1𝐸delimited-[]𝑖E=N^{-1}(E)[i]italic_E = italic_N start_POSTSUPERSCRIPT - 1 end_POSTSUPERSCRIPT ( italic_E ) [ italic_i ]. Every rooted embanked state is either 00-rooted embanked or 1111-rooted embanked.

  4. (4)

    For a state transition EE𝐸superscript𝐸E\to E^{\prime}italic_E → italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT of rooted embanked states, let TEEsuperscriptsubscript𝑇𝐸superscript𝐸T_{E\to E^{\prime}}^{\prime}italic_T start_POSTSUBSCRIPT italic_E → italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT denote the sequence of N𝑁Nitalic_N’s that were applied to E𝐸Eitalic_E to achieve Esuperscript𝐸E^{\prime}italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT.

We have the immediate corollary:

Corollary 3.8.

For i{0,1}𝑖01i\in\{0,1\}italic_i ∈ { 0 , 1 }, let E𝐸Eitalic_E be an i𝑖iitalic_i-rooted embanked state with h(N1(E))=(h1,h2)superscript𝑁1𝐸subscript1subscript2h(N^{-1}(E))=(h_{1},h_{2})italic_h ( italic_N start_POSTSUPERSCRIPT - 1 end_POSTSUPERSCRIPT ( italic_E ) ) = ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ), and assume that N(E)𝑁𝐸N(E)italic_N ( italic_E ) is weakly embanked. Then we have

N(E)𝑁𝐸\displaystyle N(E)italic_N ( italic_E ) ={E[ν2(h1)]i=0E[ν2(h2+1)+1]i=1,absentcases𝐸delimited-[]subscript𝜈2subscript1𝑖0𝐸delimited-[]subscript𝜈2subscript211𝑖1\displaystyle=\begin{cases}E[\nu_{2}(h_{1})]&i=0\\ E[\nu_{2}(h_{2}+1)+1]&i=1,\end{cases}= { start_ROW start_CELL italic_E [ italic_ν start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ) ] end_CELL start_CELL italic_i = 0 end_CELL end_ROW start_ROW start_CELL italic_E [ italic_ν start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 1 ) + 1 ] end_CELL start_CELL italic_i = 1 , end_CELL end_ROW

so that N(E)superscript𝑁𝐸N^{\prime}(E)italic_N start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ( italic_E ) is ν2(h1)¯¯subscript𝜈2subscript1\overline{\nu_{2}(h_{1})}over¯ start_ARG italic_ν start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ) end_ARG-rooted embanked if i=0𝑖0i=0italic_i = 0, and ν2(h2+1)+1¯¯subscript𝜈2subscript211\overline{\nu_{2}(h_{2}+1)+1}over¯ start_ARG italic_ν start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ( italic_h start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + 1 ) + 1 end_ARG-rooted embanked if i=1𝑖1i=1italic_i = 1.

4. Proof of nonhalting

Proposition 4.1.

Let E𝐸Eitalic_E be a 1111-rooted embanked state such that there exists m[0,22k2)𝑚0superscript22𝑘2m\in[0,2^{2k}-2)italic_m ∈ [ 0 , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - 2 ) of odd 2222-adic valuation such that h(N1(E))=(22km1,22k+m)superscript𝑁1𝐸superscript22𝑘𝑚1superscript22𝑘𝑚h(N^{-1}(E))=(2^{2k}-m-1,2^{2k}+m)italic_h ( italic_N start_POSTSUPERSCRIPT - 1 end_POSTSUPERSCRIPT ( italic_E ) ) = ( 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - italic_m - 1 , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT + italic_m ). Then the following hold:

  1. (1)

    If m>msuperscript𝑚𝑚m^{\prime}>mitalic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT > italic_m in [0,22k2]0superscript22𝑘2[0,2^{2k}-2][ 0 , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - 2 ] denotes the next number after m𝑚mitalic_m satisfying ν2(m)1mod2subscript𝜈2superscript𝑚modulo12\nu_{2}(m^{\prime})\equiv 1\bmod 2italic_ν start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ( italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) ≡ 1 roman_mod 2, then there exists a unique 1-rooted embanked state Esuperscript𝐸E^{\prime}italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT satisfying EEmaps-to𝐸superscript𝐸E\mapsto E^{\prime}italic_E ↦ italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT, such that h(N1(E))=(22km1,22k+m)superscript𝑁1superscript𝐸superscript22𝑘superscript𝑚1superscript22𝑘superscript𝑚h(N^{-1}(E^{\prime}))=(2^{2k}-m^{\prime}-1,2^{2k}+m^{\prime})italic_h ( italic_N start_POSTSUPERSCRIPT - 1 end_POSTSUPERSCRIPT ( italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) ) = ( 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - 1 , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT + italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ).

  2. (2)

    In the setting of (2), let d:=mmassign𝑑superscript𝑚𝑚d:=m^{\prime}-mitalic_d := italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - italic_m. Then ai(E)=ai(E)+2dsubscript𝑎𝑖superscript𝐸subscript𝑎𝑖𝐸2𝑑a_{i}(E^{\prime})=a_{i}(E)+2ditalic_a start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) = italic_a start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_E ) + 2 italic_d for i{0,1}𝑖01i\in\{0,1\}italic_i ∈ { 0 , 1 }.

Proof.

Suppose E𝐸Eitalic_E and m𝑚mitalic_m are as in the problem statement. In what follows, the quantities a1subscript𝑎1a_{1}italic_a start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT and a0subscript𝑎0a_{0}italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT never breach the bounds given by the conditions in Proposition 3.4; combining this with Corollary 3.8, it follows that all Nsuperscript𝑁N^{\prime}italic_N start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT-iterates of E𝐸Eitalic_E we consider will be rooted embanked.

We claim that for each e[0,mm1]𝑒0superscript𝑚𝑚1e\in[0,m^{\prime}-m-1]italic_e ∈ [ 0 , italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - italic_m - 1 ], Ee:=(N)e(E)assignsubscript𝐸𝑒superscriptsuperscript𝑁𝑒𝐸E_{e}:=(N^{\prime})^{e}(E)italic_E start_POSTSUBSCRIPT italic_e end_POSTSUBSCRIPT := ( italic_N start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) start_POSTSUPERSCRIPT italic_e end_POSTSUPERSCRIPT ( italic_E ) is 1111-rooted embanked with h(N1(Ee))=(22km1,22k+m+e)superscript𝑁1subscript𝐸𝑒superscript22𝑘𝑚1superscript22𝑘𝑚𝑒h(N^{-1}(E_{e}))=(2^{2k}-m-1,2^{2k}+m+e)italic_h ( italic_N start_POSTSUPERSCRIPT - 1 end_POSTSUPERSCRIPT ( italic_E start_POSTSUBSCRIPT italic_e end_POSTSUBSCRIPT ) ) = ( 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - italic_m - 1 , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT + italic_m + italic_e ). This follows by induction on e𝑒eitalic_e: the base case e=0𝑒0e=0italic_e = 0 is given, while for the induction step, if e<mm1𝑒superscript𝑚𝑚1e<m^{\prime}-m-1italic_e < italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - italic_m - 1 satisfies the induction hypothesis, then since m+e+1<m𝑚𝑒1superscript𝑚m+e+1<m^{\prime}italic_m + italic_e + 1 < italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT, it must necessarily have even valuation; hence by Corollary 3.8, Ee+1:=N(Ee)assignsubscript𝐸𝑒1superscript𝑁subscript𝐸𝑒E_{e+1}:=N^{\prime}(E_{e})italic_E start_POSTSUBSCRIPT italic_e + 1 end_POSTSUBSCRIPT := italic_N start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ( italic_E start_POSTSUBSCRIPT italic_e end_POSTSUBSCRIPT ) is ν2((m+e)+1)+1¯=1¯subscript𝜈2𝑚𝑒111\overline{\nu_{2}((m+e)+1)+1}=1over¯ start_ARG italic_ν start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ( ( italic_m + italic_e ) + 1 ) + 1 end_ARG = 1-rooted embanked, and moreover by Lemma 3.5 we have h(N1(Ee+1))=h(N1(Ee)[1])=(22km1,22k+m+e+1)superscript𝑁1subscript𝐸𝑒1superscript𝑁1subscript𝐸𝑒delimited-[]1superscript22𝑘𝑚1superscript22𝑘𝑚𝑒1h(N^{-1}(E_{e+1}))=h(N^{-1}(E_{e})[1])=(2^{2k}-m-1,2^{2k}+m+e+1)italic_h ( italic_N start_POSTSUPERSCRIPT - 1 end_POSTSUPERSCRIPT ( italic_E start_POSTSUBSCRIPT italic_e + 1 end_POSTSUBSCRIPT ) ) = italic_h ( italic_N start_POSTSUPERSCRIPT - 1 end_POSTSUPERSCRIPT ( italic_E start_POSTSUBSCRIPT italic_e end_POSTSUBSCRIPT ) [ 1 ] ) = ( 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - italic_m - 1 , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT + italic_m + italic_e + 1 ). This completes the induction. In addition, we also learn that from E𝐸Eitalic_E to Emm1subscript𝐸superscript𝑚𝑚1E_{m^{\prime}-m-1}italic_E start_POSTSUBSCRIPT italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - italic_m - 1 end_POSTSUBSCRIPT, the quantity a1subscript𝑎1a_{1}italic_a start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT increments by 2(mm1).2superscript𝑚𝑚12(m^{\prime}-m-1).2 ( italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - italic_m - 1 ) .

When we apply Nsuperscript𝑁N^{\prime}italic_N start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT to Emm1subscript𝐸superscript𝑚𝑚1E_{m^{\prime}-m-1}italic_E start_POSTSUBSCRIPT italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - italic_m - 1 end_POSTSUBSCRIPT, we obtain a state Esuperscript𝐸E^{\prime}italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT such that h(N1(E))=(22km1,22k+m)superscript𝑁1superscript𝐸superscript22𝑘𝑚1superscript22𝑘superscript𝑚h(N^{-1}(E^{\prime}))=(2^{2k}-m-1,2^{2k}+m^{\prime})italic_h ( italic_N start_POSTSUPERSCRIPT - 1 end_POSTSUPERSCRIPT ( italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) ) = ( 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - italic_m - 1 , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT + italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ). Since ν2((m1)+1)=ν2(m)subscript𝜈2superscript𝑚11subscript𝜈2superscript𝑚\nu_{2}((m^{\prime}-1)+1)=\nu_{2}(m^{\prime})italic_ν start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ( ( italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - 1 ) + 1 ) = italic_ν start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ( italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) is odd, it follows by Corollary 3.8 that E=N(Emm1)superscript𝐸superscript𝑁subscript𝐸superscript𝑚𝑚1E^{\prime}=N^{\prime}(E_{m^{\prime}-m-1})italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT = italic_N start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ( italic_E start_POSTSUBSCRIPT italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - italic_m - 1 end_POSTSUBSCRIPT ) is ν2((m1)+1)+1¯=0¯subscript𝜈2superscript𝑚1110\overline{\nu_{2}((m^{\prime}-1)+1)+1}=0over¯ start_ARG italic_ν start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ( ( italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - 1 ) + 1 ) + 1 end_ARG = 0-rooted. We claim that for each e[0,mm1]𝑒0superscript𝑚𝑚1e\in[0,m^{\prime}-m-1]italic_e ∈ [ 0 , italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - italic_m - 1 ], Ee:=(N)e(E)assignsuperscriptsubscript𝐸𝑒superscriptsuperscript𝑁𝑒superscript𝐸E_{e}^{\prime}:=(N^{\prime})^{e}(E^{\prime})italic_E start_POSTSUBSCRIPT italic_e end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT := ( italic_N start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) start_POSTSUPERSCRIPT italic_e end_POSTSUPERSCRIPT ( italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) is 00-rooted embanked with h(N1(Ee))=(22km1e,22k+m)superscript𝑁1superscriptsubscript𝐸𝑒superscript22𝑘𝑚1𝑒superscript22𝑘superscript𝑚h(N^{-1}(E_{e}^{\prime}))=(2^{2k}-m-1-e,2^{2k}+m^{\prime})italic_h ( italic_N start_POSTSUPERSCRIPT - 1 end_POSTSUPERSCRIPT ( italic_E start_POSTSUBSCRIPT italic_e end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) ) = ( 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - italic_m - 1 - italic_e , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT + italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ). This, again, follows by induction on e𝑒eitalic_e: the base case e=0𝑒0e=0italic_e = 0 is given, while for the induction step, if e<mm1𝑒superscript𝑚𝑚1e<m^{\prime}-m-1italic_e < italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - italic_m - 1 satisfies the induction hypothesis, then since m+e+1<m𝑚𝑒1superscript𝑚m+e+1<m^{\prime}italic_m + italic_e + 1 < italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT, it must necessarily have even valuation; hence by Corollary 3.8, Ee+1:=N(Ee)assignsuperscriptsubscript𝐸𝑒1superscript𝑁superscriptsubscript𝐸𝑒E_{e+1}^{\prime}:=N^{\prime}(E_{e}^{\prime})italic_E start_POSTSUBSCRIPT italic_e + 1 end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT := italic_N start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ( italic_E start_POSTSUBSCRIPT italic_e end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) is ν2(22km1e)¯=0¯subscript𝜈2superscript22𝑘𝑚1𝑒0\overline{\nu_{2}(2^{2k}-m-1-e)}=0over¯ start_ARG italic_ν start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ( 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - italic_m - 1 - italic_e ) end_ARG = 0-rooted embanked, and moreover by Lemma 3.5 we have h(N1(Ee+1))=h(N1(Ee)[0])=(22km2e,22k+m)superscript𝑁1superscriptsubscript𝐸𝑒1superscript𝑁1superscriptsubscript𝐸𝑒delimited-[]0superscript22𝑘𝑚2𝑒superscript22𝑘superscript𝑚h(N^{-1}(E_{e+1}^{\prime}))=h(N^{-1}(E_{e}^{\prime})[0])=(2^{2k}-m-2-e,2^{2k}+% m^{\prime})italic_h ( italic_N start_POSTSUPERSCRIPT - 1 end_POSTSUPERSCRIPT ( italic_E start_POSTSUBSCRIPT italic_e + 1 end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) ) = italic_h ( italic_N start_POSTSUPERSCRIPT - 1 end_POSTSUPERSCRIPT ( italic_E start_POSTSUBSCRIPT italic_e end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) [ 0 ] ) = ( 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - italic_m - 2 - italic_e , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT + italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ). This completes the induction. In addition, we also learn that from Emm1subscript𝐸superscript𝑚𝑚1E_{m^{\prime}-m-1}italic_E start_POSTSUBSCRIPT italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - italic_m - 1 end_POSTSUBSCRIPT to Emm1superscriptsubscript𝐸superscript𝑚𝑚1E_{m^{\prime}-m-1}^{\prime}italic_E start_POSTSUBSCRIPT italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - italic_m - 1 end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT, the quantity a0subscript𝑎0a_{0}italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT decrements by 2(mm).2superscript𝑚𝑚2(m^{\prime}-m).2 ( italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - italic_m ) .

Finally, applying Nsuperscript𝑁N^{\prime}italic_N start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT to Emm1superscriptsubscript𝐸superscript𝑚𝑚1E_{m^{\prime}-m-1}^{\prime}italic_E start_POSTSUBSCRIPT italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - italic_m - 1 end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT yields a state E′′superscript𝐸′′E^{\prime\prime}italic_E start_POSTSUPERSCRIPT ′ ′ end_POSTSUPERSCRIPT such that h(N1(E′′))=(22km1,22k+m)superscript𝑁1superscript𝐸′′superscript22𝑘superscript𝑚1superscript22𝑘superscript𝑚h(N^{-1}(E^{\prime\prime}))=(2^{2k}-m^{\prime}-1,2^{2k}+m^{\prime})italic_h ( italic_N start_POSTSUPERSCRIPT - 1 end_POSTSUPERSCRIPT ( italic_E start_POSTSUPERSCRIPT ′ ′ end_POSTSUPERSCRIPT ) ) = ( 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - 1 , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT + italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ), and E′′superscript𝐸′′E^{\prime\prime}italic_E start_POSTSUPERSCRIPT ′ ′ end_POSTSUPERSCRIPT is ν2(22km)¯=1¯subscript𝜈2superscript22𝑘superscript𝑚1\overline{\nu_{2}(2^{2k}-m^{\prime})}=1over¯ start_ARG italic_ν start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ( 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) end_ARG = 1-rooted embanked, which proves (1). This extra application of Nsuperscript𝑁N^{\prime}italic_N start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT also increments a1subscript𝑎1a_{1}italic_a start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT by 2222, so in total, a1subscript𝑎1a_{1}italic_a start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT has incremented by 2(mm1)+2=2d2superscript𝑚𝑚122𝑑2(m^{\prime}-m-1)+2=2d2 ( italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - italic_m - 1 ) + 2 = 2 italic_d, while a0subscript𝑎0a_{0}italic_a start_POSTSUBSCRIPT 0 end_POSTSUBSCRIPT has decremented by 2(mm)=2d2superscript𝑚𝑚2𝑑2(m^{\prime}-m)=2d2 ( italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - italic_m ) = 2 italic_d; this proves (2). ∎

Starting with Sk=(0,2,22,,22k,0)subscript𝑆𝑘02superscript22superscript22𝑘0S_{k}=(0,2,2^{2},\dots,2^{2k},0)italic_S start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT = ( 0 , 2 , 2 start_POSTSUPERSCRIPT 2 end_POSTSUPERSCRIPT , … , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT , 0 ), a brief computation yields h(Sk)=(22k1,22k)subscript𝑆𝑘superscript22𝑘1superscript22𝑘h(S_{k})=(2^{2k}-1,2^{2k})italic_h ( italic_S start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT ) = ( 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - 1 , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT ) and N(Sk)=Sk[2k+1]𝑁subscript𝑆𝑘subscript𝑆𝑘delimited-[]2𝑘1N(S_{k})=S_{k}[2k+1]italic_N ( italic_S start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT ) = italic_S start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT [ 2 italic_k + 1 ]. Thus, applying Nsuperscript𝑁N^{\prime}italic_N start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT to Sksubscript𝑆𝑘S_{k}italic_S start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT five times yields a 1111-rooted embanked state E:=(N)5(Sk)assign𝐸superscriptsuperscript𝑁5subscript𝑆𝑘E:=(N^{\prime})^{5}(S_{k})italic_E := ( italic_N start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) start_POSTSUPERSCRIPT 5 end_POSTSUPERSCRIPT ( italic_S start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT ) such that h(N1(E))=(22k3,22k+2)superscript𝑁1𝐸superscript22𝑘3superscript22𝑘2h(N^{-1}(E))=(2^{2k}-3,2^{2k}+2)italic_h ( italic_N start_POSTSUPERSCRIPT - 1 end_POSTSUPERSCRIPT ( italic_E ) ) = ( 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - 3 , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT + 2 ). Hence, by inducting on m𝑚mitalic_m to reach m=22k2𝑚superscript22𝑘2m=2^{2k}-2italic_m = 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - 2, Proposition 4.1 and Proposition 3.4 imply the following corollary:

Corollary 4.2.

There exists a rooted embanked state E𝐸Eitalic_E such that h(N1(E))=(1,22k+12)superscript𝑁1𝐸1superscript22𝑘12h(N^{-1}(E))=(1,2^{2k+1}-2)italic_h ( italic_N start_POSTSUPERSCRIPT - 1 end_POSTSUPERSCRIPT ( italic_E ) ) = ( 1 , 2 start_POSTSUPERSCRIPT 2 italic_k + 1 end_POSTSUPERSCRIPT - 2 ).

4.1. Counting increments

For rooted embanked states EEmaps-to𝐸superscript𝐸E\mapsto E^{\prime}italic_E ↦ italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT, let κEE(j)subscript𝜅𝐸superscript𝐸𝑗\kappa_{E\to E^{\prime}}(j)italic_κ start_POSTSUBSCRIPT italic_E → italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT end_POSTSUBSCRIPT ( italic_j ) denote the number of N:SN(S):𝑁maps-to𝑆𝑁𝑆N\colon S\mapsto N(S)italic_N : italic_S ↦ italic_N ( italic_S ) in TEEsuperscriptsubscript𝑇𝐸superscript𝐸T_{E\to E^{\prime}}^{\prime}italic_T start_POSTSUBSCRIPT italic_E → italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT such that N(S)=S[j]𝑁𝑆𝑆delimited-[]𝑗N(S)=S[j]italic_N ( italic_S ) = italic_S [ italic_j ].

Proposition 4.3.

Suppose we are in the setting of Proposition 4.1, with E𝐸Eitalic_E, Esuperscript𝐸E^{\prime}italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT, m𝑚mitalic_m and msuperscript𝑚m^{\prime}italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT defined as before. Then, for all j[0,2k+1]𝑗02𝑘1j\in[0,2k+1]italic_j ∈ [ 0 , 2 italic_k + 1 ], we have κEE(j)=#{e[m+1,m]:max(1,2j1)e}subscript𝜅𝐸superscript𝐸𝑗#conditional-set𝑒𝑚1superscript𝑚conditional1superscript2𝑗1𝑒\kappa_{E\to E^{\prime}}(j)=\#\{e\in[m+1,m^{\prime}]\colon\max(1,2^{j-1})\mid e\}italic_κ start_POSTSUBSCRIPT italic_E → italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT end_POSTSUBSCRIPT ( italic_j ) = # { italic_e ∈ [ italic_m + 1 , italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ] : roman_max ( 1 , 2 start_POSTSUPERSCRIPT italic_j - 1 end_POSTSUPERSCRIPT ) ∣ italic_e }.

Proof.

For a statement X𝑋Xitalic_X, define δ(X)𝛿𝑋\delta(X)italic_δ ( italic_X ) to be 1111 if X𝑋Xitalic_X is true, and 00 if X𝑋Xitalic_X is false. Fix a j[0,2k+1]𝑗02𝑘1j\in[0,2k+1]italic_j ∈ [ 0 , 2 italic_k + 1 ]. By Corollary 3.8, we have

κEE(j)subscript𝜅𝐸superscript𝐸𝑗\displaystyle\kappa_{E\to E^{\prime}}(j)italic_κ start_POSTSUBSCRIPT italic_E → italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT end_POSTSUBSCRIPT ( italic_j ) ={δ(ν2((m1)+1)+1j)+#{e[m+1,m1]:ν2(e)j}j0mod2#{e[m,m2]:ν2(e+1)+1j}+δ(ν2(m)j)j1mod2absentcases𝛿subscript𝜈2superscript𝑚111𝑗#conditional-set𝑒𝑚1superscript𝑚1subscript𝜈2𝑒𝑗𝑗modulo02#conditional-set𝑒𝑚superscript𝑚2subscript𝜈2𝑒11𝑗𝛿subscript𝜈2superscript𝑚𝑗𝑗modulo12\displaystyle=\begin{cases}\delta(\nu_{2}((m^{\prime}-1)+1)+1\geq j)+\#\{e\in[% m+1,m^{\prime}-1]\colon\nu_{2}(e)\geq j\}&j\equiv 0\bmod 2\\ \#\{e\in[m,m^{\prime}-2]\colon\nu_{2}(e+1)+1\geq j\}+\delta(\nu_{2}(m^{\prime}% )\geq j)&j\equiv 1\bmod 2\end{cases}= { start_ROW start_CELL italic_δ ( italic_ν start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ( ( italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - 1 ) + 1 ) + 1 ≥ italic_j ) + # { italic_e ∈ [ italic_m + 1 , italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - 1 ] : italic_ν start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ( italic_e ) ≥ italic_j } end_CELL start_CELL italic_j ≡ 0 roman_mod 2 end_CELL end_ROW start_ROW start_CELL # { italic_e ∈ [ italic_m , italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - 2 ] : italic_ν start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ( italic_e + 1 ) + 1 ≥ italic_j } + italic_δ ( italic_ν start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ( italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) ≥ italic_j ) end_CELL start_CELL italic_j ≡ 1 roman_mod 2 end_CELL end_ROW
={δ(2j1m)+#{e[m+1,m1]:2je}j0mod2#{e[m+1,m1]:2j1e}+δ(2jm)j1mod2absentcases𝛿conditionalsuperscript2𝑗1superscript𝑚#conditional-set𝑒𝑚1superscript𝑚1conditionalsuperscript2𝑗𝑒𝑗modulo02#conditional-set𝑒𝑚1superscript𝑚1conditionalsuperscript2𝑗1𝑒𝛿conditionalsuperscript2𝑗superscript𝑚𝑗modulo12\displaystyle=\begin{cases}\delta(2^{j-1}\mid m^{\prime})+\#\{e\in[m+1,m^{% \prime}-1]\colon 2^{j}\mid e\}&j\equiv 0\bmod 2\\ \#\{e\in[m+1,m^{\prime}-1]\colon 2^{j-1}\mid e\}+\delta(2^{j}\mid m^{\prime})&% j\equiv 1\bmod 2\end{cases}= { start_ROW start_CELL italic_δ ( 2 start_POSTSUPERSCRIPT italic_j - 1 end_POSTSUPERSCRIPT ∣ italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) + # { italic_e ∈ [ italic_m + 1 , italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - 1 ] : 2 start_POSTSUPERSCRIPT italic_j end_POSTSUPERSCRIPT ∣ italic_e } end_CELL start_CELL italic_j ≡ 0 roman_mod 2 end_CELL end_ROW start_ROW start_CELL # { italic_e ∈ [ italic_m + 1 , italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - 1 ] : 2 start_POSTSUPERSCRIPT italic_j - 1 end_POSTSUPERSCRIPT ∣ italic_e } + italic_δ ( 2 start_POSTSUPERSCRIPT italic_j end_POSTSUPERSCRIPT ∣ italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) end_CELL start_CELL italic_j ≡ 1 roman_mod 2 end_CELL end_ROW
={δ(2j1m)+#{e[m+1,m1]:2j1e}j0mod2#{e[m+1,m1]:2j1e}+δ(2j1m)j1mod2absentcases𝛿conditionalsuperscript2𝑗1superscript𝑚#conditional-set𝑒𝑚1superscript𝑚1conditionalsuperscript2𝑗1𝑒𝑗modulo02#conditional-set𝑒𝑚1superscript𝑚1conditionalsuperscript2𝑗1𝑒𝛿conditionalsuperscript2𝑗1superscript𝑚𝑗modulo12\displaystyle=\begin{cases}\delta(2^{j-1}\mid m^{\prime})+\#\{e\in[m+1,m^{% \prime}-1]\colon 2^{j-1}\mid e\}&j\equiv 0\bmod 2\\ \#\{e\in[m+1,m^{\prime}-1]\colon 2^{j-1}\mid e\}+\delta(2^{j-1}\mid m^{\prime}% )&j\equiv 1\bmod 2\end{cases}= { start_ROW start_CELL italic_δ ( 2 start_POSTSUPERSCRIPT italic_j - 1 end_POSTSUPERSCRIPT ∣ italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) + # { italic_e ∈ [ italic_m + 1 , italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - 1 ] : 2 start_POSTSUPERSCRIPT italic_j - 1 end_POSTSUPERSCRIPT ∣ italic_e } end_CELL start_CELL italic_j ≡ 0 roman_mod 2 end_CELL end_ROW start_ROW start_CELL # { italic_e ∈ [ italic_m + 1 , italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT - 1 ] : 2 start_POSTSUPERSCRIPT italic_j - 1 end_POSTSUPERSCRIPT ∣ italic_e } + italic_δ ( 2 start_POSTSUPERSCRIPT italic_j - 1 end_POSTSUPERSCRIPT ∣ italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) end_CELL start_CELL italic_j ≡ 1 roman_mod 2 end_CELL end_ROW
=#{e[m+1,m]:2j1e},absent#conditional-set𝑒𝑚1superscript𝑚conditionalsuperscript2𝑗1𝑒\displaystyle=\#\{e\in[m+1,m^{\prime}]\colon 2^{j-1}\mid e\},= # { italic_e ∈ [ italic_m + 1 , italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ] : 2 start_POSTSUPERSCRIPT italic_j - 1 end_POSTSUPERSCRIPT ∣ italic_e } ,

where the third equality is using the fact that m𝑚mitalic_m and msuperscript𝑚m^{\prime}italic_m start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT have odd 2222-adic valuations, but every number in between has even 2222-adic valuation. ∎

4.2. Endgame

Our setup for the end of the proof is the sequence of state transitions SkEEE′′subscript𝑆𝑘𝐸superscript𝐸superscript𝐸′′S_{k}\to E\to E^{\prime}\to E^{\prime\prime}italic_S start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT → italic_E → italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT → italic_E start_POSTSUPERSCRIPT ′ ′ end_POSTSUPERSCRIPT, where E𝐸Eitalic_E, Esuperscript𝐸E^{\prime}italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT and E′′superscript𝐸′′E^{\prime\prime}italic_E start_POSTSUPERSCRIPT ′ ′ end_POSTSUPERSCRIPT are all rooted embanked states satisfying h(N1(E))=(22k3,22k+2)superscript𝑁1𝐸superscript22𝑘3superscript22𝑘2h(N^{-1}(E))=(2^{2k}-3,2^{2k}+2)italic_h ( italic_N start_POSTSUPERSCRIPT - 1 end_POSTSUPERSCRIPT ( italic_E ) ) = ( 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - 3 , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT + 2 ), h(N1(E))=(1,22k+12)superscript𝑁1superscript𝐸1superscript22𝑘12h(N^{-1}(E^{\prime}))=(1,2^{2k+1}-2)italic_h ( italic_N start_POSTSUPERSCRIPT - 1 end_POSTSUPERSCRIPT ( italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) ) = ( 1 , 2 start_POSTSUPERSCRIPT 2 italic_k + 1 end_POSTSUPERSCRIPT - 2 ) and h(N1(E′′))=(1,22k+11)superscript𝑁1superscript𝐸′′1superscript22𝑘11h(N^{-1}(E^{\prime\prime}))=(1,2^{2k+1}-1)italic_h ( italic_N start_POSTSUPERSCRIPT - 1 end_POSTSUPERSCRIPT ( italic_E start_POSTSUPERSCRIPT ′ ′ end_POSTSUPERSCRIPT ) ) = ( 1 , 2 start_POSTSUPERSCRIPT 2 italic_k + 1 end_POSTSUPERSCRIPT - 1 ). In particular, we have EE′′superscript𝐸superscript𝐸′′E^{\prime}\to E^{\prime\prime}italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT → italic_E start_POSTSUPERSCRIPT ′ ′ end_POSTSUPERSCRIPT since Proposition 4.1(2) guarantees that Esuperscript𝐸E^{\prime}italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT will satisfy the bounds in Proposition 3.4 so that Esuperscript𝐸E^{\prime}italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT is weakly embanked, and then Corollary 3.8 implies that Esuperscript𝐸E^{\prime}italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT is embanked. Also, we have E=(N)5(Sk)𝐸superscriptsuperscript𝑁5subscript𝑆𝑘E=(N^{\prime})^{5}(S_{k})italic_E = ( italic_N start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) start_POSTSUPERSCRIPT 5 end_POSTSUPERSCRIPT ( italic_S start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT ). An explicit computation yields

κSkE(j)subscript𝜅subscript𝑆𝑘𝐸𝑗\displaystyle\kappa_{S_{k}\to E}(j)italic_κ start_POSTSUBSCRIPT italic_S start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT → italic_E end_POSTSUBSCRIPT ( italic_j ) ={2j=03j=11j=2j¯3j2k+1,absentcases2𝑗03𝑗11𝑗2¯𝑗3𝑗2𝑘1\displaystyle=\begin{cases}2&j=0\\ 3&j=1\\ 1&j=2\\ \bar{j}&3\leq j\leq 2k+1,\end{cases}= { start_ROW start_CELL 2 end_CELL start_CELL italic_j = 0 end_CELL end_ROW start_ROW start_CELL 3 end_CELL start_CELL italic_j = 1 end_CELL end_ROW start_ROW start_CELL 1 end_CELL start_CELL italic_j = 2 end_CELL end_ROW start_ROW start_CELL over¯ start_ARG italic_j end_ARG end_CELL start_CELL 3 ≤ italic_j ≤ 2 italic_k + 1 , end_CELL end_ROW
κEE(j)subscript𝜅𝐸superscript𝐸𝑗\displaystyle\kappa_{E\to E^{\prime}}(j)italic_κ start_POSTSUBSCRIPT italic_E → italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT end_POSTSUBSCRIPT ( italic_j ) =#{e[3,22k2]:2j1e}absent#conditional-set𝑒3superscript22𝑘2conditionalsuperscript2𝑗1𝑒\displaystyle=\#\{e\in[3,2^{2k}-2]\colon 2^{j-1}\mid e\}= # { italic_e ∈ [ 3 , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - 2 ] : 2 start_POSTSUPERSCRIPT italic_j - 1 end_POSTSUPERSCRIPT ∣ italic_e }
={22k4j=0,122k12j=222kj+11j[3,2k]0j=2k+1,absentcasessuperscript22𝑘4𝑗01superscript22𝑘12𝑗2superscript22𝑘𝑗11𝑗32𝑘0𝑗2𝑘1\displaystyle=\begin{cases}2^{2k}-4&j=0,1\\ 2^{2k-1}-2&j=2\\ 2^{2k-j+1}-1&j\in[3,2k]\\ 0&j=2k+1,\end{cases}= { start_ROW start_CELL 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - 4 end_CELL start_CELL italic_j = 0 , 1 end_CELL end_ROW start_ROW start_CELL 2 start_POSTSUPERSCRIPT 2 italic_k - 1 end_POSTSUPERSCRIPT - 2 end_CELL start_CELL italic_j = 2 end_CELL end_ROW start_ROW start_CELL 2 start_POSTSUPERSCRIPT 2 italic_k - italic_j + 1 end_POSTSUPERSCRIPT - 1 end_CELL start_CELL italic_j ∈ [ 3 , 2 italic_k ] end_CELL end_ROW start_ROW start_CELL 0 end_CELL start_CELL italic_j = 2 italic_k + 1 , end_CELL end_ROW
κEE′′(j)subscript𝜅superscript𝐸superscript𝐸′′𝑗\displaystyle\kappa_{E^{\prime}\to E^{\prime\prime}}(j)italic_κ start_POSTSUBSCRIPT italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT → italic_E start_POSTSUPERSCRIPT ′ ′ end_POSTSUPERSCRIPT end_POSTSUBSCRIPT ( italic_j ) ={1j=10j1.absentcases1𝑗10𝑗1\displaystyle=\begin{cases}1&j=1\\ 0&j\neq 1.\end{cases}= { start_ROW start_CELL 1 end_CELL start_CELL italic_j = 1 end_CELL end_ROW start_ROW start_CELL 0 end_CELL start_CELL italic_j ≠ 1 . end_CELL end_ROW

It follows that

κSkE′′(j)subscript𝜅subscript𝑆𝑘superscript𝐸′′𝑗\displaystyle\kappa_{S_{k}\to E^{\prime\prime}}(j)italic_κ start_POSTSUBSCRIPT italic_S start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT → italic_E start_POSTSUPERSCRIPT ′ ′ end_POSTSUPERSCRIPT end_POSTSUBSCRIPT ( italic_j ) =κSkE(j)+κEE(j)+κEE′′(j)absentsubscript𝜅subscript𝑆𝑘𝐸𝑗subscript𝜅𝐸superscript𝐸𝑗subscript𝜅superscript𝐸superscript𝐸′′𝑗\displaystyle=\kappa_{S_{k}\to E}(j)+\kappa_{E\to E^{\prime}}(j)+\kappa_{E^{% \prime}\to E^{\prime\prime}}(j)= italic_κ start_POSTSUBSCRIPT italic_S start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT → italic_E end_POSTSUBSCRIPT ( italic_j ) + italic_κ start_POSTSUBSCRIPT italic_E → italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT end_POSTSUBSCRIPT ( italic_j ) + italic_κ start_POSTSUBSCRIPT italic_E start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT → italic_E start_POSTSUPERSCRIPT ′ ′ end_POSTSUPERSCRIPT end_POSTSUBSCRIPT ( italic_j )
={22k2j=022kj=122kj+11+j¯j[2,2k]1j=2k+1.absentcasessuperscript22𝑘2𝑗0superscript22𝑘𝑗1superscript22𝑘𝑗11¯𝑗𝑗22𝑘1𝑗2𝑘1\displaystyle=\begin{cases}2^{2k}-2&j=0\\ 2^{2k}&j=1\\ 2^{2k-j+1}-1+\overline{j}&j\in[2,2k]\\ 1&j=2k+1.\end{cases}= { start_ROW start_CELL 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - 2 end_CELL start_CELL italic_j = 0 end_CELL end_ROW start_ROW start_CELL 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT end_CELL start_CELL italic_j = 1 end_CELL end_ROW start_ROW start_CELL 2 start_POSTSUPERSCRIPT 2 italic_k - italic_j + 1 end_POSTSUPERSCRIPT - 1 + over¯ start_ARG italic_j end_ARG end_CELL start_CELL italic_j ∈ [ 2 , 2 italic_k ] end_CELL end_ROW start_ROW start_CELL 1 end_CELL start_CELL italic_j = 2 italic_k + 1 . end_CELL end_ROW

Since moving from S𝑆Sitalic_S to S[j]𝑆delimited-[]𝑗S[j]italic_S [ italic_j ] increments ajsubscript𝑎𝑗a_{j}italic_a start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT by 2222, we obtain

aj(E′′)subscript𝑎𝑗superscript𝐸′′\displaystyle a_{j}(E^{\prime\prime})italic_a start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_E start_POSTSUPERSCRIPT ′ ′ end_POSTSUPERSCRIPT ) =aj(Sk)+2κSkE′′(j)absentsubscript𝑎𝑗subscript𝑆𝑘2subscript𝜅subscript𝑆𝑘superscript𝐸′′𝑗\displaystyle=a_{j}(S_{k})+2\kappa_{S_{k}\to E^{\prime\prime}}(j)= italic_a start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_S start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT ) + 2 italic_κ start_POSTSUBSCRIPT italic_S start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT → italic_E start_POSTSUPERSCRIPT ′ ′ end_POSTSUPERSCRIPT end_POSTSUBSCRIPT ( italic_j )
={22k+14j=0322kj=1322kj+12+2j¯j[2,2k]2j=2k+1.absentcasessuperscript22𝑘14𝑗03superscript22𝑘𝑗13superscript22𝑘𝑗122¯𝑗𝑗22𝑘2𝑗2𝑘1\displaystyle=\begin{cases}2^{2k+1}-4&j=0\\ 3\cdot 2^{2k}&j=1\\ 3\cdot 2^{2k-j+1}-2+2\overline{j}&j\in[2,2k]\\ 2&j=2k+1.\end{cases}= { start_ROW start_CELL 2 start_POSTSUPERSCRIPT 2 italic_k + 1 end_POSTSUPERSCRIPT - 4 end_CELL start_CELL italic_j = 0 end_CELL end_ROW start_ROW start_CELL 3 ⋅ 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT end_CELL start_CELL italic_j = 1 end_CELL end_ROW start_ROW start_CELL 3 ⋅ 2 start_POSTSUPERSCRIPT 2 italic_k - italic_j + 1 end_POSTSUPERSCRIPT - 2 + 2 over¯ start_ARG italic_j end_ARG end_CELL start_CELL italic_j ∈ [ 2 , 2 italic_k ] end_CELL end_ROW start_ROW start_CELL 2 end_CELL start_CELL italic_j = 2 italic_k + 1 . end_CELL end_ROW

Observe that E′′superscript𝐸′′E^{\prime\prime}italic_E start_POSTSUPERSCRIPT ′ ′ end_POSTSUPERSCRIPT fails the conditions of Proposition 3.4, and so it will not make sense to apply N𝑁Nitalic_N anymore. We resort to an explicit analysis from here. From the state E′′superscript𝐸′′E^{\prime\prime}italic_E start_POSTSUPERSCRIPT ′ ′ end_POSTSUPERSCRIPT, applying Zero yields

(0,0,3,3212,322,3232,,322k12,322k,22k+15)0033superscript2123superscript223superscript2323superscript22𝑘123superscript22𝑘superscript22𝑘15\displaystyle(0,0,3,3\cdot 2^{1}-2,3\cdot 2^{2},3\cdot 2^{3}-2,\dots,3\cdot 2^% {2k-1}-2,3\cdot 2^{2k},2^{2k+1}-5)( 0 , 0 , 3 , 3 ⋅ 2 start_POSTSUPERSCRIPT 1 end_POSTSUPERSCRIPT - 2 , 3 ⋅ 2 start_POSTSUPERSCRIPT 2 end_POSTSUPERSCRIPT , 3 ⋅ 2 start_POSTSUPERSCRIPT 3 end_POSTSUPERSCRIPT - 2 , … , 3 ⋅ 2 start_POSTSUPERSCRIPT 2 italic_k - 1 end_POSTSUPERSCRIPT - 2 , 3 ⋅ 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT , 2 start_POSTSUPERSCRIPT 2 italic_k + 1 end_POSTSUPERSCRIPT - 5 ) (n,σ)=(22k+11,1)𝑛𝜎superscript22𝑘111\displaystyle(n,\sigma)=(2^{2k+1}-1,-1)( italic_n , italic_σ ) = ( 2 start_POSTSUPERSCRIPT 2 italic_k + 1 end_POSTSUPERSCRIPT - 1 , - 1 )

after which applying 22k+14superscript22𝑘142^{2k+1}-42 start_POSTSUPERSCRIPT 2 italic_k + 1 end_POSTSUPERSCRIPT - 4 Increment rules yields

(0,0,22,232,24,252,,22k12,22k,22k+13,22k+22,1)00superscript22superscript232superscript24superscript252superscript22𝑘12superscript22𝑘superscript22𝑘13superscript22𝑘221\displaystyle(0,0,2^{2},2^{3}-2,2^{4},2^{5}-2,\dots,2^{2k-1}-2,2^{2k},2^{2k+1}% -3,2^{2k+2}-2,-1)( 0 , 0 , 2 start_POSTSUPERSCRIPT 2 end_POSTSUPERSCRIPT , 2 start_POSTSUPERSCRIPT 3 end_POSTSUPERSCRIPT - 2 , 2 start_POSTSUPERSCRIPT 4 end_POSTSUPERSCRIPT , 2 start_POSTSUPERSCRIPT 5 end_POSTSUPERSCRIPT - 2 , … , 2 start_POSTSUPERSCRIPT 2 italic_k - 1 end_POSTSUPERSCRIPT - 2 , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT , 2 start_POSTSUPERSCRIPT 2 italic_k + 1 end_POSTSUPERSCRIPT - 3 , 2 start_POSTSUPERSCRIPT 2 italic_k + 2 end_POSTSUPERSCRIPT - 2 , - 1 ) (n,σ)=(3,1),𝑛𝜎31\displaystyle(n,\sigma)=(3,-1),( italic_n , italic_σ ) = ( 3 , - 1 ) ,

and now we Halve to obtain

(0,0,22,232,24,252,,22k12,22k,22k+13,22k+22).00superscript22superscript232superscript24superscript252superscript22𝑘12superscript22𝑘superscript22𝑘13superscript22𝑘22\displaystyle(0,0,2^{2},2^{3}-2,2^{4},2^{5}-2,\dots,2^{2k-1}-2,2^{2k},2^{2k+1}% -3,2^{2k+2}-2).( 0 , 0 , 2 start_POSTSUPERSCRIPT 2 end_POSTSUPERSCRIPT , 2 start_POSTSUPERSCRIPT 3 end_POSTSUPERSCRIPT - 2 , 2 start_POSTSUPERSCRIPT 4 end_POSTSUPERSCRIPT , 2 start_POSTSUPERSCRIPT 5 end_POSTSUPERSCRIPT - 2 , … , 2 start_POSTSUPERSCRIPT 2 italic_k - 1 end_POSTSUPERSCRIPT - 2 , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT , 2 start_POSTSUPERSCRIPT 2 italic_k + 1 end_POSTSUPERSCRIPT - 3 , 2 start_POSTSUPERSCRIPT 2 italic_k + 2 end_POSTSUPERSCRIPT - 2 ) . (n,σ)=(1,+1).𝑛𝜎11\displaystyle(n,\sigma)=(1,+1).( italic_n , italic_σ ) = ( 1 , + 1 ) .

Applying 22k+22superscript22𝑘222^{2k+2}-22 start_POSTSUPERSCRIPT 2 italic_k + 2 end_POSTSUPERSCRIPT - 2 Increment rules yields

(1,2,23,242,25,262,,22k2,22k+1,22k+24,0)12superscript23superscript242superscript25superscript262superscript22𝑘2superscript22𝑘1superscript22𝑘240\displaystyle(1,2,2^{3},2^{4}-2,2^{5},2^{6}-2,\dots,2^{2k}-2,2^{2k+1},2^{2k+2}% -4,0)( 1 , 2 , 2 start_POSTSUPERSCRIPT 3 end_POSTSUPERSCRIPT , 2 start_POSTSUPERSCRIPT 4 end_POSTSUPERSCRIPT - 2 , 2 start_POSTSUPERSCRIPT 5 end_POSTSUPERSCRIPT , 2 start_POSTSUPERSCRIPT 6 end_POSTSUPERSCRIPT - 2 , … , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - 2 , 2 start_POSTSUPERSCRIPT 2 italic_k + 1 end_POSTSUPERSCRIPT , 2 start_POSTSUPERSCRIPT 2 italic_k + 2 end_POSTSUPERSCRIPT - 4 , 0 ) (n,σ)=(22k+21,+1)𝑛𝜎superscript22𝑘211\displaystyle(n,\sigma)=(2^{2k+2}-1,+1)( italic_n , italic_σ ) = ( 2 start_POSTSUPERSCRIPT 2 italic_k + 2 end_POSTSUPERSCRIPT - 1 , + 1 )

after which we are forced to apply an Overflow rule to get

Ek,final:=(0,2,2,23,242,,22k2,22k+1,22k+24,0)assignsubscript𝐸𝑘final022superscript23superscript242superscript22𝑘2superscript22𝑘1superscript22𝑘240\displaystyle E_{k,\text{final}}:=(0,2,2,2^{3},2^{4}-2,\dots,2^{2k}-2,2^{2k+1}% ,2^{2k+2}-4,0)italic_E start_POSTSUBSCRIPT italic_k , final end_POSTSUBSCRIPT := ( 0 , 2 , 2 , 2 start_POSTSUPERSCRIPT 3 end_POSTSUPERSCRIPT , 2 start_POSTSUPERSCRIPT 4 end_POSTSUPERSCRIPT - 2 , … , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT - 2 , 2 start_POSTSUPERSCRIPT 2 italic_k + 1 end_POSTSUPERSCRIPT , 2 start_POSTSUPERSCRIPT 2 italic_k + 2 end_POSTSUPERSCRIPT - 4 , 0 ) (n,σ)=(0,1).𝑛𝜎01\displaystyle(n,\sigma)=(0,-1).( italic_n , italic_σ ) = ( 0 , - 1 ) .

By Proposition 3.4, Ek,finalsubscript𝐸𝑘finalE_{k,\text{final}}italic_E start_POSTSUBSCRIPT italic_k , final end_POSTSUBSCRIPT is weakly embanked, and one may compute that h(Ek,final)=(22k+21,22k+22)subscript𝐸𝑘finalsuperscript22𝑘21superscript22𝑘22h(E_{k,\text{final}})=(2^{2k+2}-1,2^{2k+2}-2)italic_h ( italic_E start_POSTSUBSCRIPT italic_k , final end_POSTSUBSCRIPT ) = ( 2 start_POSTSUPERSCRIPT 2 italic_k + 2 end_POSTSUPERSCRIPT - 1 , 2 start_POSTSUPERSCRIPT 2 italic_k + 2 end_POSTSUPERSCRIPT - 2 ). Further computing the state formed after the second Halve rule of TEk,finalsubscript𝑇subscript𝐸𝑘finalT_{E_{k,\text{final}}}italic_T start_POSTSUBSCRIPT italic_E start_POSTSUBSCRIPT italic_k , final end_POSTSUBSCRIPT end_POSTSUBSCRIPT shows that Ek,finalsubscript𝐸𝑘finalE_{k,\text{final}}italic_E start_POSTSUBSCRIPT italic_k , final end_POSTSUBSCRIPT is in fact embanked with N(Ek,final)=2k+1𝑁subscript𝐸𝑘final2𝑘1N(E_{k,\text{final}})=2k+1italic_N ( italic_E start_POSTSUBSCRIPT italic_k , final end_POSTSUBSCRIPT ) = 2 italic_k + 1. By (1), applying N()superscript𝑁N^{\prime}(\cdot)italic_N start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ( ⋅ ) to Ek,finalsubscript𝐸𝑘finalE_{k,\text{final}}italic_E start_POSTSUBSCRIPT italic_k , final end_POSTSUBSCRIPT yields

Ek,finalsuperscriptsubscript𝐸𝑘final\displaystyle E_{k,\text{final}}^{\prime}italic_E start_POSTSUBSCRIPT italic_k , final end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT =(0,2,22,23,24,,22k,22k+1,22k+22,0).absent02superscript22superscript23superscript24superscript22𝑘superscript22𝑘1superscript22𝑘220\displaystyle=(0,2,2^{2},2^{3},2^{4},\dots,2^{2k},2^{2k+1},2^{2k+2}-2,0).= ( 0 , 2 , 2 start_POSTSUPERSCRIPT 2 end_POSTSUPERSCRIPT , 2 start_POSTSUPERSCRIPT 3 end_POSTSUPERSCRIPT , 2 start_POSTSUPERSCRIPT 4 end_POSTSUPERSCRIPT , … , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT , 2 start_POSTSUPERSCRIPT 2 italic_k + 1 end_POSTSUPERSCRIPT , 2 start_POSTSUPERSCRIPT 2 italic_k + 2 end_POSTSUPERSCRIPT - 2 , 0 ) .

By Lemma 3.5, we have h(Ek,final)=(22k+21,22k+21)superscriptsubscript𝐸𝑘finalsuperscript22𝑘21superscript22𝑘21h(E_{k,\text{final}}^{\prime})=(2^{2k+2}-1,2^{2k+2}-1)italic_h ( italic_E start_POSTSUBSCRIPT italic_k , final end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) = ( 2 start_POSTSUPERSCRIPT 2 italic_k + 2 end_POSTSUPERSCRIPT - 1 , 2 start_POSTSUPERSCRIPT 2 italic_k + 2 end_POSTSUPERSCRIPT - 1 ); therefore, Proposition 3.6 tells us that N(Ek,final)=Ek,final[ν2(22k+21)+1]=Ek,final[1]𝑁superscriptsubscript𝐸𝑘finalsuperscriptsubscript𝐸𝑘finaldelimited-[]subscript𝜈2superscript22𝑘211superscriptsubscript𝐸𝑘finaldelimited-[]1N(E_{k,\text{final}}^{\prime})=E_{k,\text{final}}^{\prime}[\nu_{2}(2^{2k+2}-1)% +1]=E_{k,\text{final}}^{\prime}[1]italic_N ( italic_E start_POSTSUBSCRIPT italic_k , final end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) = italic_E start_POSTSUBSCRIPT italic_k , final end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT [ italic_ν start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT ( 2 start_POSTSUPERSCRIPT 2 italic_k + 2 end_POSTSUPERSCRIPT - 1 ) + 1 ] = italic_E start_POSTSUBSCRIPT italic_k , final end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT [ 1 ]. Hence,

N(Ek,final)𝑁superscriptsubscript𝐸𝑘final\displaystyle N(E_{k,\text{final}}^{\prime})italic_N ( italic_E start_POSTSUBSCRIPT italic_k , final end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ′ end_POSTSUPERSCRIPT ) =(0,2,22,23,24,,22k,22k+1,22k+2,0),absent02superscript22superscript23superscript24superscript22𝑘superscript22𝑘1superscript22𝑘20\displaystyle=(0,2,2^{2},2^{3},2^{4},\dots,2^{2k},2^{2k+1},2^{2k+2},0),= ( 0 , 2 , 2 start_POSTSUPERSCRIPT 2 end_POSTSUPERSCRIPT , 2 start_POSTSUPERSCRIPT 3 end_POSTSUPERSCRIPT , 2 start_POSTSUPERSCRIPT 4 end_POSTSUPERSCRIPT , … , 2 start_POSTSUPERSCRIPT 2 italic_k end_POSTSUPERSCRIPT , 2 start_POSTSUPERSCRIPT 2 italic_k + 1 end_POSTSUPERSCRIPT , 2 start_POSTSUPERSCRIPT 2 italic_k + 2 end_POSTSUPERSCRIPT , 0 ) ,

which is just Sk+1subscript𝑆𝑘1S_{k+1}italic_S start_POSTSUBSCRIPT italic_k + 1 end_POSTSUBSCRIPT.

\printbibliography