Derivation of context monotonicity. Diagram multiplication is increasing in each factor. If \(\tau(u)\sqsubseteq\tau(v)\), then \[\lambda\tau(\alpha)\tau(u)\tau(\beta)\rho \ \sqsubseteq\ \lambda\tau(\alpha)\tau(v)\tau(\beta)\rho.\] The designated forward edge persists under this inclusion. Applying (5) proves (6). ◻

Proof. Apply Lemma 3 to the complementing machine, and let \(S=\tau(\Sigma_H^*)\). Suppose \(\tau(u)\sqsubseteq\tau(v)\). For each \(p,q\in H\), take the one-letter words \[\alpha=I_{\{p\}},\qquad \beta=I_{\{q\}}.\] They belong to \(\Sigma_H\), and \[I_{\{p\}}r(u)I_{\{q\}} = \begin{cases} \{(p,q)\},& (p,q)\in r(u),\\ \varnothing,&(p,q)\notin r(u). \end{cases}\] Since the machine accepts exactly the words with empty relation product, (6) implies \[(p,q)\notin r(u) \quad\Longrightarrow\quad (p,q)\notin r(v).\] Thus \[ \tau(u)\sqsubseteq\tau(v) \quad\Longrightarrow\quad r(v)\subseteq r(u). \tag{8}\]

If \(\tau(u)=\tau(v)\), applying (8) in both directions yields \(r(u)=r(v)\). Therefore \[\phi:S\longrightarrow\mathcal R_H, \qquad \phi(\tau(w))=r(w),\] is well-defined. Concatenation of words proves multiplicativity, and the empty word proves preservation of the identity. It is surjective because every relation in \(\mathcal R_H\) is itself a letter of \(\Sigma_H\). Equation (8) is exactly the required order reversal (7). ◻

Proof. The returns of \(e\) persist in both \(z\) and \(w\), so \((L_wR_z)^*\supseteq K_e\). Formula (2) therefore gives \(U_e^+(zw)\supseteq U_e^+(z)U_e^+(w)\). Two loops at the same point compose to a loop. For the negative sign the corresponding product is \(U_e^-(w)U_e^-(z)\), which gives the same conclusion. Finally \(U_e^\sigma(e)=P_e^\sigma\), so no recurrent class is missing from \(e\). ◻

Proof. Containment in \(F_e\) follows from \(F_eK_eF_e=F_e\). The identities \[(F_eK_e)P_e=F_eK_e,\qquad P_e(K_eF_e)=K_eF_e\] show that replacing \(p\) by a mutually \(P_e\)-related point does not change either factor of the rectangle.

To prove coverage, (10) implies \(F_eP_e^kF_e=F_e\) for every \(k\ge1\). Given a pair in \(F_e\), choose a witness for this expression with \(k>m\). Some label repeats along the \(P_e\) portion. That label \(p\) is recurrent, since a nonempty \(P_e\)-path from \(p\) back to itself is a \(P_e\)-edge by transitivity. The portions before and after \(p\) belong to \(F_eK_e\) and \(K_eF_e\): indeed \(F_eP_e^j\subseteq F_eK_e\) and \(P_e^jF_e\subseteq K_eF_e\) for \(j\ge0\), including \(j=0\) since \(K_e\) is reflexive.

If \(C\) is not missing from \(z\), insert \(pK_eF_zK_ep\) between the two halves of its rectangle. The resulting relation is contained in \(F_eK_eF_zK_eF_e\subseteq F_z\) by (13). Reflection proves the backward assertion. When the missing set is empty all through edges of \(e\) are thus present in \(z\), and its return edges persist by (12). ◻

Proof. For each positive class of \(\mathcal C_d\), choose a representative \(x\) and a witness for \(xK_d^+F_{uev}K_d^+x\). Expand the middle edge into an actual finite path through the three diagrams \(u,e,v\). For a negative class do the same with \(xK_d^-B_{uev}K_d^-x\). Make these choices once, independently of \(z\).

For every occurrence of a through edge of the middle factor \(e\) on a chosen path, choose an \(e\)-class whose rectangle covers that edge, using Lemma 6. Mark a \(d\)-class if any class chosen along its witness lies in \(J\); let \(J'\) be the marked set. If a class is unmarked, all its chosen through edges survive replacement of \(e\) by \(z\), as do all return edges of \(e\). Its original outer \(K_d^\sigma\) pieces remain fixed. Thus its witness is a loop in \(U_d^\sigma(uzv)\), and the class is not missing. This proves the required common-set inclusion.

It remains to count marked classes. For each \(d\)-class \(C\), let \(S_C\) be the set of \(e\)-classes chosen along its fixed witness. We show that the sets \(S_C\) are pairwise disjoint among \(d\)-classes of a fixed sign. Consider two positive witnesses, written as \[xK_d^+\alpha\;F_d\;\beta K_d^+x, \qquad yK_d^+\alpha'\;F_d\;\beta'K_d^+y,\] where \(\alpha,\beta,\alpha',\beta'\in D^+\) and the displayed \(F_d\)-edges have been expanded through \(u,e,v\). Suppose the expanded paths use occurrences of middle-factor edges \((a,b)\) and \((a',b')\) covered by one \(e\)-class. Its rectangle also contains \((a,b')\) and \((a',b)\). The sign of that \(e\)-class fixes the orientation of both edges and their entry and exit boundaries inside the three-factor product. Thus the prefix ending at \(a\), the crossed edge \((a,b')\), and the suffix starting at \(b'\) concatenate to a path from \(\alpha\) to \(\beta'\). Neither retained subpath has an earlier outer exit. The concatenation is therefore a valid finite path for \(F_d\), even if it repeats internal crossings or its selected middle edge points backward. Interchanging the two prefixes and suffixes similarly gives \(\alpha'F_d\beta\).

The original exterior factors now give \(xP_d^+y\) and \(yP_d^+x\), so \(x\) and \(y\) belong to the same recurrent class. Reflection gives the same conclusion for negative witnesses, with \(B_d\) in place of \(F_d\). This proves the asserted disjointness for each sign. A witness using only returns of \(e\) has \(S_C=\varnothing\) and is never marked. Since \(J'=\{C:S_C\cap J\ne\varnothing\}\), at most \(|J|\) classes of each sign are marked, and \(|J'|\le2|J|\). ◻

Proof. Every element \(w\) of a finite semigroup has an idempotent positive power: the sequence of powers is eventually periodic, so a sufficiently large exponent divisible by its eventual period gives \(w^{2k}=w^k\). Applying this to a preimage of \(q\) gives an idempotent preimage of \(q\). Finiteness then gives one minimal in the nesting order.

For any \(y\in qMq\), choose \(x\in A\) with \(\theta(x)=y\). Then \(\theta(dxd)=qyq=y\), proving surjectivity on the corner; its identity \(d\) maps to \(q\). Now let \(w\in dAd\) have unit image. An idempotent power \(w^k\) has an image that is both a unit and an idempotent in \(qMq\), hence equals \(q\). Since \(w^k\trianglelefteq d\), minimality gives \(w^k=d\). If \(k>1\), the element \(w^{k-1}\) is a two-sided inverse of \(w\) in \(dAd\); if \(k=1\), then \(w=d\) is already the identity. ◻

Proof. Using \(P^2=P\) and \(iPi=i\), we obtain \[Q^2=Q,\qquad PQ=QP=Q,\qquad Qi=Pi,\qquad iQ=iP,\qquad iQi=i.\] If \(Z=QZQ\), then \(PZP=Z\), and therefore \[Z=PiPZPiP=PiZiP.\] Thus restriction determines \(Z\) uniquely. Conversely, for a relation \(A=iAi\) supported on \(F\), the relation \(PAP\) belongs to \(Q\mathcal R_HQ\), since \(PAP=QAQ\), and \[i(PAP)i=(iPi)A(iPi)=A.\] This proves bijectivity with the claimed inverse. For supported relations \(A,B\in\mathcal R_F\), \[(PAP)(PBP)=PAPBP =PA(iPi)BP =PABP.\] Hence the inverse, and therefore restriction, preserves multiplication. Finally \(\rho(Q)=i\), the identity of \(\mathcal R_F\). ◻

Proof. We induct on \(h\), simultaneously over all the data in the statement, including \(m\), \(e\), \(S\), and \(\phi\). For \(2\leq h\leq2t\), we have \(D(h)=1\). If \(\mathcal M_e(a)\) were empty, Lemma 6 would give \(e\sqsubseteq a\). Order reversal would then give \(I_H\cup\{(x,y)\}\subseteq I_H\), a contradiction.

Assume henceforth that \(h\geq2t+1\), and put \(c=|\mathcal M_e(a)|\). We will construct \(t^2\) nested steps with total missing-set size at most \(16tc\). Each step will contain a smaller instance of the Proposition, on \(h-2t+1\) points.

Step 1: A common budget for all pair additions. Choose disjoint sets \[U=\{u_1,\ldots,u_t\},\qquad V=\{v_1,\ldots,v_t\},\qquad \{z\}\] in \(H\). Conjugating \(a\) by unit lifts of permutations gives elements \(s_i,s'_j\in S\) with \[ \phi(s_i)=I_H\cup\{(u_i,z)\},\qquad \phi(s'_j)=I_H\cup\{(z,v_j)\}. \tag{22}\] Indeed, permutation conjugation acts transitively on ordered pairs of distinct points, and the inverse of a unit lift maps to the inverse permutation. Explicitly, a unit \(p\in S\) gives the conjugate \(pap^{-1}\), with \(pep^{-1}=e\). Applying Lemma 7 with \(J=\mathcal M_e(a)\) therefore gives \[|\mathcal M_e(s_i)|\leq2c,\qquad |\mathcal M_e(s'_j)|\leq2c.\] Consequently the single set \[J=\bigcup_{i=1}^t\mathcal M_e(s_i) \ \cup\ \bigcup_{j=1}^t\mathcal M_e(s'_j) \ \subseteq\mathcal C_e\] has \(|J|\leq4tc\), and the product inequality of Lemma 5 gives \(\mathcal M_e(s_i s'_j)\subseteq J\) for every \(i,j\).

Let \(P_0=I_{H\setminus\{z\}}\). Choose an idempotent lift \(b_0\in S\) of \(P_0\), by taking an idempotent positive power of any lift, and define \[g_{ij}=b_0s_i s'_j b_0\in b_0Sb_0.\] The image of \(s_i s'_j\) consists of the identity and the three pairs \((u_i,z)\), \((z,v_j)\), and \((u_i,v_j)\). The outer factors \(P_0\) remove the first two, so \[ \phi(g_{ij})=P_0\cup\{(u_i,v_j)\}. \tag{23}\] Figure 3 illustrates this conversion of two generator families into a family indexed by \(U\times V\).

Since \(b_0eb_0=b_0\), the common-set conclusion of Lemma 7 gives a single set \(J_0\subseteq\mathcal C_{b_0}\) such that \[ |J_0|\leq8tc,\qquad \mathcal M_{b_0}(g_{ij})\subseteq J_0 \quad(1\leq i,j\leq t). \tag{24}\]

Step 2: A nested chain spending that budget. List the \(t^2\) pairs of \(U\times V\) in any order, without repetitions. Let \(E_\ell\) be the set of the first \(\ell\) pairs, and put \(P_\ell=P_0\cup E_\ell\) for \(0\leq\ell\leq t^2\). For any \(E,E'\subseteq U\times V\), \[ (P_0\cup E)(P_0\cup E')=P_0\cup E\cup E'. \tag{25}\] To check this, \(P_0\) acts as the identity on all the endpoints in question, and no pair of \(E\) can be followed by a pair of \(E'\), because \(U\cap V=\varnothing\). In particular, every \(P_\ell\) is idempotent.

If the pair at position \(\ell\) is \((u_i,v_j)\), choose \(b_\ell\) to be an idempotent positive power of \(b_{\ell-1}g_{ij}b_{\ell-1}\). Inductively, Equation (25) gives \(\phi(b_\ell)=P_\ell\). The sandwich, and hence all its positive powers, is absorbed on both sides by \(b_{\ell-1}\). Thus \[b_\ell\trianglelefteq b_{\ell-1} \qquad(1\leq\ell\leq t^2).\] All these elements lie in the \(b_0\)-corner. Starting with \(\mathcal M_{b_0}(b_0)=\varnothing\), repeated use of Lemma 5 and Equation (24) shows that \[\mathcal M_{b_0}(b_\ell)\subseteq J_0 \qquad(0\leq\ell\leq t^2).\] Here taking a positive power cannot enlarge the missing set: all factors have the same missing set, and their union is unchanged. Proposition 10 now yields \[ \sum_{\ell=1}^{t^2}\delta_\ell\leq16tc, \qquad \delta_\ell=|\mathcal M_{b_{\ell-1}}(b_\ell)|. \tag{26}\] We have bounded the total cost of the chain using only the \(2t\) original conjugates. It remains to give an inductive lower bound for each of its \(t^2\) steps.

Step 3: A smaller instance inside every step. Fix \(\ell\), let \((u_i,v_j)\) be its newly added pair, and write \(b=b_{\ell-1}\) and \(P=P_{\ell-1}\). Retain the two endpoints of this pair and all points outside the construction: \[F=\{u_i,v_j\}\cup \bigl(H\setminus(U\cup V\cup\{z\})\bigr), \qquad i_F=I_F,\qquad Q=Pi_FP.\] Then \(|F|=h-2t+1\geq2\). Among the possible extra pairs of \(P\), only \((u_i,v_j)\) has both endpoints in \(F\), and this pair has not yet been added. Therefore \(i_FPi_F=i_F\). By Lemma 12, \(Q\trianglelefteq P\) and restriction gives \(Q\mathcal R_HQ\simeq\mathcal R_F\). Moreover, Equation (25) gives \(PP_\ell P=P_\ell\). Using \(i_FQ=i_FP\) and \(Qi_F=Pi_F\), we obtain \[ i_F(QP_\ell Q)i_F =i_FP_\ell i_F =I_F\cup\{(u_i,v_j)\}. \tag{27}\]

Consider the finite monoid \(A=bSb\). The restriction of \(\phi\) maps it onto \(P\mathcal R_HP\): sandwiching any preimage by \(b\) gives a preimage of its \(P\)-sandwich. Apply Lemma 11 inside \(A\) to the idempotent \(Q\). We obtain an idempotent \(d\in A\) with \(\phi(d)=Q\), minimal there among idempotent lifts of \(Q\). Its corner \(dAd\) maps unitally onto \[Q(P\mathcal R_HP)Q=Q\mathcal R_HQ,\] and all units of this image have unit lifts. Composing with restriction gives a unital surjective homomorphism \[ \psi:dAd\longrightarrow\mathcal R_F, \qquad \psi(w)=i_F\phi(w)i_F. \tag{28}\] This map is order-reversing because \(\phi\) is and restriction preserves inclusion. It has unit lifts of every permutation of \(F\), by the isomorphism in Lemma 12. Also \(dAd\) is a submonoid of \(d\mathcal T_md\) with identity \(d\). These observations verify all the map and domain hypotheses needed for induction.

Because \(b_\ell\trianglelefteq b\), we have \(b_\ell\in A\). By Equation (27), the element \(db_\ell d\in dAd\) maps under \(\psi\) to \(I_F\cup\{(u_i,v_j)\}\). This relation is idempotent, so an idempotent positive power \(v\) of \(db_\ell d\) has the same image. Since \(d\in A\) is idempotent, \(dbd=d\). Apply Lemma 7 from the identity \(b\) to the identity \(d\), with context \((d,d)\) and missing set \(\mathcal M_b(b_\ell)\). Then apply the power consequence of Lemma 5 in the \(d\)-corner. This gives \[ |\mathcal M_d(v)| \leq |\mathcal M_d(db_\ell d)| \leq 2\delta_\ell. \tag{29}\] The induction hypothesis applies to \(d\), \(dAd\), \(\psi\), and \(v\), with the smaller parameter \(|F|=h-2t+1\). It follows that \[2\delta_\ell\geq D(h-2t+1).\]

Summing this lower bound and using Equation (26), we conclude that \[16tc\ \geq\ \frac{t^2}{2}D(h-2t+1), \qquad c\ \geq\ \frac{t}{32}D(h-2t+1).\] For \(t=64\), the last expression is \(2D(h-127)=D(h)\), by the definition of \(D\). This completes the induction. ◻

Proof of Theorem 2. Apply Lemma 11 to \(\phi_0\) and the idempotent \(I_H\). It supplies an idempotent \(e\in S_0\) such that \(S=eS_0e\) maps unitally onto \(\mathcal R_H\) and every permutation has a unit lift. The restricted map retains order reversal, and \(S\) is a submonoid of \(e\mathcal T_me\) with identity \(e\).

Choose distinct \(x,y\in H\) and any lift in \(S\) of \(I_H\cup\{(x,y)\}\). An idempotent positive power \(a\) of that lift has the same image. Proposition 13 therefore gives \[D(h)\leq|\mathcal M_e(a)|\leq|\mathcal C_e|\leq2m,\] as required. ◻

Proof. Use one initial state \(q_{\mathrm{in}}\), the \(h\) states in \(H\), and one accepting state \(q_{\mathrm{acc}}\), all distinct. From \(q_{\mathrm{in}}\) on the left endmarker, the machine moves right into any chosen state of \(H\). On a letter \(R\in\mathcal R_H\), it may move right from \(p\in H\) to \(q\in H\) precisely when \((p,q)\in R\). At the right endmarker, every state in \(H\) has a stay transition to \(q_{\mathrm{acc}}\). There are no other transitions, and \(q_{\mathrm{acc}}\) is the only accepting state.

On \(R_1\cdots R_k\), an accepting computation is exactly a sequence \(p_0,\ldots,p_k\in H\) with \((p_{i-1},p_i)\in R_i\) for \(1\leq i\leq k\). Such a sequence exists exactly when the relation product is nonempty. For \(k=0\), the initial move reaches the right endmarker directly, and the machine accepts. This agrees with \(r(\varepsilon)=I_H\ne\varnothing\). ◻

Proof of Lemma 3. Let \(B\) be the \(s\)-state automaton in the lemma, with state set \(Q\) and initial state \(q_0\). Introduce one new state \(q_\dagger\). From every original accepting state, at every cell, add a stay transition to \(q_\dagger\). In state \(q_\dagger\), move right regardless of the scanned symbol, finally exiting past the right endmarker in state \(q_\dagger\). This last exit is only a device for representing acceptance, not a transition of the original machine. All original transitions remain subject to the endmarker restrictions.

A finite augmented computation from the original initial configuration to the designated exit exists if and only if \(B\) accepts. Indeed, an accepting original computation can be followed by the added stay and rightward sweep. Conversely, the first entry into \(q_\dagger\) must come from an original accepting configuration. This argument includes the case that \(q_0\) itself is accepting. Infinite computations create no additional finite successful computation.

Put \(\widehat Q=Q\cup\{q_\dagger\}\) and \(m=s+1\). Take the directional label sets to be two disjoint copies \[D^+=\{q^+:q\in\widehat Q\}, \qquad D^-=\{q^-:q\in\widehat Q\}.\] For a cell symbol \(c\), including either endmarker with its boundary rules, let \(E_c\) be the relation on \(\widehat Q\) given by the augmented stay transitions. Let \(T_c^+\) and \(T_c^-\) be the relations given by the augmented rightward and leftward transitions, respectively; their second coordinates record the state after the move. At the right endmarker, \(T_c^+\) includes only the designated augmented exit, and at the left endmarker \(T_c^-\) is empty. Define a diagram \(d_c\) by \[\begin{align*} (q^+,p^+)\in F_{d_c} &\quad\Longleftrightarrow\quad (q^-,p^+)\in R_{d_c} \quad\Longleftrightarrow\quad (q,p)\in E_c^*T_c^+,\\ (q^-,p^-)\in B_{d_c} &\quad\Longleftrightarrow\quad (q^+,p^-)\in L_{d_c} \quad\Longleftrightarrow\quad (q,p)\in E_c^*T_c^-. \end{align*}\] Thus each local diagram edge represents a finite sequence of stays, possibly empty, followed by one move out of the cell. The incoming sign specifies the side of entry, not additional machine memory; the transition rules themselves depend only on the state and symbol.

Set \(\lambda=d_{\mathrm{left}}\) and \(\rho=d_{\mathrm{right}}\) for the two endmarkers, and set \[\tau(c_1\cdots c_k)=d_{c_1}\cdots d_{c_k}, \qquad \tau(\varepsilon)=1_{\mathcal T_m}.\] This is a monoid homomorphism. Every finite augmented computation ending in the designated exit decomposes into successive visits to individual cells, each consisting of finitely many stays and one exit move. These visits give a path through the product of the cell diagrams. In the opposite direction, each local edge in a finite diagram path has a finite transition witness. Expanding these witnesses and concatenating them gives an augmented computation, because the exit state from one cell is exactly the entry state to the next. Neither direction assumes that a cut is crossed at most once.

The fictitious entry into the left endmarker with label \(q_0^+\) represents the initial configuration; it is not an additional machine transition. No path can leave the tape to the left, and a path can leave to the right only through the designated exit. Hence (5) holds with \(a=q_0^+\) and \(b=q_\dagger^+\). For the empty word, the two endmarker cells are adjacent, and the identity \(\tau(\varepsilon)\) gives precisely their product. A stay cycle causes no difficulty: only its finite traversals are represented in \(E_c^*\). ◻

Proof of Theorem 1. For any \(n\geq4\), let \(h=n-2\), choose a set \(H\) of size \(h\), and use the \(n\)-state source automaton from Lemma 14. If an \(s\)-state 2NFA recognizes its complement, then Proposition 4 supplies the order-reversing relation image required by Theorem 2. With \(m=s+1\), that bound gives \[2(s+1)\geq 2^{\lfloor(h-2)/127\rfloor} =2^{\lfloor(n-4)/127\rfloor}.\] Rearranging proves the stated lower bound. Since its right-hand side grows exponentially with \(n\), no fixed polynomial can bound the complementation cost for all finite alphabets. ◻

Proof. We use only the linear-overhead conclusion of (Geffert et al. 2007), allowing constant-factor changes for model conventions. The standard marker model and its normalization are described in the precursor (Geffert et al. 2005, sec. 2 and Lemma 3.1). Stay moves can be replaced by a two-step excursion that stores the destination state and the return direction in a fixed number of copies of the state set. The excursion goes left at the right endmarker and right elsewhere. Even on the empty word, the two distinct endmarker cells provide the needed adjacent cell. Auxiliary states are nonaccepting, and the destination state is entered only on returning to the original cell. A reached accepting configuration, including the initial configuration, can instead start a fixed marker sweep to a designated accepting halt. Missing transitions can halt and reject. These changes require \(O(s+1)\) states for an \(s\)-state 2DFA and preserve finite acceptance. The cited transformation supplies the substantive additional step of handling infinite nonaccepting computations.

Thus an \(s\)-state deterministic recognizer for \(L(A_n)\) has a deterministic complement, also a 2NFA, with at most \(C(s+1)\) states for an absolute constant \(C\). Theorem 1 gives \[C(s+1)\ge \tfrac12\,2^{\lfloor(n-4)/127\rfloor}-1.\] For all sufficiently large \(n\) this implies the asserted bound with an absolute \(c>0\). Since the same alphabets are finite for every \(n\), it also excludes every polynomial bound uniform over alphabets. ◻