This paper was converted on www.awesomepapers.org from LaTeX by an anonymous user.
Want to know more? Visit the Converter page.

Density Devolution for Ordering Synthetic Channels

Hsin-Po Wang University of California, Berkeley, CA, USA
simple@berkeley.edu
   Chi-Wei Chin Apricob Biomedicals Co Ltd, Taiwan
qin@quantumsafe.dev
Abstract

Constructing a polar code is all about selecting a subset of rows from a Kronecker power of [𝟏𝟏]𝟏𝟎[^{1}_{1}{}^{0}_{1}]. It is known that, under successive cancellation decoder, some rows are Pareto-better than the other. For instance, whenever a user sees a substring 𝟎𝟏01 in the binary expansion of a row index and replaces it with 𝟏𝟎10, the user obtains a row index that is always more welcomed. We call this a “rule” and denote it by 𝟏𝟎𝟎𝟏10\succcurlyeq 01. In present work, we first enumerate some rules over binary erasure channels such as 𝟏𝟎𝟎𝟏𝟎𝟏𝟏𝟎1001\succcurlyeq 0110 and 𝟏𝟎𝟎𝟎𝟏𝟎𝟏𝟎𝟏𝟎10001\succcurlyeq 01010 and 𝟏𝟎𝟏𝟎𝟏𝟎𝟏𝟏𝟏𝟎10101\succcurlyeq 01110. We then summarize them using a “rule of rules”: if 𝟏𝟎𝒂𝟎𝟏𝒃10a\succcurlyeq 01b is a rule, where 𝒂a and 𝒃b are arbitrary binary strings, then 𝟏𝟎𝟎𝒂𝟎𝟏𝟎𝒃100a\succcurlyeq 010b and 𝟏𝟎𝟏𝒂𝟎𝟏𝟏𝒃101a\succcurlyeq 011b are rules. This work’s main contribution is using field theory, Galois theory, and numerical analysis to develop an algorithm that decides if a rule of rules is mathematically sound. We apply the algorithm to enumerate some rules of rules. Each rule of rule is capable of generating an infinite family of rules. For instance, 𝟏𝟎𝒄𝟎𝟏𝟎𝟏𝒄𝟏𝟎10c01\succcurlyeq 01c10 for arbitrary binary string 𝒄c can be generated. We found an application of 𝟏𝟎𝒄𝟎𝟏𝟎𝟏𝒄𝟏𝟎10c01\succcurlyeq 01c10 that is related to integer partition and the dominance order therein.

I Introduction

Ever since polar code was invented [1], it has constantly reminded researchers about its similarity to Reed–Muller codes [2, 3, 4, 5, 6] for that they both are generated by some subsets of rows of a Kronecker power of [11]10[^{1}_{1}{}^{0}_{1}].

There is, nevertheless, a huge discrepancy. For Reed–Muller code, a user always picks rows with the highest Hamming weights up to the desired rate. Whether this will yield a good code is a very challenging problem [7, 8]. For polar code, the story goes the opposite way. While Arıkan proved the existence of subsets of rows that are capacity-achieving under successive cancellation decoder, it was not clear if there is any simple rule that tells us what to choose other than actually simulating the channels and carrying out the statistics. Should we be not careful and choose the wrong row, the performance will go low.

Mori and Tanaka [9], to address the row-selection issue, suggested using density evolution and the degradation relation W1WW0W^{1}\mathrel{-\mkern-2.0mu\triangleright}W\mathrel{-\mkern-2.0mu\triangleright}W^{0} as an alternative to simulation. Degradation does not directly tell us which rows are to select, but it tells us that some rows are always better than the other. This means that not all rows need to undergo simulation or density evolution, presumably simplifying the row-selection process.

Later, Schürch [10] and Bardet, Drägoi, Otmani, and Tillich [11] added one more degradation relation W10W01W^{10}\mathrel{-\mkern-2.0mu\triangleright}W^{01}. Mondelli and Hassani and Urbanke [12] then showed that the number of rows that need to be seriously evaluated (either by simulation or evolution) is sub-linear in the block length. For the majority of rows, the degradation relation alone is enough to make the decision.

In this work, we follow the track of Wu and Siegel [13], Camps, López, Matthews, and Sarmiento [14], Drägoi and Cristescu [15], Geiger [16], Kahraman [17], and Kim, Oh, Kim, and Ha [18] to study comparison between rows. Throughout the work, we assume that the underlying channel is a binary erasure channel (BEC) and the successive cancellation decoder is in use.

For the first time, we consider density devolution, which stands for the opposite operation of density evolution. In the absence of devolution, comparing two BECs is essentially about proving a certain polynomial nonnegative, which can be done procedurally. Devolution introduces square root into the world of polynomials and the problem become proving certain algebraic function nonnegative. Wielding tools from field theory, Galois theory, and numerical analysis, we can decide, rigorously, if an algebraic function is always nonnegative. Each nonnegative algebraic function imply the nonnegativity of infinitely many polynomials, which means that we can now prove polynomial inequalities en masse.

The paper is organized as follows. Section II reviews the definition of polar code and a related preorder. Section III shows how to determine a polynomial inequality. Section IV extends the alphabet to {0,1,2,3}\{0,1,2,3\}. Section V lays some field theory bricks. Section VI shows how to determine a inequality involving {0,1,2,3}\{0,1,2,3\}. Section VII proves infinitely many inequalities.

II Polar Code and Partial Order over BEC

A simplified recipe of polar code reads: Let K[11]10K\coloneqq[^{1}_{1}{}^{0}_{1}]. Choose a positive integer nn and construct KnK^{\otimes n}, the nnth Kronecker power of KK. Then, choose a subset of rows of KnK^{\otimes n} as the generator matrix GG. This GG generates a polar code.

In selecting rows, a useful fact is that each row corresponds to a synthetic channel that is defined through density evolution. Let’s take the BEC with capacity x[0,1]x\in[0,1] as an example. First, define I0(x)x2I_{0}(x)\coloneqq x^{2} and I1(x)1(1x)2I_{1}(x)\coloneqq 1-(1-x)^{2}. Next, define Ib1b2bn(x)Ib2bn(Ib1(x))I_{b_{1}b_{2}\dotsm b_{n}}(x)\coloneqq I_{b_{2}\dotsm b_{n}}(I_{b_{1}}(x)) for any binary string b=b1b2bn{0,1}nb=b_{1}b_{2}\dotsm b_{n}\in\{0,1\}^{n}. Now, the (1+i=1nbi2ni)(1+\sum_{i=1}^{n}b_{i}2^{n-i})th row of KnK^{\otimes n} corresponds to the BEC with capacity Ib(x)I_{b}(x).

The design principle of polar code recommends that the best rows are those with the highest capacities. A natural question is: Can there be two rows such that one always has a higher capacity than the other?

Definition 1

For any binary strings aa and bb, we say aba\succcurlyeq b if Ia(x)Ib(x)I_{a}(x)\geq I_{b}(x) for all x[0,1]x\in[0,1].

The following lemmas are known regarding II and \succcurlyeq.

Lemma 2

I0I_{0} and I1I_{1} are strictly monotonically increasing and map [0,1][0,1] bijectively onto [0,1][0,1]. In fact, all IbI_{b} are.

Proof:

Being strictly monotonically increasing and bijective is closed under function composition. ∎

Lemma 3

\succcurlyeq forms a preorder on binary strings.

Proof:

Reflexivity: Ia(x)Ia(x)I_{a}(x)\geq I_{a}(x), hence aaa\succcurlyeq a. Transitivity: Ia(x)Ib(x)Ic(x)I_{a}(x)\geq I_{b}(x)\geq I_{c}(x) implies Ia(x)Ic(x)I_{a}(x)\geq I_{c}(x). ∎

Lemma 4

acbdac\succcurlyeq bd if aba\succcurlyeq b and cdc\succcurlyeq d for any binary strings aa, bb, cc, and dd. Juxtaposition stands for string concatenation.

Proof:

IcI_{c} is monotonically increasing so acbcac\succcurlyeq bc. The image Ib([0,1])I_{b}([0,1]) is contained in [0,1][0,1] so bcbdbc\succcurlyeq bd. ∎

Lemma 5

If aba\succcurlyeq b, then b~a~\tilde{b}\succcurlyeq\tilde{a}. Tilde stands for bitwise complement.

Proof:

The plot of Ia~I_{\tilde{a}} is the plot of IaI_{a} rotated by 180180 degrees w.r.t. (1/2,1/2)(1/2,1/2) as the center. Hence the assumption that IaI_{a}’s plot lies above IbI_{b}’s plot implies that Ia~I_{\tilde{a}}’s plot lies below Ib~I_{\tilde{b}}’s plot. ∎

These lemmas together with 101\succcurlyeq 0 imply comparisons such as 111110111010001000001111\succcurlyeq 1011\succcurlyeq 1010\succcurlyeq 0010\succcurlyeq 0000. Readers might argue that this should not be counted as multiple contributions. Rather, it is but one simple rule, 101\succcurlyeq 0, applied multiple times. Likewise, 110010101001010100111100\succcurlyeq 1010\succcurlyeq 1001\succcurlyeq 0101\succcurlyeq 0011 can be summarized by a simple rule, 100110\succcurlyeq 01.

The main goal of this paper is to demonstrate how to generate new rules that are not consequences of other rules. We hope readers understand that what qualifies as an independent rule is context-dependent, sometimes even subjective. For instance, 001110000011\succcurlyeq 1000 probably looks like an independent rule, but it is a consequence111 Take the bitwise complement: 01110011\succcurlyeq 10 implies 0110001\succcurlyeq 100. Hence 001101010000011\succcurlyeq 010\succcurlyeq 1000. of 01110011\succcurlyeq 10. For longer comparisons such as 010111010001011\succcurlyeq 10100, it is never clear if they can be verified without brute force. Therefore, we will declare a new rule whenever it seems to be so.

III Polynomial Inequality Problem

III-A A procedure

Suppose P𝐙[x]P\in{\mathbf{Z}}[x] is an polynomial with integer coefficients. There exist algorithms that find the exact number of roots of PP in a given interval (cf. Sturm’s theorem) or at least a mathematical sound upper bound on the number of roots (cf. Vincent’s theorem) [19]. A root-counting algorithm is usually paired with a bisecting strategy and the Newton–Raphson method to pinpoint the roots. But for now, we only need the counting part.

Assume P𝐙[x]P\in{\mathbf{Z}}[x]. Here is how to decide whether

P(x)0for all x[0,1].P(x)\geq 0\qquad\text{for all }x\in[0,1]. (1)

Step one: Divide PP by xm(1x)nx^{m}(1-x)^{n}, where mm and nn are the multiplicities of 0 and 11, respectively, as roots of PP. Since xx and 1x1-x are nonnegative over [0,1][0,1], the sign of PP stays unchanged after division.

Step two: Remove the perfect square part of PP by dividing PP by (g/gcd(g,g))2(g/\gcd(g,g^{\prime}))^{2}, where ggcd(P,P)g\coloneqq\gcd(P,P^{\prime}) (cf. Yun’s algorithm [20]). To see why this division works, suppose d𝐙[x]d\in{\mathbf{Z}}[x] is any irreducible factor of PP. Write dmPd^{m}\mathrel{\|}P to mean dmPd^{m}\mid P but dm+1Pd^{m+1}\nmid P, i.e, mm is the multiplicity of dd in the factorization of PP. We then have

dmax(0,m1)\displaystyle d^{\max(0,m-1)} P,\displaystyle\mathrel{\|}P^{\prime},
dmax(0,m1)\displaystyle d^{\max(0,m-1)} g,\displaystyle\mathrel{\|}g,
dmax(0,m2)\displaystyle d^{\max(0,m-2)} gcd(g,g),\displaystyle\mathrel{\|}\gcd(g,g^{\prime}),
dmax(0,m1)max(0,m2)\displaystyle d^{\max(0,m-1)-\max(0,m-2)} g/gcd(g,g).\displaystyle\mathrel{\|}g/\gcd(g,g^{\prime}).

Note that max(0,m1)max(0,m2)\max(0,m-1)-\max(0,m-2) is just the indicator of m2m\geq 2. This means that we are removing two copies of dd from PP if there are two or more copies. Repeat this step several times until the multiplicities of all irreducible factors become 0 or 11. Since we always divide PP by a perfect square, the sign of PP stays unchanged.

Step three: Granted that PP is now square-free, we evaluate P(1/2)P(1/2). If P(1/2)<0P(1/2)<0, this violates (1) right away. If P(1/2)=0P(1/2)=0, since x=1/2x=1/2 is a single root, either P(1/2+ε)P(1/2+\varepsilon) or P(1/2ε)P(1/2-\varepsilon) will be negative for some small ε>0\varepsilon>0, violating (1). In either case, our procedure terminates early and returns FALSE.

Step four: Count the number of roots of PP in the interval [0,1][0,1]. If there is any root, say x=ξx=\xi, then by the same reasoning as above, P(ξ+ε)P(\xi+\varepsilon) or P(ξε)P(\xi-\varepsilon) will be negative, violating (1). If there are no roots, then all P(x)P(x) share the same sign as P(1/2)P(1/2), confirming that (1) is TRUE. This concludes our procedure to decide (1).

Theorem 6

The procedure described in this subsection decides inequalities of the form (1).

III-B Application of the procedure

Checking Ia(x)Ib(x)I_{a}(x)\geq I_{b}(x) is equivalent to checking Ia(x)Ib(x)0I_{a}(x)-I_{b}(x)\geq 0. This constitutes a terminating procedure that decides if aba\succcurlyeq b for any binary strings aa and bb. One runs this procedure and finds the following comparisons.

  • 1ϵ01\succcurlyeq\epsilon\succcurlyeq 0, where ϵ\epsilon is the empty string.

  • 1110010011\succcurlyeq 10\succcurlyeq 01\succcurlyeq 00.

  • 0111001100011\succcurlyeq 10\succcurlyeq 01\succcurlyeq 100.

  • 111110101011100010001111\succcurlyeq 110\succcurlyeq 101\succcurlyeq 011\succcurlyeq 100\succcurlyeq 010\succcurlyeq 001.

  • 11111110110110110111110010101001011001010011100001000010000100001111\succcurlyeq 1110\succcurlyeq 1101\succcurlyeq 1011\succcurlyeq 0111\succcurlyeq 1100\succcurlyeq 1010\succcurlyeq 1001\succcurlyeq 0110\succcurlyeq 0101\succcurlyeq 0011\succcurlyeq 1000\succcurlyeq 0100\succcurlyeq 0010\succcurlyeq 0001\succcurlyeq 0000.

  • 1111111110111011101110111011111101011111\succcurlyeq 11110\succcurlyeq 11101\succcurlyeq 11011\succcurlyeq 10111\succcurlyeq 01111\succcurlyeq 11010.

  • 1011111100110101100110110101011001101101110001010010111\succcurlyeq 11100\succcurlyeq 11010\succcurlyeq 11001\succcurlyeq 10110\succcurlyeq 10101\succcurlyeq 10011\succcurlyeq 01101\succcurlyeq 11000\succcurlyeq 10100.

  • 101010111001101010111010010010100010101010101\succcurlyeq 01110\succcurlyeq 01101\succcurlyeq 01011\succcurlyeq 10100\succcurlyeq 10010\succcurlyeq 10001\succcurlyeq 01010.

  • 0101100111100100110001010010010011000101000110100001011\succcurlyeq 00111\succcurlyeq 10010\succcurlyeq 01100\succcurlyeq 01010\succcurlyeq 01001\succcurlyeq 00110\succcurlyeq 00101\succcurlyeq 00011\succcurlyeq 01000.

  • 0010110000010000010000010000010000000101\succcurlyeq 10000\succcurlyeq 01000\succcurlyeq 00100\succcurlyeq 00010\succcurlyeq 00001\succcurlyeq 00000.

Among these comparisons, 1ϵ1\succcurlyeq\epsilon ,  0111001011\succcurlyeq 10\succcurlyeq 01 ,  100101101001\succcurlyeq 0110 ,  100010101010001\succcurlyeq 01010 ,  001011000000101\succcurlyeq 10000 ,  001111001000111\succcurlyeq 10010 ,  and 010111010001011\succcurlyeq 10100 qualify as new rules. Theoretically, one Their run the procedure on arbitrarily long strings to generate all possible comparisons. As of now, this is the only reliable way to enumerate comparisons that are not consequences of each other.

Executing that, one might find interesting patterns among those comparisons. For instance, 10b0110b01 seems to be 01b10\succcurlyeq 01b10 for any binary string bb. After some reductions, one sees that 100m01010m10100^{m}01\succcurlyeq 010^{m}10 seems to be a set of rules that are not consequences of each other. Can we prove this for all mm?

IV Inverse of Density Evolution

To motivate why we need the inverses of WW0W\mapsto W^{0} and WW1W\mapsto W^{1}, consider the following. We know from running the deterministic procedure that 100m01010m10100^{m}01\succcurlyeq 010^{m}10 holds for m=0,1,,10m=0,1,\dotsc,10. But we want it to hold for all positive integers mm. Wouldn’t it be convenient if there is a comparison cdc\succcurlyeq d that, when combined with 100m01010m10100^{m}01\succcurlyeq 010^{m}10, gives

100m+101\displaystyle 100^{m+1}01 =c100m01\displaystyle=c100^{m}01 (2)
d010m10=010m+110?\displaystyle\succcurlyeq d010^{m}10=010^{m+1}10? (3)

What should cc and dd be to make this happen?

By reverse-engineering (2) and (3), we see that cc “equals” 10001111000^{-1}1^{-1} and dd “equals” 01011010101^{-1}0^{-1}. The inverses 010^{-1} and 111^{-1} can be made formal by appointing I2(x)xI_{2}(x)\coloneqq\sqrt{x} the inverse function of I0I_{0} and I3(x)11xI_{3}(x)\coloneqq 1-\sqrt{1-x} the inverse function of I1I_{1}. We use 22 and 33 in place of 010^{-1} and 111^{-1} to ease the notation. These are density devolution; if WW is a BEC with capacity xx, then U0=V1=WU^{0}=V^{1}=W, where UU and VV are BECs with capacities I2(x)I_{2}(x) and I3(x)I_{3}(x), respectively.

Define Iq1q2qn(x)Iq2qn(Iq1(x))I_{q_{1}q_{2}\dotsm q_{n}}(x)\coloneqq I_{q_{2}\dotsm q_{n}}(I_{q_{1}}(x)) for any quaternary string q1q2qn{0,1,2,3}q_{1}q_{2}\dotsm q_{n}\in\{0,1,2,3\}. Note that 02=20=13=31=ϵ02=20=13=31=\epsilon.

Definition 7

For any quaternary strings pp and qq, we say pqp\succcurlyeq q if Ip(x)Iq(x)I_{p}(x)\geq I_{q}(x) for all x[0,1]x\in[0,1].

We find generalizations of the old lemmas to the new alphabet as well as new lemmas that only make sense with the new alphabet. Some proofs are omitted.

Lemma 8

I0I_{0}, I1I_{1}, I2I_{2}, and I3I_{3} are strictly monotonically increasing and map [0,1][0,1] bijectively onto [0,1][0,1]. In fact, all IqI_{q} are.

Lemma 9

\succcurlyeq still forms a preorder on quaternary strings. pqp\succcurlyeq q and rsr\succcurlyeq s still imply prqspr\succcurlyeq qs and q~p~\tilde{q}\succcurlyeq\tilde{p}. Here, the complement (denoted by tilde) of 22 and 33 are each other.

Lemma 10

pqp\succcurlyeq q iff pq1ϵpq^{-1}\succcurlyeq\epsilon iff q1pϵq^{-1}p\succcurlyeq\epsilon iff q1p1q^{-1}\succcurlyeq p^{-1} iff ϵp1q\epsilon\succcurlyeq p^{-1}q iff ϵqp1\epsilon\succcurlyeq qp^{-1}. Here, ϵ\epsilon represents the empty string.

Proof:

Let rsq1r\coloneqq s\coloneqq q^{-1} to prove the first “only if”. The rest are similar. ∎

Lemma 11

q2ϵq^{2}\succcurlyeq\epsilon iff qϵq\succcurlyeq\epsilon.

Proof:

q2ϵq^{2}\succcurlyeq\epsilon implies qq1q\succcurlyeq q^{-1}. Note that the plot of IqI_{q} and the plot of Iq1I_{q^{-1}} are symmetric with respect to the diagonal that passes (0,0)(0,0) and (1,1)(1,1). As qq1q\succcurlyeq q^{-1} implies that the former plot lies entirely above the later plot, the former plot lies entirely above the diagonal. This is saying qϵq\succcurlyeq\epsilon. ∎

So far, we have explored some basic properties concerning the quaternary alphabet. But let’s not forget that the goal is to make (2) and (3) (and presumably more of that form) mathematically sound. How exactly can we prove c1002301032dc\coloneqq 10023\succcurlyeq 01032\eqqcolon d?

V Field Extensions of Univariate Polynomials

We aim to generalize the procedure in Section III to one that can decides whether pqp\succcurlyeq q for all quaternary strings pp and qq. This sections prepares some building blocks for such a procedure.

Let 𝐐{\mathbf{Q}} be the set of rational numbers. Let 𝐐[x]{\mathbf{Q}}[x] be the set of univariate polynomials in variable xx whose coefficients are in 𝐐{\mathbf{Q}}. Let 𝐊Frac(𝐐[x]){\mathbf{K}}\coloneqq\operatorname{Frac}({\mathbf{Q}}[x]) be the fraction field of 𝐐[x]{\mathbf{Q}}[x]. Let 𝐂{\mathbf{C}} be the set of complex numbers. Let 𝐂𝐂{\mathbf{C}}^{\mathbf{C}} be the set of functions from 𝐂{\mathbf{C}} to 𝐂{}{\mathbf{C}}\cup\{\infty\} that take infinity finitely many times.

A complex number ξ𝐂\xi\in{\mathbf{C}} is called an algebraic number if there exists a polynomial f𝐐[x]f\in{\mathbf{Q}}[x] with rational number coefficients such that f(ξ)=0f(\xi)=0. Since our quaternary alphabet involves extracting the square root of a polynomial, we want to extend the concept of algebraic numbers to polynomials.

Definition 12

We call any function φ𝐂𝐂\varphi\in{\mathbf{C}}^{\mathbf{C}} an algebraic function if there exists a bivariate polynomial G𝐐[x,y]G\in{\mathbf{Q}}[x,y] with rational number coefficients such that G(ξ,φ(ξ))=0G(\xi,\varphi(\xi))=0 for all ξ𝐂\xi\in{\mathbf{C}} except for the case φ(ξ)=\varphi(\xi)=\infty. We denote the set of algebraic functions by 𝐀𝐅{\mathbf{AF}}.

Clearly, 𝐐𝐐[x]𝐊𝐀𝐅𝐂𝐂{\mathbf{Q}}\subset{\mathbf{Q}}[x]\subset{\mathbf{K}}\subset{\mathbf{AF}}\subset{\mathbf{C}}^{\mathbf{C}}.

Lemma 13

Algebraic functions are closed under addition and multiplication. That is, φ+ψ,φψ𝐀𝐅\varphi+\psi,\varphi\psi\in{\mathbf{AF}} given φ,ψ𝐀𝐅\varphi,\psi\in{\mathbf{AF}}.

Proof:

We use a routine argument from the field theory. Readers are encouraged to skip should they find this boring.

Let 𝐊[φ,ψ]{\mathbf{K}}[\varphi,\psi], as a subset of 𝐂𝐂{\mathbf{C}}^{\mathbf{C}}, be the collection of functions of the form

i,jpi,jqi,jφiψj,\sum_{i,j}\frac{p_{i,j}}{q_{i,j}}\varphi^{i}\psi^{j},

where the sum is finite and pi,j,qi,j𝐐[x]p_{i,j},q_{i,j}\in{\mathbf{Q}}[x]. 𝐊[φ,ψ]{\mathbf{K}}[\varphi,\psi] forms a vector space over 𝐊{\mathbf{K}} because it is closed under addition and scalar-multiplication by an element of 𝐊{\mathbf{K}}.

Suppose the degree of φ\varphi over 𝐊{\mathbf{K}} is dd and the degree of ψ\psi over 𝐊{\mathbf{K}} is ee. That is to say, there are relations

i=0dgiφi=0,i=0ehjψj=0,\sum_{i=0}^{d}g_{i}\varphi^{i}=0,\qquad\sum_{i=0}^{e}h_{j}\psi^{j}=0,\qquad

where gi,hj𝐐[x]g_{i},h_{j}\in{\mathbf{Q}}[x]. Then we can express φd\varphi^{d} as a combination of φi\varphi^{i} for i<di<d. Likewise, we can express ψe\psi^{e} as a combination of lower power terms. Hence 𝐊[φ,ψ]{\mathbf{K}}[\varphi,\psi] is a finite dimensional vector space over 𝐊{\mathbf{K}}.

This implies that 𝐊[φψ]{\mathbf{K}}[\varphi\psi], as a vector subspace of 𝐊[φ,ψ]{\mathbf{K}}[\varphi,\psi], is of finite dimension over 𝐊{\mathbf{K}}. Hence 1,φψ,(φψ)2,,(φψ)d+e1,\varphi\psi,(\varphi\psi)^{2},\dotsc,(\varphi\psi)^{d+e} are not linearly independent over 𝐊{\mathbf{K}}. There must exist a linear equation relating the powers of φψ\varphi\psi, which witnesses the fact that φψ\varphi\psi is an algebraic function.

For φ+ψ\varphi+\psi, the same argument applies. ∎

Lemma 14

Algebraic functions are closed under extracting the mmth roots. That is, φ𝐀𝐅\varphi\in{\mathbf{AF}} if the function φ𝐂𝐂\varphi\in{\mathbf{C}}^{\mathbf{C}} is such that φm𝐀𝐅\varphi^{m}\in{\mathbf{AF}} for some positive integer mm.

Proof:

If G(x,φm(x))=0G(x,\varphi^{m}(x))=0, then H(x,y)G(x,ym)H(x,y)\coloneqq G(x,y^{m}) is a bivariate polynomial such that H(x,φ(x))=0H(x,\varphi(x))=0. ∎

Definition 15

A root of an algebraic function φ𝐀𝐅\varphi\in{\mathbf{AF}} is a complex number ξ𝐂\xi\in{\mathbf{C}} such that φ(ξ)=0\varphi(\xi)=0.

Lemma 16

A root of an algebraic function is an algebraic number.

Proof:

If ξ𝐂\xi\in{\mathbf{C}} is such that φ(ξ)=0\varphi(\xi)=0, then f(x)G(x,0)f(x)\coloneqq G(x,0) is a polynomial in xx such that f(ξ)=G(ξ,0)=G(ξ,φ(ξ))=0f(\xi)=G(\xi,0)=G(\xi,\varphi(\xi))=0. Note that f(x)f(x) is a polynomial with rational-number coefficients so ξ\xi is an algebraic number. ∎

Theorem 17

Suppose ξ[0,1]\xi\in[0,1] and pp and qq are quaternary strings. If Ip(ξ)=Iq(ξ)I_{p}(\xi)=I_{q}(\xi), then ξ\xi is an algebraic number.

Proof:

The building blocks of IqI_{q} are squaring, subtracting from 11, and extracting the square root. We have seen that all three operations map an algebraic function to an algebraic function. Hence Ip(x)Iq(x)I_{p}(x)-I_{q}(x) is an algebraic function. Hence ξ\xi is an algebraic number. ∎

VI Algebraic Function Inequality Problem

Thanks to the previous section, we can verify any inequality of the form

Ip(x)Iq(x)for all x[0,1],I_{p}(x)\geq I_{q}(x)\qquad\text{for all }x\in[0,1], (4)

where pp and qq are quaternary strings. Here is how.

VI-A The “in principle, we can” part

Let φ(x)Ip(x)Iq(x)𝐂𝐂\varphi(x)\coloneqq I_{p}(x)-I_{q}(x)\in{\mathbf{C}}^{\mathbf{C}}. To safely extend the domain of IpIqI_{p}-I_{q} to 𝐂{\mathbf{C}}, we always select the square root in [0,1][0,1] if there is any, and select an arbitrary one otherwise.

By the proof of that any root of φ\varphi is an algebraic number, there is an algorithm that outputs a polynomial f𝐐[x]f\in{\mathbf{Q}}[x] that evaluates any root of φ\varphi to zero. That is to say, to check if [0,1][0,1] contains any root of φ\varphi, it suffices to check if any root of ff in [0,1][0,1] happens to be a root of φ\varphi.

Now, let the roots of ff that are also in [0,1][0,1] be, in ascending order, 0=ξ0<ξ1<ξ2<<ξm=10=\xi_{0}<\xi_{1}<\xi_{2}<\dotsb<\xi_{m}=1. It suffices to check if φ((ξj+ξj+1)/2)\varphi((\xi_{j}+\xi_{j+1})/2) are all positive. It might seem that this step will cost a lot because we need precise roots of ff. Luckily, a root-isolating algorithm will give us disjoint intervals that each contains an isolated root. Thus, instead of (ξj+ξj+1)/2(\xi_{j}+\xi_{j+1})/2, checking the endpoints of the intervals is equally valid.

VI-B The “thanks to Galois theory, we’d better” part

But how exactly are we going to find the polynomial ff given quaternary strings pp and qq? Instead of relying on the lemma that φψ\varphi\psi and φ+ψ\varphi+\psi are finite-dimensional over 𝐊{\mathbf{K}} but the linear equations are implicit. The following is what we actually do to work out ff more efficiently.

First and foremost, instead of Ip(x)Iq(x)I_{p}(x)-I_{q}(x), we will be working on φ(x)Ipq1(x)x\varphi(x)\coloneqq I_{pq^{-1}}(x)-x. If φ\varphi contains no square root, then it is a polynomial and we have detailed how to handle polynomials in Section III. Otherwise, φ\varphi is of the form

φ(x)=H(x,ψ(x)),\varphi(x)=H\bigl{(}x,\sqrt{\psi(x)}\bigr{)},

where H𝐐[x,y]H\in{\mathbf{Q}}[x,y] and ψ𝐀𝐅\psi\in{\mathbf{AF}}. We see that, if φ(ξ)=0\varphi(\xi)=0, then

H(x,ψ(ξ))H(x,ψ(ξ))=0H\bigl{(}x,\sqrt{\psi(\xi)}\bigr{)}\cdot H\bigl{(}x,-\sqrt{\psi(\xi)}\bigr{)}=0

Note that H(x,y)H(x,y)𝐐[x,y]H(x,\sqrt{y})\cdot H(x,-\sqrt{y})\in{\mathbf{Q}}[x,y]. So we can eliminate one layer of square root by replacing φ\varphi with

H(x,ψ(x))H(x,ψ(x)).H\bigl{(}x,\sqrt{\psi(x)}\bigr{)}\cdot H\bigl{(}x,-\sqrt{\psi(x)}\bigr{)}. (5)

Repeating the same procedure, we can eliminate all square roots introduced by symbols 22 and 33 in pq1pq^{-1}. And the resulting product of HH’s will be our ff.

As an example, suppose we begin with

φ(x)1x23x2.\varphi(x)\coloneqq 1-x-\sqrt{2-\sqrt{3-x^{2}}}.

This means H(x,y)=1xyH(x,y)=1-x-y and ψ(x)=23x2\psi(x)=2-\sqrt{3-x^{2}}. So (5) becomes

(1x)2(23x2).(1-x)^{2}-(2-\sqrt{3-x^{2}}).

Proceed to the next step, H(x,y)H(x,y) becomes (1x)22+y(1-x)^{2}-2+y and ψ(x)\psi(x) becomes 3x23-x^{2}. So (5) becomes

((1x)22)2(3x2).((1-x)^{2}-2)^{2}-(3-x^{2}). (6)

Now this is the polynomial ff we want.

Remark: the idea presented in this subsection can be summarized as “multiplying all Galois-conjugates together.” To elaborate, since φ\varphi is algebraic over 𝐊{\mathbf{K}}, there exists Galois actions σ1,σ2,,σd\sigma_{1},\sigma_{2},\dotsc,\sigma_{d} that sends φ\varphi to other functions that satisfies the very same equation satisfied by φ\varphi. The product of all conjugates must be in the base field: fσ1(φ)σ2(φ)σd(φ)𝐊f\coloneqq\sigma_{1}(\varphi)\sigma_{2}(\varphi)\dotsm\sigma_{d}(\varphi)\in{\mathbf{K}}. But one of the factors is φ\varphi; so φ(ξ)=0\varphi(\xi)=0 implies f(ξ)=0f(\xi)=0. In the example above, the conjugates are

1x23x2, 1x+23x2,\displaystyle 1-x-\sqrt{2-\sqrt{3-x^{2}}}\,,\,1-x+\sqrt{2-\sqrt{3-x^{2}}}\,,
1x2+3x2, 1x+2+3x2.\displaystyle 1-x-\sqrt{2+\sqrt{3-x^{2}}}\,,\,1-x+\sqrt{2+\sqrt{3-x^{2}}}.

Their product is the same ff we conclude in (6).

Theorem 18

The procedure described in this section decides inequalities of the form (4).

VII The TBM Partial Order

VII-A Prefix TBM

Inspired by the proposed proof of 100m01010m10100^{m}01\succcurlyeq 010^{m}10, i.e., (2) and (3), we make the following definition.

Definition 19

Fix quaternary strings α\alpha and β\beta. We write α

β
\alpha\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}\beta
if, for any quaternary strings yy and zz,

αyβzimpliesα0yβ0zandα1yβ1z.\alpha y\succcurlyeq\beta z\qquad\text{implies}\qquad\alpha 0y\succcurlyeq\beta 0z\quad\text{and}\quad\alpha 1y\succcurlyeq\beta 1z.

We call

\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}
a TBM relation. TBM stands for tunnel boring machine, a machine that extends existing tunnels, inspired by the potential usage in (2) and (3). As a starter, we can prove 1

0
1\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}0
fairly easily: if 1y0z1y\succcurlyeq 0z, then 10y01y00z10y\succcurlyeq 01y\succcurlyeq 00z and 11y10z01z11y\succcurlyeq 10z\succcurlyeq 01z.

Another example: Suppose 100230103210023\succcurlyeq 01032 holds, then 10y01z10y\succcurlyeq 01z implies 100y=(10023)(10y)(01032)(01z)=010z100y=(10023)(10y)\succcurlyeq(01032)(01z)=010z. Take the bitwise complement: 100230103210023\succcurlyeq 01032 implies 101230113210123\succcurlyeq 01132; then 10y01z10y\succcurlyeq 01z implies 101y=(10123)(10y)(01132)(01z)=011z101y=(10123)(10y)\succcurlyeq(01132)(01z)=011z. Therefore, 100230103210023\succcurlyeq 01032 implies 10

01
10\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}01
.

As it gets more complicated, we see the necessity to develop a machine that can automate this away.

Lemma 20

α

β
\alpha\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}\beta
if and only if both α0α1β0β1\alpha 0\alpha^{-1}\succcurlyeq\beta 0\beta^{-1} and α1α1β1β1\alpha 1\alpha^{-1}\succcurlyeq\beta 1\beta^{-1} hold.

Proof:

Let’s prove the “if” part. Suppose α0α1β0β1\alpha 0\alpha^{-1}\succcurlyeq\beta 0\beta^{-1} holds and suppose αyβz\alpha y\succcurlyeq\beta z, then (α0α1)(αy)(β0β1)(βz)(\alpha 0\alpha^{-1})(\alpha y)\succcurlyeq(\beta 0\beta^{-1})(\beta z), implying α0yβ0z\alpha 0y\succcurlyeq\beta 0z. For α1α1β1β1\alpha 1\alpha^{-1}\succcurlyeq\beta 1\beta^{-1}, the same argument applies.

Let’s prove the “only if” part. Let (y,z)(α1,β1)(y,z)\coloneqq(\alpha^{-1},\beta^{-1}), then αyβz\alpha y\succcurlyeq\beta z definitely holds as both sides are empty. But then that implies that α0yβ0z\alpha 0y\succcurlyeq\beta 0z, which is α0α1β0β1\alpha 0\alpha^{-1}\succcurlyeq\beta 0\beta^{-1}. Likewise, α1yβ1z\alpha 1y\succcurlyeq\beta 1z is just α1α1β1β1\alpha 1\alpha^{-1}\succcurlyeq\beta 1\beta^{-1}. ∎

Lemma 21

\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}
is a preorder.

Proof:

Reflexivity: Observe that α0α1α0α1\alpha 0\alpha^{-1}\succcurlyeq\alpha 0\alpha^{-1} and α1α1α1α1\alpha 1\alpha^{-1}\succcurlyeq\alpha 1\alpha^{-1}. Transitivity: Use α0α1β0β1γ0γ1\alpha 0\alpha^{-1}\succcurlyeq\beta 0\beta^{-1}\succcurlyeq\gamma 0\gamma^{-1} and α1α1β1β1γ1γ1\alpha 1\alpha^{-1}\succcurlyeq\beta 1\beta^{-1}\succcurlyeq\gamma 1\gamma^{-1}. ∎

Lemma 22

α

β
\alpha\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}\beta
iff β~

α~
\tilde{\beta}\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}\tilde{\alpha}
iff β1α

ϵ
\beta^{-1}\alpha\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}\epsilon
iff ϵ

α1β
\epsilon\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}\alpha^{-1}\beta
.

Theorem 23

α

β
\alpha\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}\beta
implies αβ\alpha\succcurlyeq\beta. Note: the converse is not true as counterexamples are found.

Proof:

This is a sketch of proof. See the appendix for more details.

If αβ\alpha\succcurlyeq\beta is not true, then there exists ξ[0,1]\xi\in[0,1] such that Iα(ξ)<Iβ(ξ)I_{\alpha}(\xi)<I_{\beta}(\xi). Pick a binary string cc such that Iαc(ξ)I_{\alpha c}(\xi) is very, very close to 0, so close that Iαcα1(ξ)<1/2I_{\alpha c\alpha^{-1}}(\xi)<1/2. At the same time, make Iβc(ξ)I_{\beta c}(\xi) very, very close to 11, so close that Iβcβ1(ξ)>1/2I_{\beta c\beta^{-1}}(\xi)>1/2. Then Iαcα1(ξ)<Iβcβ1(ξ)I_{\alpha c\alpha^{-1}}(\xi)<I_{\beta c\beta^{-1}}(\xi), which contradicts αcα1βcβ1\alpha c\alpha^{-1}\succcurlyeq\beta c\beta^{-1}. So αβ\alpha\succcurlyeq\beta must be true. ∎

VII-B Some rules of rules

Since checking α0α1β0β1\alpha 0\alpha^{-1}\succcurlyeq\beta 0\beta^{-1} and α1α1β1β1\alpha 1\alpha^{-1}\succcurlyeq\beta 1\beta^{-1} is straightforward using the procedure described in Section VI, we list some TBM relations as follows.

  • 1

    ϵ

    0
    1\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}\epsilon\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}0
    , where ϵ\epsilon is the empty string.

  • 11

    10

    01

    00
    11\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}10\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}01\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}00
    .

  • 111

    110

    101

    011

    100

    010

    001
    111\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}110\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}101\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}011\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}100\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}010\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}001
    .

  • 1111

    1110

    1101

    1011

    1100

    1010

    1001
    1111\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}1110\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}1101\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}1011\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}1100\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}1010\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}1001
    .

  • 1011

    0111

    1001

    0110

    1000

    0100
    1011\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}0111\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}1001\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}0110\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}1000\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}0100
    .

  • 0110

    0101

    0011

    0100

    0010

    0001

    0000
    0110\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}0101\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}0011\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}0100\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}0010\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}0001\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}0000
    .

As commented before, 10

01
10\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}01
is equivalent to 100230103210023\succcurlyeq 01032; we now know that they both are true. Hence, as claimed before, we have 100m01010m10100^{m}01\succcurlyeq 010^{m}10 for any positive integer mm.

Another example: 100011010110100011\succcurlyeq 010110 and 10

01
10\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}01
imply 100m0011010m0110100^{m}0011\succcurlyeq 010^{m}0110 for any positive integer mm.

Yet another example: 011010100011011010\succcurlyeq 100011 and 011

100
011\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}100
, imply 0110m0101000m0110110^{m}010\succcurlyeq 1000^{m}011 for any positive integer mm.

VII-C Suffix TBM

One might be motivated to make the following definition: α

β
\alpha\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}^{\prime}\beta
if, for any quaternary strings yy and zz,

yαzβimpliesy0αz0β and y1αz1β.y\alpha\preccurlyeq z\beta\qquad\text{implies}\qquad y0\alpha\preccurlyeq z0\beta\text{ and }y1\alpha\preccurlyeq z1\beta.

Nevertheless, this is not a new concept, because α

β
\alpha\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}^{\prime}\beta
is equivalent to β10βα10α\beta^{-1}0\beta\succcurlyeq\alpha^{-1}0\alpha, which is equivalent to β1

α1
\beta^{-1}\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}\alpha^{-1}
.

The following are some suffix TBM relations we found.

  • 1

    ϵ

    0
    1\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}^{\prime}\epsilon\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}^{\prime}0
    . 11

    10

    01

    00
    11\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}^{\prime}10\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}^{\prime}01\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}^{\prime}00
    . 111

    101

    011
    111\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}^{\prime}101\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}^{\prime}011
    . 110

    011

    001
    110\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}^{\prime}011\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}^{\prime}001
    .

  • 101

    010
    101\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}^{\prime}010
    . 110

    100

    001
    110\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}^{\prime}100\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}^{\prime}001
    . 100

    010

    000
    100\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}^{\prime}010\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}^{\prime}000
    .

An example application for suffix TBM: 100010101010101000101\succcurlyeq 0101010 and 10

01
10\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}^{\prime}01
, implies 100010n01010100n10100010^{n}01\succcurlyeq 010100^{n}10 for any positive integer nn.

Another example application for suffix TBM: 001101100010001101\succcurlyeq 100010 and and 101

010
101\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}^{\prime}010
, imply 0010n1011000n0100010^{n}101\succcurlyeq 1000^{n}010 for any positive integer nn.

To the best of our knowledge, all example inequalities given in this section are independent rules. These are particular examples of family of infinitely many rules. In the next section, we relate families of rules to the dominance order of integer partition.

VIII Integer Partition and Dominance Order

For a binary string aa, let π(a)\pi(a) be the integer partition p1+p2++pmp_{1}+p_{2}+\dotsb+p_{m} where pip_{i} is the number of zeros to the right of the iith one in 1a01a0. For instance π(10001)\pi(10001) is 4+4+14+4+1. We claim the following theorem.

Theorem 24

If aa and bb are of the same length and weight, and π(a)\pi(a) dominates π(b)\pi(b) as in the theory of integer partition, then aba\succcurlyeq b.

Proof:

It suffices to prove that, if π(a)\pi(a) covers π(b)\pi(b) in the dominance order, then aba\succcurlyeq b. By a theorem in integer partition, π(a)\pi(a) covers π(b)\pi(b) if aa and bb contain 10ϕm0110\phi^{m}01 and 01ϕm1001\phi^{m}10, respectively, where ϕ{0,1}\phi\in\{0,1\}. But we already know 10ϕm0101ϕm1010\phi^{m}01\succcurlyeq 01\phi^{m}10: they are consequences of 100101101001\succcurlyeq 0110 and 10

01
10\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}01
. ∎

For a binary string bb, let Lindenmayer(b,001,110)\operatorname{Lindenmayer}(b,0{\to}01,1{\to}10) be the resulting string wherein each zero in bb is replaced by 0101 and each 11 by 1010. We claim that there are two more embeddings of the dominance order.

Theorem 25

Same assumptions as Theorem 24. Then Lindenmayer(a\operatorname{Lindenmayer}(a, 0010{\to}01, 110)Lindenmayer(b1{\to}10)\succcurlyeq\operatorname{Lindenmayer}(b, 0010{\to}01, 110)1{\to}10). What’s more, Lindenmayer(a\operatorname{Lindenmayer}(a, 01000{\to}100, 1011)Lindenmayer(b1{\to}011)\succcurlyeq\operatorname{Lindenmayer}(b, 01000{\to}100, 1011)1{\to}011).

Proof:

It suffices to check 100101100110100110010110\succcurlyeq 01101001 and 1001

0110
1001\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}0110
for the first inequality, and 011100100011100011011100011100100011\succcurlyeq 100011011100 and 011100

100011
011100\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}100011
for the second inequality. All of them are checked on a personal computer. ∎

IX Conclusions

This paper addresses the problem of determining if one synthetic channel is always more preferred over another synthetic channel. We use a root-counting algorithm to demonstrate how to determine if a polynomial is nonnegative over [0,1][0,1]. We then extend that to a procedure that determines if an algebraic function is nonnegative over [0,1][0,1]. The latter becomes a tool that can prove infinitely many rules in one go.

References

  • [1] E. Arikan, “Channel polarization: A method for constructing capacity-achieving codes for symmetric binary-input memoryless channels,” IEEE Transactions on Information Theory, vol. 55, no. 7, pp. 3051–3073, July 2009.
  • [2] ——, “A performance comparison of polar codes and reed-muller codes,” IEEE Communications Letters, vol. 12, no. 6, pp. 447–449, June 2008.
  • [3] ——, “A survey of reed-muller codes from polar coding perspective,” in 2010 IEEE Information Theory Workshop on Information Theory (ITW 2010, Cairo), Jan 2010, pp. 1–5.
  • [4] M. Mondelli, S. H. Hassani, and R. L. Urbanke, “From polar to reed-muller codes: A technique to improve the finite-length performance,” IEEE Transactions on Communications, vol. 62, no. 9, pp. 3084–3091, Sep. 2014.
  • [5] B. Li, H. Shen, and D. Tse, “A rm-polar codes,” 2014. [Online]. Available: https://arxiv.org/abs/1407.5483
  • [6] E. Abbe and M. Ye, “Reed-muller codes polarize,” IEEE Transactions on Information Theory, vol. 66, no. 12, pp. 7311–7332, Dec 2020.
  • [7] S. Kudekar, S. Kumar, M. Mondelli, H. D. Pfister, E. Şaşoǧlu, and R. L. Urbanke, “Reed–muller codes achieve capacity on erasure channels,” IEEE Transactions on Information Theory, vol. 63, no. 7, pp. 4298–4316, July 2017.
  • [8] G. Reeves and H. D. Pfister, “Reed-muller codes achieve capacity on bms channels,” 2021. [Online]. Available: https://arxiv.org/abs/2110.14631
  • [9] R. Mori and T. Tanaka, “Performance of polar codes with the construction using density evolution,” IEEE Communications Letters, vol. 13, no. 7, pp. 519–521, July 2009.
  • [10] C. Schürch, “A partial order for the synthesized channels of a polar code,” in 2016 IEEE International Symposium on Information Theory (ISIT), July 2016, pp. 220–224.
  • [11] M. Bardet, V. Dragoi, A. Otmani, and J.-P. Tillich, “Algebraic properties of polar codes from a new polynomial formalism,” in 2016 IEEE International Symposium on Information Theory (ISIT), July 2016, pp. 230–234.
  • [12] M. Mondelli, S. H. Hassani, and R. L. Urbanke, “Construction of polar codes with sublinear complexity,” IEEE Transactions on Information Theory, vol. 65, no. 5, pp. 2782–2791, May 2019.
  • [13] W. Wu and P. H. Siegel, “Generalized partial orders for polar code bit-channels,” IEEE Transactions on Information Theory, vol. 65, no. 11, pp. 7114–7130, Nov 2019.
  • [14] E. Camps, H. H. López, G. L. Matthews, and E. Sarmiento, “Polar decreasing monomial-cartesian codes,” IEEE Transactions on Information Theory, vol. 67, no. 6, pp. 3664–3674, June 2021.
  • [15] V.-F. Drăgoi and G. Cristescu, “Bhattacharyya parameter of monomial codes for the binary erasure channel: From pointwise to average reliability,” Sensors, vol. 21, no. 9, 2021. [Online]. Available: https://www.mdpi.com/1424-8220/21/9/2976
  • [16] B. C. Geiger, “The fractality of polar and reed–muller codes,” Entropy, vol. 20, no. 1, 2018. [Online]. Available: https://www.mdpi.com/1099-4300/20/1/70
  • [17] S. Kahraman, “Strange attractor for efficient polar code design,” 2017. [Online]. Available: https://arxiv.org/abs/1708.04167
  • [18] D. Kim, K. Oh, D. Kim, and J. Ha, “Information set analysis of polar codes,” in 2016 International Conference on Information and Communication Technology Convergence (ICTC), Oct 2016, pp. 813–815.
  • [19] M. Sagraloff and K. Mehlhorn, “Computing real roots of real polynomials,” Journal of Symbolic Computation, vol. 73, pp. 46–86, 2016. [Online]. Available: https://www.sciencedirect.com/science/article/pii/S0747717115000292
  • [20] D. Y. Yun, “On square-free decomposition algorithms,” in Proceedings of the Third ACM Symposium on Symbolic and Algebraic Computation, ser. SYMSAC ’76.   New York, NY, USA: Association for Computing Machinery, 1976, pp. 26–35. [Online]. Available: https://doi.org/10.1145/800205.806320

Appendix A Proof of Theorem 23

For any binary string c1c2cnc_{1}c_{2}\dotsm c_{n},

(αc1α1)(αc2α1)(αcnα1)\displaystyle\kern-10.00002pt(\alpha c_{1}\alpha^{-1})(\alpha c_{2}\alpha^{-1})\dotsm(\alpha c_{n}\alpha^{-1})
(βc1β1)(βc2β1)(βcnβ1).\displaystyle\succcurlyeq(\beta c_{1}\beta^{-1})(\beta c_{2}\beta^{-1})\dotsm(\beta c_{n}\beta^{-1}).

This holds because each αciα1βciβ1\alpha c_{i}\alpha^{-1}\succcurlyeq\beta c_{i}\beta^{-1} is a consequence of α

β
\alpha\mathrel{\ooalign{$\succcurlyeq$\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.8}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.64}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.512}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.4096}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.32768}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.26214}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr\raisebox{2.9pt}{\kern 1.0pt\scalebox{0.20972}{\kern-1.0pt\raisebox{-2.5pt}{$\succ$}}}\cr}}\beta
. Therefore, we will have αcα1βcβ1\alpha c\alpha^{-1}\succcurlyeq\beta c\beta^{-1} for all binary strings cc.

Next, suppose αβ\alpha\succcurlyeq\beta is not true, i.e., there exists ξ[0,1]\xi\in[0,1] such that Iα(ξ)<Iβ(ξ)I_{\alpha}(\xi)<I_{\beta}(\xi). Let AIα(ξ)A\coloneqq I_{\alpha}(\xi) and let BIβ(ξ)B\coloneqq I_{\beta}(\xi).

We now attempt to construct capacity-achieving polar codes over BECs with capacities 1A1-A and BB, respectively. Since 1A+B>11-A+B>1, i.e., the sum of the capacities of these two channels exceed one, the bitwise complement of the information set of the former overlaps the information set of the latter provided that the block length is large enough. That is, for sufficiently large block lengths, there is some binary string cc such that c~\tilde{c} is in the information set of a polar code over BEC with capacity 1A1-A and cc is in the information set of a polar code over BEC with capacity BB.

Recall that polar code has exponentially small error probabilities. Therefore, for arbitrarily small ε>0\varepsilon>0, we will see

Ic~(1A)>1εandIc(B)>1εI_{\tilde{c}}(1-A)>1-\varepsilon\quad\text{and}\quad I_{c}(B)>1-\varepsilon

as long as cc is long enough and taken from the intersection. Using I0(1x)=1I1(x)I_{0}(1-x)=1-I_{1}(x), the inequalities above are equivalent to

Iαc(ξ)=Ic(A)<εandIβc(ξ)=Ic(B)>1ε.I_{\alpha c}(\xi)=I_{c}(A)<\varepsilon\quad\text{and}\quad I_{\beta c}(\xi)=I_{c}(B)>1-\varepsilon.

That is, cc is such that Iαc(ξ)I_{\alpha c}(\xi) is very close to 0 and Iβc(ξ)I_{\beta c}(\xi) is very close to 11. If we choose ε\varepsilon to be really, really small, we will see

Iαcα1(ξ)<Iα1(ε)<1/2I_{\alpha c\alpha^{-1}}(\xi)<I_{\alpha^{-1}}(\varepsilon)<1/2

and

Iβcβ1(ξ)>Iβ1(1ε)>1/2.I_{\beta c\beta^{-1}}(\xi)>I_{\beta^{-1}}(1-\varepsilon)>1/2.

This contradicts the fact that αcα1βcβ1\alpha c\alpha^{-1}\succcurlyeq\beta c\beta^{-1}, so it must be the case that αβ\alpha\succcurlyeq\beta is true. This finishes the proof.

Consider the preceding proof similar to [13, Proposition 1].