a62ba7d 295faa5
================================================================================
TWO-WAY NONDETERMINISTIC FINITE AUTOMATA CANNOT BE COMPLEMENTED
WITH POLYNOMIALLY MANY STATES
================================================================================

A complete, self-contained proof written to be read by a motivated
high-school student.  Every symbol is defined before it is used, and every
claim is proved.  The theorem is genuinely deep, so the proof is long; we
break it into small steps and explain the idea behind each step.

--------------------------------------------------------------------------------
0.  THE RESULT
--------------------------------------------------------------------------------

Fix an integer n >= 4.  Write

    h = n - 2 .

Let H be a set with h elements, and let Sigma be the set of ALL binary
relations on H (we recall below what a relation on H is).  A "two-way
nondeterministic finite automaton" (2NFA) is a finite machine with a single
read-only head that can move left or right along its input.

We will build an n-state 2NFA A_n over the alphabet Sigma.  It recognizes a
simple language (the "liveness language" L_H defined in section 2).

THEOREM (main).  Every 2NFA that recognizes the complement of the language
of A_n has at least

    (1/2) * 2^floor( (n-4)/127 )  -  1

states.  In particular, no single polynomial in n bounds, uniformly over all
finite alphabets, the number of states needed to complement an n-state 2NFA.

The number 127 will come from a parameter t = 64, with 2t - 1 = 127.  The
exponential grows very slowly at first, but it is exponential, and that is
all that matters for ruling out a polynomial bound.

The proof has three layers, which we build from the ground up.

  (1) REPRESENTATION.  Any 2NFA computation on a segment of the tape can be
      summarized by four relations ("a path diagram").  This turns machine
      behaviour into a finite algebraic object.

  (2) REDUCTION.  A machine that recognizes the COMPLEMENT of the liveness
      language forces a surjective map from path diagrams onto relations that
      REVERSES inclusion.  The automaton question becomes: how small can a
      path-diagram monoid be if it maps onto the relation monoid in an
      inclusion-reversing way?

  (3) ALGEBRA.  An inclusion-reversing surjection onto the relation monoid on
      h points needs a domain with at least 2^floor((h-2)/127) "recurrent
      classes".  A diagram monoid with m labels per side has at most 2m
      recurrent classes, so 2m must be that large.

Layer (3) is where nearly all the work lives.  It is proved by counting how a
nested chain of idempotent diagrams can "lose" recurrent classes.

--------------------------------------------------------------------------------
1.  TWO-WAY AUTOMATA
--------------------------------------------------------------------------------

An alphabet is a finite set; its elements are letters.  A word is a finite
sequence of letters; the empty word has length 0 and is written epsilon.
Sigma^* is the set of all words over Sigma.

A two-way nondeterministic finite automaton (2NFA) with s states consists of

  - a finite set Q of s states, with one distinguished initial state q0 and
    a set of accepting states;
  - a finite alphabet Sigma ;
  - a rule that, for each state and each scanned symbol (a letter, or one of
    the two endmarkers), lists zero or more allowed moves.  A move replaces
    the state and shifts the head one cell left, one cell right, or not at
    all.

The tape holds the input word c_1 c_2 ... c_k in cells 1,...,k, with a LEFT
ENDMARKER in cell 0 and a RIGHT ENDMARKER in cell k+1.  The head may not
leave cells 0 .. k+1.  The machine starts in state q0 on the left endmarker.

A configuration is a pair (state, cell).  A computation is a sequence of
configurations where each is an allowed move from the previous one.  The
machine ACCEPTS the input if some finite computation starts at the initial
configuration (q0, cell 0) and reaches a configuration whose state is
accepting.  In particular, if q0 is accepting, the machine accepts at once.
A branch with no available move dies, so that branch rejects.  An infinite
nonaccepting computation does not accept.

The complement of a language L (a subset of Sigma^*) is Sigma^* minus L.

We count all states, including q0 and the accepting states.  A deterministic
two-way automaton (2DFA) is one with at most one available move from every
state and scanned symbol.

--------------------------------------------------------------------------------
2.  THE LIVENESS LANGUAGE AND ITS SMALL MACHINE
--------------------------------------------------------------------------------

A binary relation on a set X is a set of ordered pairs, i.e. a subset of
X x X.  We write "a R b" as shorthand for "(a,b) is in R".  For example,
on X = {1,2,3}, the relation R = {(1,2),(2,3)} says 1 R 2 and 2 R 3.

Relations compose in PATH ORDER: a (R S) b holds iff there is some c with
a R c and c S b.  So we apply R first and then S.  In the example above,
R R = {(1,3)}: from 1 we reach 2 via R, then 3 via R; no other pairs
survive.  The EMPTY relation (the empty set of pairs) has no pairs at all,
and the IDENTITY relation I_X = {(p,p) : p in X} leaves every p fixed.

Fix the set H of h = n-2 points.  Let

    R_H  =  { all binary relations on H } ,
    Sigma =  R_H      (this is our input alphabet) ,
    I_H   =  { (p,p) : p in H }     (the identity relation) .

For a word w = R_1 R_2 ... R_k (each R_i a relation, hence a letter), define
the product

    r(w)  =  R_1 R_2 ... R_k          (path-order composition),
    r(epsilon) = I_H .

It is the running product of the relations read so far.  Define the
RELATION-PRODUCT LIVENESS LANGUAGE

    L_H  =  { w in Sigma^* :  r(w) is not the empty relation } .

Because H is nonempty, r(epsilon) = I_H is nonempty, so the empty word is in
L_H.

LEMMA 2.1 (a small source machine).
L_H is recognized by a 2NFA with exactly h+2 = n states.

PROOF.  The states are: one initial state q_in; one state p for each point p
of H; and one accepting state q_acc.  That is h+2 states.

The moves are:
  - At the left endmarker, q_in moves right into any chosen state p in H.
  - If the head is at a cell holding the letter R and the state is p in H,
    the machine may move right into state q in H exactly when p R q holds.
    (It may try every such q; this is the nondeterminism.)
  - At the right endmarker, every state p in H has a single STAY move into
    q_acc.
  - There are no other moves.

Run the machine on the word R_1 ... R_k.  After the initial guess it is in
some p_0 at cell 1.  Each later right move reads one letter and replaces
p_{i-1} by p_i with p_{i-1} R_i p_i.  So an accepting computation exists
exactly when there is a chain

    p_0 , p_1 , ... , p_k    with    p_{i-1} R_i p_i  for all i.

Such a chain exists exactly when the product R_1 ... R_k is nonempty: a pair
(p_0, p_k) lies in the product iff it is the two ends of some such chain.  So
the machine accepts w iff r(w) is nonempty.  For the empty word the guessed
p_0 sits immediately on the right endmarker and stays into q_acc, so the
empty word is also accepted, matching r(epsilon) = I_H nonempty.  QED

--------------------------------------------------------------------------------
3.  PATH DIAGRAMS
--------------------------------------------------------------------------------

A "path diagram" summarizes everything a stretch of tape can do: how a head
entering the stretch on a given side can leave it.  Fix an integer m >= 1.
Introduce two disjoint copies of an m-element label set, written

    D+  and  D- .

Think of D+ labels as "moving/standing for a rightward pass" and D- labels as
the leftward counterpart; the two copies are kept separate so that a right
move and a left move are never confused.

A path diagram  a  consists of four binary relations

    F_a  subset of  D+ x D+      through, positive
    B_a  subset of  D- x D-      through, negative
    L_a  subset of  D+ x D-      return, to the left
    R_a  subset of  D- x D+      return, to the right

Picture a rectangular segment of tape.  A head may enter it on the left with
a label from D+ or on the right with a label from D-.  The four relations say
where it can come out:

    F_a : enter left (D+), exit right (D+)      (pass straight through)
    L_a : enter left (D+), exit left  (D-)      (leave on the same side)
    B_a : enter right (D-), exit left (D-)      (pass straight back)
    R_a : enter right (D-), exit right (D+)     (leave on the same side)

F_a and B_a are the THROUGH relations; L_a and R_a are the RETURN relations.

PRODUCT.  Glue a diagram a on the left to a diagram b on the right, matching
the two copies of the label set at the shared boundary (an exit of a becomes
an entry of b with the same label).  The result is again a path diagram a b,
with

    F_ab = F_a (L_b R_a)* F_b
    B_ab = B_b (R_a L_b)* B_a
    L_ab = L_a  union  F_a (L_b R_a)* L_b B_a
    R_ab = R_b  union  B_b R_a (L_b R_a)* F_b .

Here X* means "zero or more repetitions of X" (the reflexive transitive
closure of a relation).  To see the first formula: a forward path crosses a
(F_a) to the shared boundary with a D+ label, then may bounce across the
boundary any number of times -- leaving b on its far side (L_b, now a D-
label) and coming back through a (R_a, again a D+ label), which is the block
(L_b R_a) -- and finally crosses b (F_b).  The other three formulas are the
same story started from the other side or ending on the other side; the
fourth, for instance, reads "cross b backwards, bounce with (R_a L_b)*, and
cross back through a and forward through b".

The product is associative: gluing segments left to right does not depend on
the order of gluing, because a long path is simply cut into blocks and each
block's effect can be replaced by one edge of its own diagram.  The IDENTITY
diagram has F and B equal to the identity relations on D+ and D- and L, R
empty.  So the diagrams on m labels form a finite MONOID, written T_m.

INCLUSION.  Write a is contained in b (a <= b, or "a sqsubseteq b") when each
of the four relations of a is contained in the matching relation of b.  Any
product is increasing in each factor under this order: adding possible paths
to a diagram can only add possible paths to a product.

REFLECTION.  Swapping D+ with D-, swapping F with B, and swapping L with R
turns a diagram into its mirror image, and turns a product ab into the
product (mirror b)(mirror a).  So any statement about the positive sign has a
mirror statement about the negative sign.  We will often prove only the
positive sign and quote reflection.

--------------------------------------------------------------------------------
4.  FROM A MACHINE TO A PATH DIAGRAM: THE REPRESENTATION LEMMA
--------------------------------------------------------------------------------

The next lemma is the bridge between automata and algebra.  It says that one
diagram per input symbol, multiplied along the word, records exactly which
computations of a given 2NFA succeed.  The machine may loop forever or cross
any point of the tape any number of times; the diagram records only finite
successful traversals.

LEMMA 4.1 (representation).  Let B be an s-state 2NFA over a finite alphabet
Sigma, with state set Q and initial state q0.  With m = s+1 there are

  - a monoid homomorphism  tau : Sigma^* --> T_m ,
  - two fixed endmarker diagrams  lambda, rho  in T_m ,
  - two fixed labels  a, b  in D+ ,

such that for every word w

    w is accepted by B    if and only if    (a,b) is in F_{ lambda tau(w) rho } .

Moreover, if tau(u) <= tau(v), then for all words alpha, beta

    alpha u beta is accepted   implies   alpha v beta is accepted.

PROOF.  Augment B with one fresh state q_exit and a "success exit":

  - keep all original moves of B;
  - for every accepting state q of B and every scanned symbol c, add a STAY
    move q --> q_exit ;
  - in state q_exit add a RIGHT move to q_exit on every scanned symbol;
  - at the RIGHT endmarker, in state q_exit, add one special RIGHT move that
    LEAVES the tape to the right.  Call taking this move the "success exit".
    It is bookkeeping, not a real move of B.

A finite computation of the augmented machine that starts at the initial
configuration (q0 on the left endmarker) and ends by taking the success exit
exists iff B accepts.  Indeed the only way to reach q_exit is a stay move out
of an original accepting configuration, so the first arrival at q_exit already
certifies acceptance; after that q_exit just sweeps right to the exit.  And an
accepting computation of B extends to one that takes the exit, including the
case where q0 is itself accepting.  Infinite computations are irrelevant here:
we only ask whether some finite augmented computation reaches the exit.

Set Qhat = Q union {q_exit} and m = s+1.  The two label sets are

    D+ = { q+ : q in Qhat } ,     D- = { q- : q in Qhat } .

For a scanned symbol c (a letter, or an endmarker with its local rules) let
E_c be the relation on Qhat of augmented STAY moves, and let T_c^+ and T_c^-
be the relations of augmented moves one cell RIGHT and one cell LEFT; in both
the second coordinate is the state AFTER the move.  At the right endmarker
T_c^+ contains only the single success-exit move (out of q_exit); at the left
endmarker T_c^- is empty (the head may not leave the tape on the left).

The cell diagram d_c is defined by

    (q+,p+) in F_{d_c}  and  (q-,p+) in R_{d_c}
        both hold  iff  (q,p) is in  E_c^* T_c^+ ,
    (q-,p-) in B_{d_c}  and  (q+,p-) in L_{d_c}
        both hold  iff  (q,p) is in  E_c^* T_c^- .

Read it as: one edge of d_c is one VISIT to the cell -- enter in state q, make
finitely many stay moves (the factor E_c^*, possibly zero), then take one move
that leaves the cell (T_c^+ to the right, T_c^- to the left), arriving at the
neighbor in state p.  The entry side decides whether we land in F or R (for a
right exit) or in B or L (for a left exit).

Now put lambda = d_{left endmarker}, rho = d_{right endmarker}, and

    tau(c_1 c_2 ... c_k) = d_{c_1} d_{c_2} ... d_{c_k} ,
    tau(epsilon) = the identity diagram of T_m .

By associativity of the product, tau is a monoid homomorphism.

Every finite augmented computation that ends at the success exit splits into
successive visits to individual cells, each visit being finitely many stays
then one move into the next cell.  Those visits form a finite path through the
product d_left d_{R_1} ... d_{R_k} d_right = lambda tau(w) rho, entering at the
far left and leaving at the far right; that is an edge (q0+, q_exit+) of
F_{lambda tau(w) rho}.  Conversely every edge of a cell diagram has a finite
transition witness (its E_c^* T_c^+ path), and stacking the witnesses cell by
cell gives an augmented computation, because the exit state of one cell is
exactly the entry state of the next.  Neither direction assumes a point of
the tape is crossed only once.

The fictitious entry on the far left with label q0+ stands for the initial
configuration; it is not an extra machine move.  No path can leave the tape on
the left, and a path can leave on the right only through the success exit.
Therefore, with a = q0+ and b = q_exit+,

    w is accepted by B    if and only if    (a,b) is in F_{lambda tau(w) rho} .

For the empty word, lambda and rho are adjacent endmarker cells and
tau(epsilon) is the identity, so lambda tau(epsilon) rho = lambda rho is
exactly that product.

Monotonicity: diagram multiplication is increasing in each factor, so if
tau(u) <= tau(v) then

    lambda tau(alpha) tau(u) tau(beta) rho
        <=  lambda tau(alpha) tau(v) tau(beta) rho .

An edge (a,b) of F of the smaller diagram is also an edge of F of the larger
one.  Hence alpha u beta accepted (the edge is present) forces alpha v beta
accepted.  QED

--------------------------------------------------------------------------------
5.  A COMPLEMENTING MACHINE FORCES AN INCLUSION-REVERSING MAP
--------------------------------------------------------------------------------

Now suppose some machine recognizes the COMPLEMENT of L_H, i.e. the words
whose relation product is EMPTY.  We will show that the diagrams of that
machine must map onto the relation monoid, reversing inclusion.  This is the
"reduction" from automata to algebra.

PROPOSITION 5.1 (order reversal).  Let H be a finite set with |H| >= 2.  If an
s-state 2NFA recognizes Sigma^* minus L_H, then some submonoid of T_{s+1}
admits a surjective, identity-preserving (unital) homomorphism phi onto R_H
with

    z <= z'    implies    phi(z') <= phi(z) .

PROOF.  Apply the representation lemma (Lemma 4.1) to the complementing
machine, and let S = tau(Sigma^*) be the image of all words in T_{s+1}.

First we relate the diagram order to the relation product.  Suppose
tau(u) <= tau(v).  Pick any p, q in H and take the one-letter words

    alpha = { (p,p) } = I_{p} ,     beta = { (q,q) } = I_{q} .

These singletons are relations, hence letters of Sigma.  In path order,

    I_{p} r(u) I_{q}  =  { (p,q) }   if (p,q) is in r(u),
                      =  empty       if (p,q) is not in r(u).

The complementing machine accepts exactly the words whose product is empty.
So "alpha u beta accepted" simply means "(p,q) is not in r(u)".  By the
monotonicity half of Lemma 4.1, tau(u) <= tau(v) gives

    (p,q) not in r(u)   implies   (p,q) not in r(v).

Taking the contrapositive,

    (p,q) in r(v)   implies   (p,q) in r(u),   that is   r(v) <= r(u).

Since p, q were arbitrary,  tau(u) <= tau(v)  implies  r(v) <= r(u).   (*)

Second, (*) shows phi is well defined.  If tau(u) = tau(v), apply (*) in both
directions to get r(u) <= r(v) and r(v) <= r(u), i.e. r(u) = r(v).  So

    phi( tau(w) ) = r(w)        (w in Sigma^*)

is a genuine map from S to R_H.  It is multiplicative because tau and r both
respect concatenation (r is by definition the product, tau by Lemma 4.1).  It
preserves the identity: the empty word maps to r(epsilon) = I_H, the identity
of R_H.  It is surjective because every relation in R_H is itself a letter of
Sigma, so every element of R_H is phi of a one-letter word.  And (*) is
exactly the reversal phi(z') <= phi(z) whenever z <= z'.  QED

We have reduced the whole automaton problem to one algebraic question.  State
it as a theorem, whose proof fills the rest of the paper.

THEOREM 5.2 (inclusion-reversing image bound).  Let m >= 1 and let H be a
finite set with h = |H| >= 2.  Let S_0 be a submonoid of T_m.  Suppose a
surjective multiplicative map

    phi_0 : S_0 --> R_H

satisfies   z <= w  implies  phi_0(w) <= phi_0(z)   for all z, w in S_0.
Then

    2m  >=  2^floor( (h-2)/127 ) .

The map is not assumed in advance to preserve identities.

WHY THIS FINISHES THE COUNTING.  Combine Proposition 5.1 with Theorem 5.2.
A complementing machine with s states yields a map from a submonoid of
T_{s+1} onto R_H, reversing inclusion, so Theorem 5.2 gives

    2(s+1)  >=  2^floor( (h-2)/127 ) .

With h = n-2 this is 2(s+1) >= 2^floor((n-4)/127), i.e.

    s  >=  (1/2) * 2^floor( (n-4)/127 )  -  1 .

That is the main theorem.  So it remains ONLY to prove Theorem 5.2.  Sections
6 through 10 build its pieces and section 11 assembles them.  The strategy is:

  - attach to each idempotent diagram e a fixed set of "recurrent classes"
    of boundary labels, at most 2m of them (section 6);
  - measure how a diagram z destroys those loops: its "missing set"
    (section 6), and prove the missing set of a product is contained in the
    union of the missing sets of the factors (section 7);
  - show that one missing-set bound survives transport through any fixed
    diagram context, at the cost of a factor 2 (section 8);
  - show that along a chain of nested idempotents, the total loss is at most
    twice the initial budget (section 9);
  - amplify a single added pair into t^2 additions sharing one budget, and
    induct on h; t = 64 gives the recurrence and the number 127 (section 10).

--------------------------------------------------------------------------------
6.  RECURRENT CLASSES, CORNERS, AND MISSING SETS
--------------------------------------------------------------------------------

For the rest of the proof fix m and write <= for the inclusion order on T_m.
Recall an element e of a monoid is IDEMPOTENT when e e = e.

6.1  Loops and recurrent points.  Let e be an idempotent diagram.  Define,
on the two label sets,

    K_e^+ = (L_e R_e)*        (a relation on D+, a "positive loop")
    K_e^- = (R_e L_e)*        (a relation on D-, a "negative loop")
    P_e^+ = K_e^+ F_e K_e^+
    P_e^- = K_e^- B_e K_e^- .

Think of K_e^+ as "go out on the left as a D- label and come back on the right
as a D+ label, any number of times"; it is a free loop that never has a net
effect.  P_e^+ is "cross forward, wrapped in free loops".  We shall mostly
work with the positive sign and drop the superscript, recovering the negative
sign by reflection.

Two identities follow directly from e e = e and the product formula:

    F_e K_e F_e = F_e        hence        P_e P_e = P_e .

First F_e K_e F_e = F_{ee} = F_e, because the middle factor of F_{ee} is
precisely (L_e R_e)* = K_e.  Then P_e P_e = K_e F_e K_e K_e F_e K_e, and
K_e K_e = K_e, so this equals K_e (F_e K_e F_e) K_e = K_e F_e K_e = P_e.
Thus P_e is transitive.

Call a label x in D^+ RECURRENT (for e) when x P_e x holds.  On recurrent
points, "x P_e y and y P_e x" is an equivalence relation: reflexive by
definition, symmetric by the condition, transitive because P_e is transitive.
Call its equivalence classes the recurrent classes of the positive sign, and
do the same on D^- via P_e^-.  Let C_e be the whole collection of recurrent
classes over both signs, keeping the two signs separate as different classes.

COUNT.  There are only m labels in D+ and m in D-, so

    |C_e|  <=  2m .

For the identity diagram e = 1, K_e^+ and K_e^- are identity relations and so
P_e^+ = F_e, P_e^- = B_e are identity relations; every one of the 2m labels
is its own singleton recurrent class.

6.2  Corners.  For an idempotent e, the CORNER e T_m e = { e a e : a in T_m }
is a monoid with identity e.  An element z lies in the corner exactly when
e z = z e = z.  For z in the corner, the product formulas applied to e z = z
and z e = z give the RETURN containment and the THROUGH identities

    L_e <= L_z ,  R_e <= R_z ,
    F_z = F_e (L_z R_e)* F_z = F_z (L_e R_z)* F_e .

(For example e z = z reads F_z = F_e (L_z R_e)* F_z, and z e = z reads
F_z = F_z (L_e R_z)* F_e; the matches for L, R are similar.)

For z in the corner define the wrapped through relations

    U_e^+(z) = K_e^+ F_z K_e^+ ,     U_e^-(z) = K_e^- B_z K_e^- .

Multiplying the identities above by K_e on the appropriate sides gives the
ABSORPTION inclusions

    F_e K_e F_z <= F_z ,   F_z K_e F_e <= F_z ,   P_e U_e(z) <= U_e(z) ,
    U_e(z) P_e <= U_e(z) .

For instance F_e K_e F_z = F_e K_e F_e (L_z R_e)* F_z = F_e (L_z R_e)* F_z =
F_z; and P_e U_e(z) = K_e (F_e K_e F_z) K_e <= K_e F_z K_e = U_e(z).

6.3  Missing sets.  Relative to an idempotent e and a corner element z, say a
recurrent class C (say C <= D^+, the negative case is identical) is MISSING
from z when, for x in C, the loop x U_e^+(z) x FAILS.  This is well defined:
if x, y lie in one recurrent class then y P_e x and x P_e y, so
y U_e(z) y contains y P_e x U_e(z) x P_e y; thus x U_e(z) x holds iff
y U_e(z) y holds.  Collect the missing classes into the MISSING SET

    M_e(z)  <=  C_e .

So M_e(z) records exactly which recurrent loops of e are destroyed by the
corner element z.  When z = e we have U_e(e) = P_e, so every loop survives
and M_e(e) is empty.

--------------------------------------------------------------------------------
7.  TWO BASIC FACTS ABOUT MISSING SETS
--------------------------------------------------------------------------------

Both facts are proved first for the positive sign and then quoted for the
negative sign by reflection.

LEMMA 7.1 (a product misses no more than its factors).  Let e be idempotent
and let z, w be in the corner e T_m e.  Then

    M_e(z w)  <=  M_e(z) union M_e(w) ,        M_e(e) is empty.

In particular M_e(z^k) <= M_e(z) for every positive integer k.

PROOF.  The returns of e survive in every corner element: L_e <= L_z, L_e <=
L_w, R_e <= R_z, R_e <= R_w.  Hence K_e = (L_e R_e)* <= (L_w R_z)*.  Using the
product formula for F_{zw},

    U_e^+(z w) = K_e F_{zw} K_e
              = K_e F_z (L_w R_z)* F_w K_e
              >= K_e F_z K_e F_w K_e
              = U_e^+(z) U_e^+(w) .

So if a label x supports both loops x U_e(z) x and x U_e(w) x, then it supports
x U_e(z w) x.  Therefore a class that is missing from neither factor is not
missing from the product, which is exactly M_e(z w) <= M_e(z) union M_e(w).
For the negative sign the same computation with B in place of F gives
U_e^-(z w) >= U_e^-(w) U_e^-(z), with the factors in the other order; the
conclusion is identical.  Finally U_e(e) = K_e F_e K_e = P_e, and every
recurrent class is defined by a loop of P_e, so M_e(e) is empty.  QED

LEMMA 7.2 (rectangles of through edges).  Let e be idempotent and let z be in
e T_m e.  For a positive recurrent class C in C_e and any p in C set

    A_C = { u : u (F_e K_e) p } ,      B_C = { v : p (K_e F_e) v } .

Then A_C x B_C does not depend on the choice of p, it is contained in F_e, and
these rectangles over all recurrent classes cover F_e.  If C is not missing
from z then its rectangle is contained in F_z.  The reflected statements hold
for negative classes and B_e.  In particular

    if M_e(z) is empty, then e <= z .

PROOF.  Containment in F_e: take u in A_C and v in B_C.  Then for the point
p in C,  u F_e K_e p  and  p K_e F_e v.  Since K_e is reflexive, p K_e p, and
K_e is transitive, the two K_e pieces chain:  u F_e K_e p K_e F_e v, that is
u F_e K_e F_e v = u F_e v, which lies in F_e because F_e K_e F_e = F_e.

Independence of p: the identities (F_e K_e) P_e = F_e K_e and
P_e (K_e F_e) = K_e F_e let us move from p to any q in C, using q P_e p and
p P_e q, without changing the set; the two factors of the rectangle are
unchanged.

Coverage: we factor an arbitrary pair (u,v) in F_e through a recurrent point.
Because P_e = K_e F_e K_e and F_e K_e F_e = F_e,

    F_e P_e  =  F_e K_e F_e K_e  =  F_e K_e ,
    P_e F_e  =  K_e F_e K_e F_e  =  K_e F_e ,

so, since K_e is reflexive, induction on j >= 0 gives

    F_e P_e^j  <=  F_e K_e           and           P_e^j F_e  <=  K_e F_e .

Also P_e is idempotent, so F_e P_e^k F_e = F_e P_e F_e = F_e K_e F_e = F_e
for every k >= 1.  Fix k > m and expand (u,v) in F_e = F_e P_e^k F_e as

    u  F_e  c_1  P_e  c_2  P_e  ...  P_e  c_k  P_e  c_{k+1}  F_e  v .

The k+1 labels c_1, ..., c_{k+1} all lie in the m-element set D+, so two of
them coincide: c_i = c_j with i < j.  Idempotence of P_e then gives
c_i P_e^{j-i} c_j = c_i P_e c_i, so p = c_i is recurrent.  The prefix ending
at p lies in F_e P_e^{i-1} <= F_e K_e, giving u F_e K_e p; the suffix starting
at p lies in P_e^{k+1-i} F_e <= K_e F_e, giving p K_e F_e v.  Thus (u,v) lies
in the rectangle of the recurrent class of p, so the rectangles cover F_e.

Now suppose C is not missing from z.  Then for p in C the loop
p K_e F_z K_e p holds.  Inserting it between the two halves of the rectangle,

    A_C x B_C  <=  F_e K_e F_z K_e F_e  <=  F_z ,

the last step by the absorption inclusions F_e K_e F_z <= F_z and
F_z K_e F_e <= F_z.  In particular, if the whole missing set is empty every
through edge of e is a through edge of z; and the return edges of e persist
because z lies in the corner.  Hence e <= z.  QED

--------------------------------------------------------------------------------
8.  TRANSPORT: A BUDGET SURVIVES ANY FIXED CONTEXT
--------------------------------------------------------------------------------

The next lemma is the heart of the bookkeeping.  It says that a bound on
missing classes can be carried through any FIXED outer context u(...)v, at the
price of one factor of 2, and with a common target set J' that works for a
whole family of replacements z at once.  The word "common" is essential: in
the amplification step we replace many different z inside the SAME context and
need them all to fit one budget.

LEMMA 8.1 (transport).  Let e, d be idempotents and let u, v be diagrams with

    u e v  =  d .

For every set J <= C_e there is a SINGLE set J' <= C_d with |J'| <= 2|J| such
that, for every z in the corner e T_m e with  M_e(z) <= J  and  u z v in d T_m d,

    M_d(u z v)  <=  J' .

PROOF.  We fix witnesses once and for all, independent of z.

Fix a positive class C of C_d with representative x.  Its recurrence reads
x K_d^+ F_d K_d^+ x.  Substituting d = u e v, the edge F_d = F_{uev} expands
into a finite path that enters u, crosses e, and exits through v (with
possible return loops at each boundary).  Every time this path crosses the
middle factor e it uses a through edge of e (a pair of F_e, or of B_e for
the negative sign).  For each such middle edge pick, using Lemma 7.2, an
e-recurrent class whose rectangle covers it.  Do the same for every negative
class, using x K_d^- B_d K_d^- x.  These choices depend only on u, e, v, d,
not on z.

Now define J'.  A class C of C_d is MARKED when any e-class chosen along its
fixed witness lies in J.  Let J' be the set of marked classes.

Claim 1: every class NOT in J' is not missing from u z v.  Suppose C is
unmarked, so every e-class chosen along its witness is outside J, hence (since
M_e(z) <= J) also outside M_e(z).  By Lemma 7.2 each chosen through edge of e
survives in the corresponding through relation of z, and the return edges of
e survive because z is in the corner (L_e <= L_z, R_e <= R_z).  The outer K_d
pieces are untouched.  So the same witness becomes a loop in
U_d(u z v) = K_d F_{uzv} K_d  (or the B version).  Hence no such class is
missing, i.e. M_d(u z v) <= J'.

Claim 2: at most |J| classes of each sign are marked.  For a d-class C let
S_C be the set of e-classes chosen along its fixed witness.  We show the
family { S_C } is pairwise disjoint among d-classes of a fixed sign.  Take two
positive witnesses, written (with the F_d edges expanded through u, e, v)

    x K_d^+ alpha  F_d  beta  K_d^+ x ,
    y K_d^+ alpha' F_d  beta' K_d^+ y          (alpha,beta,alpha',beta' in D+),

and suppose the first expansion uses a middle edge (a,b) and the second uses
(a',b'), both covered by ONE e-class.  A rectangle of a recurrent class is a
product A x B, so it also contains (a,b') and (a',b).  The sign of that e-class
fixes the travel direction of all four edges, so we may splice: the prefix of
witness 1 ending at a, then the edge (a,b') of the rectangle, then the suffix
of witness 2 starting at b'.  Neither retained subpath passes an outer exit
before its end, so this concatenation is a genuine finite path for F_d, giving
alpha F_d beta'.  Interchanging the roles gives alpha' F_d beta.

Now the exterior factors close the loops: from x K_d alpha and beta' K_d y we
get x (K_d F_d K_d) y = x P_d y, and symmetrically y P_d x.  So x and y lie in
the same d-recurrent class, i.e. C = C'.  This proves the disjointness for one
sign; reflection does the negative sign.  A witness using only returns of e
has S_C empty and is never marked.  Since J' = { C : S_C meets J } and the
S_C are disjoint, at most |J| classes of each sign are marked, i.e.
|J'| <= 2 |J|.

Claims 1 and 2 together give the lemma.  QED

--------------------------------------------------------------------------------
9.  NESTED IDEMPOTENTS: ABSORPTION AND THE CHAIN BOUND
--------------------------------------------------------------------------------

NESTING ORDER.  For idempotents write  d =< e  (read "d nested under e") when

    d e = e d = d .

This is a partial order: reflexivity is clear, and if d =< e =< f then
d f = (d e) f = d (e f) = d e = d and f d = f (e d) = (f e) d = e d = d.  So
nesting is transitive.  It is NOT the same order as edge inclusion <=; nesting
compares identities, inclusion compares edges.

Tool used below.  For relations, star expansion gives
(X union Y)* = X* (Y X*)*  and  X (Y X)* = (X Y)* X, grouping steps by their
alternating colour.  We use these freely.

9.1  ABSORPTION UNDER NESTING.

LEMMA 9.1 (absorption under nesting).  Let d, e be idempotents with d =< e.
For either sign sigma one has

    K_e^sigma <= K_d^sigma ,   P_e^sigma P_d^sigma <= P_d^sigma ,
    P_d^sigma P_e^sigma <= P_d^sigma .

In the positive sign one also has F_e P_d^+ <= P_d^+ and P_d^+ F_e <= P_d^+,
and the negative sign has the same with B_e.

PROOF (positive sign, superscript suppressed).  Because d lies in the corner
e T_m e, its returns contain those of e: L_e <= L_d and R_e <= R_d.  Set

    S = (L_d R_e)* ,      T = (L_e R_d)* .

Then K_e = (L_e R_e)* <= S <= K_d and K_e <= T <= K_d.  Multiplying the
product formulas and using e d = d e = d gives

    F_d = F_e S F_d = F_d T F_e ,
    L_d = L_e union F_e S L_d B_e ,
    R_d = R_e union B_e R_d T F_e .

Now expand R_d inside K_d = (L_d R_d)*.  Since
L_d R_d = L_d R_e union L_d B_e R_d T F_e ,

    K_d = S (L_d B_e R_d T F_e S)* ,

and using the second star identity,

    F_e K_d F_d = (F_e S L_d B_e R_d T)* F_e S F_d
                = (F_e S L_d B_e R_d T)* F_d
                <= K_d F_d .

The inequality holds because F_e S L_d B_e <= L_d, so the starred relation lies
in L_d R_d T <= K_d, and K_d is closed under the star.  Expanding L_d instead,

    K_d = T (F_e S L_d B_e R_d T)* ,
    F_d K_d F_e = F_d T F_e (S L_d B_e R_d T F_e)*
                = F_d (S L_d B_e R_d T F_e)*
                <= F_d K_d ,

because B_e R_d T F_e <= R_d.  Multiplying by the surrounding K_d and using
P_d = K_d F_d K_d, these two inclusions say exactly F_e P_d <= P_d and
P_d F_e <= P_d.

Finally K_d P_d = P_d K_d = P_d together with K_e <= K_d gives

    P_e P_d = K_e F_e K_e P_d <= K_e P_d <= K_d P_d = P_d ,
    P_d P_e = P_d K_e F_e K_e <= P_d K_e <= P_d K_d = P_d .

Reflection gives every negative-sign statement.  QED

9.2  CONTAINMENT OF RECURRENT CLASSES.

LEMMA 9.2 (containment of classes).  Let d, e be idempotents with d =< e.
Every class in C_d contains either

  (1) a whole class of C_e that is NOT in M_e(d); or

  (2) two distinct whole classes of C_e.

All classes involved have the same sign.

PROOF (positive sign, superscript suppressed).  Fix a recurrent point x of
P_d.  Write F_d two ways using Lemma 9.1's identities, F_d = F_e S F_d = F_e S F_d
T F_e.  Then P_d = K_d F_d K_d = K_d F_e S F_d T F_e K_d, and recurrence of x
reads

    x ( K_d F_e S F_d T F_e K_d ) x .

The rectangle cover (Lemma 7.2) factors each of the two displayed F_e edges
through an e-recurrent point.  Call the first p and the second q.  The witness
splits as

    x  alpha  p  beta  q  gamma  x ,    with
    alpha = K_d F_e K_e ,
    beta  = K_e F_e S F_d T F_e K_e = K_e F_d K_e = U_e^+(d) ,
    gamma = K_e F_e K_d .

Here beta = U_e(d) because F_e S F_d T F_e = F_d, and beta <= P_d because
K_e <= K_d.  By Lemma 9.1, multiplying P_d on either side by alpha or gamma
stays inside P_d.

From x P_d x and this witness we read off four facts.  Each uses the
absorption to attach the neighbouring piece to a P_d edge:

    x P_d x  alpha  p        gives   x P_d p ,
    p beta q  gamma  x P_d x gives   p P_d x ,
    x  alpha  p beta  q      gives   x P_d q ,
    q  gamma  x P_d x        gives   q P_d x .

So p and q are recurrent for P_d, and they lie in the class of x.  (In the
first and last lines the recurrence x P_d x at the ends is essential: the bare
witness fragment alone need not contain a d-through edge.)

Next, the WHOLE P_e-class of p sits inside the P_d-class of x.  If r is in it,
then x P_d p P_e r and r P_e p P_d x; the mixed absorptions P_d P_e <= P_d and
P_e P_d <= P_d give x P_d r and r P_d x.  The same holds for q.

If the P_e-classes of p and q are different, we have found two distinct whole
classes of C_e inside the class of x: alternative (2).

If instead they coincide, then p U_e(d) q by the witness, and q P_e p.  The
corner absorption U_e(d) P_e <= U_e(d) gives p U_e(d) p, so the common class is
NOT in M_e(d).  This whole class sits inside the class of x, giving
alternative (1).  Reflection handles the negative sign.  QED

9.3  THE CHAIN BOUND.

The next proposition is why we may let the corner identity change during the
amplification: along a chain of nested idempotents the successive losses add
up to no more than twice one initial budget.

PROPOSITION 9.3 (chain bound).  Let b_0, b_1, ..., b_k be idempotents with
b_j =< b_{j-1} for 1 <= j <= k.  Suppose a single set J_0 <= C_{b_0} satisfies
M_{b_0}(b_j) <= J_0 for 0 <= j <= k.  Then

    sum_{j=1}^{k} | M_{b_{j-1}}(b_j) |  <=  2 |J_0| .

PROOF.  Choose one PROTECTED label in every class of C_{b_0} that is outside
J_0, and keep these choices fixed.  A protected label x of sign sigma satisfies
x U_{b_0}^sigma(b_j) x at every stage j.  By transitivity of nesting and
Lemma 9.1, K_{b_0}^sigma <= K_{b_j}^sigma, so this loop is also a loop of
P_{b_j}^sigma.  Hence every protected label stays recurrent at every stage.

Let s_j be the number of classes of C_{b_j} that contain NO protected label.
In particular s_0 = |J_0|, because exactly the J_0-classes are unprotected at
the start.  Write delta_j = |M_{b_{j-1}}(b_j)|.

Every class missing at step j is unprotected.  Otherwise it would contain a
protected x, and x U_{b_0}(b_j) x together with K_{b_0} <= K_{b_{j-1}} would
give x U_{b_{j-1}}(b_j) x, contradicting that the class is missing.

Give weight 1/2 to each missing unprotected class of C_{b_{j-1}} and weight 1
to every other unprotected class.  The total weight is s_{j-1} - delta_j/2.
By Lemma 9.2 every unprotected class of C_{b_j} contains previous classes of
total weight at least 1: either one non-missing class (weight 1), or two
distinct classes (each at least 1/2).  Every contained previous class is
unprotected, since a protected label inside it would protect the new class too.
And distinct new classes cannot draw on the same previous class, because
classes of one sign are disjoint and the two sign sets are disjoint.  Therefore

    s_j  <=  s_{j-1} - delta_j / 2 .

Summing over j and using s_k >= 0,

    sum_{j=1}^{k} delta_j  <=  2 ( s_0 - s_k )  <=  2 s_0  =  2 |J_0| .

QED

--------------------------------------------------------------------------------
10.  AMPLIFICATION: THE COST OF ONE ADDED PAIR
--------------------------------------------------------------------------------

We now build the induction on h.  The idea, in one sentence: from a single
off-diagonal pair added to the identity relation, generate t^2 further pair
additions that share one budget, so the loss must grow.

We need two small lemmas about semigroups and relations (subsections 10.1 and
10.2) before we can state the main induction (subsection 10.3).

CONVENTIONS.  A finite semigroup A is a finite set with an associative
product.  A monoid is a semigroup with an identity.  For an idempotent d in a
semigroup A, the CORNER d A d = { d a d : a in A } is a monoid with identity
d.  A UNIT of a monoid is an element with a two-sided inverse.

10.1  MINIMAL IDEMPOTENT CORNERS.

LEMMA 10.1 (minimal idempotent corners).  Let A be a finite semigroup, M a
monoid, and theta: A --> M a surjective multiplicative map.  For every
idempotent q in M there is an idempotent d in A with theta(d) = q, minimal
among such idempotents under nesting.  For every such minimal d, restriction
of theta is a unital surjection

    d A d  -->  q M q .

Moreover every element of d A d whose image is a unit of q M q is itself a
unit of d A d; in particular every unit of q M q has a unit lift.

PROOF.  First, every element w of a finite semigroup has an idempotent
positive power.  The sequence w, w^2, w^3, ... is eventually periodic, so for
a large exponent e divisible by the eventual period, w^e satisfies w^{2e} =
w^e.  Apply this to any preimage of q to get an idempotent preimage of q.
By finiteness there is one minimal in the nesting order.

Let d be such a minimal idempotent, theta(d) = q.  For y in q M q, choose x in
A with theta(x) = y.  Then theta(d x d) = q y q = y, so restriction is
surjective onto q M q, and it is unital because theta(d) = q.

Now let w in d A d have a unit image u in q M q.  An idempotent power w^k has
image u^k, which is again a unit; being also idempotent, it equals the identity
q of q M q.  Since w in d A d, we have w^k =< d, and w^k is an idempotent lift
of q, so minimality of d gives w^k = d.  If k > 1, then w^{k-1} is a two-sided
inverse of w in d A d; if k = 1, then w = d is already the identity.  QED

10.2  A FULL RELATION MONOID INSIDE A RELATION CORNER.

LEMMA 10.2 (restriction of a relation corner).  Let P in R_H be idempotent,
let F <= H, and put i = I_F.  Suppose i P i = i, and define Q = P i P.  Then
Q is idempotent, Q =< P (nesting in R_H), and restriction

    rho : Q R_H Q --> R_F ,     rho(Z) = i Z i

is a unital monoid isomorphism.  Its inverse sends A in R_F to P A P.

PROOF.  From P P = P and i P i = i we compute

    Q Q = Q ,  P Q = Q P = Q ,  Q i = P i ,  i Q = i P ,  i Q i = i .

If Z = Q Z Q then P Z P = (P Q) Z (Q P) = Q Z Q = Z, and therefore
Z = P i P Z P i P = P i Z i P; so Z is determined by its restriction i Z i.
Conversely, for A supported on F (that is A = i A i), the relation P A P lies
in Q R_H Q (one checks P A P = Q A Q), and

    i (P A P) i = (i P i) A (i P i) = A .

So restriction is a bijection with inverse A |--> P A P.  For supported A, B,

    (P A P)(P B P) = P A P B P = P A (i P i) B P = P A B P ,

using P = P i P and i P i = i to insert i.  Hence the inverse, and therefore
restriction, preserves multiplication.  Finally rho(Q) = i Q i = i is the
identity of R_F.  QED

10.3  THE INDUCTION ON h.

Parameters.  Set t = 64, and for an integer h >= 2 put

    D(h) = 2^floor( (h-2) / (2t-1) ) = 2^floor( (h-2)/127 ) .

The value t = 64 balances two estimates proved below: t^2 pair additions each
cost at least half of the smaller-instance bound, while their total cost is at
most 16t times the original loss.  The resulting gain is t/32 = 2, bought at a
reduction of 2t - 1 = 127 points of h.  That is where 127 and the factor 2 in
2^floor((h-2)/127) come from.

PROPOSITION 10.3 (cost of one added pair).  Let m >= 1, let e in T_m be
idempotent, and let S <= e T_m e be a submonoid with identity e.  Let H be a
finite set of size h >= 2.  Suppose phi: S --> R_H is a unital surjective
homomorphism with

    z <= w   implies   phi(w) <= phi(z)     (z, w in S),

and suppose every permutation of H has a unit lift in S.  If a in S is
idempotent and, for distinct x, y in H,

    phi(a) = I_H  union  { (x,y) } ,

then

    | M_e(a) |  >=  D(h) .

PROOF.  We induct on h, simultaneously over all the data in the statement
(m, e, S, phi included), so the induction hypothesis is available for every
smaller h and every admissible (m, e, S, phi).

BASE CASE 2 <= h <= 2t = 128.  Here D(h) = 1, so it suffices to show M_e(a) is
nonempty.  If it were empty, Lemma 7.2 would give e <= a, and order reversal
would give phi(a) <= phi(e) = I_H (using that phi is unital, so phi(e) is the
identity of R_H).  But phi(a) = I_H union {(x,y)} with x != y, which is not
contained in I_H.  Contradiction.  So |M_e(a)| >= 1 = D(h).

INDUCTIVE STEP, h >= 2t+1 = 129.  Put c = |M_e(a)|.  We will build t^2 nested
steps whose missing sets total at most 16tc, and show each step alone costs at
least D(h-2t+1)/2.  Since each step is a smaller instance of the proposition,
the two bounds will force c up.

STEP 1 (one budget for all pair additions).
Choose disjoint sets

    U = { u_1, ..., u_t } ,   V = { v_1, ..., v_t } ,   { z }

inside H; this uses h >= 2t+1 points.  Conjugating a by unit lifts of
permutations gives elements s_i, s'_j of S with

    phi(s_i)  = I_H union { (u_i, z) } ,
    phi(s'_j) = I_H union { (z, v_j) } .

Why: permutation conjugation acts transitively on ordered pairs of distinct
points, and the inverse of a unit lift maps to the inverse permutation.  A
unit p in S gives the conjugate p a p^{-1}, with p e p^{-1} = e.  Applying
transport (Lemma 8.1) to a with the context p ( . ) p^{-1} and J = M_e(a)
therefore gives

    | M_e(s_i) | <= 2c ,      | M_e(s'_j) | <= 2c .

So the single set

    J = (union over i of M_e(s_i))  union  (union over j of M_e(s'_j))  <= C_e

has |J| <= 4tc, and the product inequality M_e(z w) <= M_e(z) union M_e(w)
gives  M_e(s_i s'_j) <= J  for every i, j.

Let P_0 = I_{H \ {z}}.  Choose an idempotent lift b_0 in S of P_0 (an
idempotent positive power of any lift), and set

    g_ij = b_0 s_i s'_j b_0  in  b_0 S b_0 .

The product phi(s_i s'_j) = (I_H union {(u_i,z)})(I_H union {(z,v_j)}) is
I_H together with the pairs (u_i,z), (z,v_j), (u_i,v_j).  Sandwiching by P_0
removes the two pairs incident to z, so

    phi(g_ij) = P_0 union { (u_i, v_j) } .

Since b_0 e b_0 = b_0, the common-set conclusion of transport applies with
context b_0 ( . ) b_0 (and d = b_0 e b_0 = b_0).  It gives a SINGLE set
J_0 <= C_{b_0} with

    |J_0| <= 8tc ,     M_{b_0}(g_ij) <= J_0    for all 1 <= i,j <= t .

STEP 2 (a nested chain spending that budget).
List the t^2 pairs of U x V in any order, without repetition.  Let E_l be the
set of the first l pairs, and put P_l = P_0 union E_l for 0 <= l <= t^2.  For
any E, E' subsets of U x V,

    (P_0 union E)(P_0 union E') = P_0 union E union E' .

Indeed P_0 acts as the identity on all the endpoints involved (none is z), and
no pair of E can be followed by a pair of E', because a pair of E ends in V
while the next would have to start in U, and U and V are disjoint.  Hence every
P_l is idempotent.

If the pair at position l is (u_i, v_j), let b_l be an idempotent positive
power of b_{l-1} g_ij b_{l-1}.  Inductively phi(b_l) = P_l.  The sandwich, and
so every positive power of it, is absorbed on both sides by b_{l-1}; therefore

    b_l =< b_{l-1}        (1 <= l <= t^2),

and all b_l lie in the b_0-corner.  Starting from M_{b_0}(b_0) empty, repeated
use of the product inequality (Lemma 7.1) together with M_{b_0}(g_ij) <= J_0
gives

    M_{b_0}(b_l) <= J_0        (0 <= l <= t^2).

(Taking a positive power cannot enlarge a missing set: all factors share the
same missing set and their union is unchanged.)  The chain bound
(Proposition 9.3) now gives

    sum_{l=1}^{t^2} delta_l  <=  16 t c ,     where  delta_l = |M_{b_{l-1}}(b_l)| .

STEP 3 (a smaller instance inside every step).
Fix l, let (u_i, v_j) be its newly added pair, and write b = b_{l-1},
P = P_{l-1}.  Retain the two endpoints of this pair and everything outside the
construction:

    F = { u_i, v_j }  union  ( H \ (U union V union {z}) ) ,   i_F = I_F ,
    Q = P i_F P .

Then |F| = h - 2t + 1 >= 2.  Among the possible extra pairs of P, only
(u_i, v_j) has both endpoints in F, and that pair has not yet been added, so
i_F P i_F = i_F.  By Lemma 10.2, Q is idempotent, Q =< P, and Q R_H Q is
isomorphic to R_F by restriction.  Also P P_l P = P_l (apply the union formula
twice).  Since i_F Q = i_F P and Q i_F = P i_F,

    i_F (Q P_l Q) i_F  =  i_F P_l i_F  =  I_F union { (u_i, v_j) } .

Consider the finite monoid A = b S b.  The restriction of phi maps it onto
P R_H P: sandwiching any preimage by b gives a preimage of its P-sandwich.
Apply Lemma 10.1 inside A to the idempotent Q.  This gives an idempotent d in A
with phi(d) = Q, minimal there among idempotent lifts of Q.  Its corner d A d
maps unitally onto Q(P R_H P)Q = Q R_H Q, and all units of this image lift.
Composing with the restriction isomorphism gives a unital surjective
homomorphism

    psi : d A d --> R_F ,      psi(w) = i_F phi(w) i_F .

This map is order-reversing (phi is, and restriction preserves inclusion) and
carries unit lifts of every permutation of F (via Lemma 10.2).  Also d A d is a
submonoid of d T_m d with identity d.  So every domain and map hypothesis of the
induction is met.

Because b_l =< b we have b_l in A.  By the displayed identity, the element
d b_l d in d A d maps under psi to I_F union {(u_i,v_j)}.  That relation is
idempotent, so an idempotent positive power v of d b_l d has the same image.
Since d is idempotent, d b d = d.  Apply transport (Lemma 8.1) from the
identity b to the identity d, with context (d, d) and missing set M_b(b_l):

    | M_d(d b_l d) |  <=  2 delta_l .

Then apply the power consequence in the d-corner:

    | M_d(v) |  <=  | M_d(d b_l d) |  <=  2 delta_l .

The induction hypothesis applies to d, d A d, psi, v with the smaller
parameter |F| = h-2t+1, so |M_d(v)| >= D(h-2t+1).  Hence

    2 delta_l  >=  D(h-2t+1) .

Summing this lower bound over the t^2 steps and using the total-cost bound,

    16 t c  >=  (t^2 / 2) D(h-2t+1) ,   so   c  >=  (t/32) D(h-2t+1) .

For t = 64 the coefficient is t/32 = 2, and because (h-2)/127 = (h-129)/127 + 1,

    2 D(h-127)  =  2 * 2^floor((h-129)/127)  =  2^floor((h-2)/127)  =  D(h) .

Therefore c >= D(h), which completes the induction.  QED

--------------------------------------------------------------------------------
11.  FINISHING THE ALGEBRA: PROOF OF THEOREM 5.2
--------------------------------------------------------------------------------

We now have every piece to bound an inclusion-reversing image.

PROOF OF THEOREM 5.2.  The data are: a submonoid S_0 <= T_m and a surjective
multiplicative map phi_0: S_0 --> R_H that reverses inclusion.  The identity
I_H of R_H is idempotent.  Apply Lemma 10.1 to phi_0 and the idempotent I_H.
It gives an idempotent e in S_0 with phi_0(e) = I_H, minimal among such, such
that the corner S = e S_0 e maps unitally onto R_H, and every unit of R_H has a
unit lift in S.  Since S is a submonoid of e T_m e with identity e, it fits the
hypotheses of Proposition 10.3.

A permutation of H is a bijective relation, hence a unit of R_H.  By Lemma 10.1
every permutation of H therefore has a unit lift in S.

Choose distinct x, y in H and any lift a' in S of I_H union {(x,y)}.  The
relation I_H union {(x,y)} is idempotent, because the off-diagonal pair (x,y)
cannot be composed with itself (x != y).  So an idempotent positive power a of
a' has the same image.  Proposition 10.3 applies and gives

    D(h)  <=  | M_e(a) | .

On the other hand M_e(a) is a subset of C_e, and by the count of section 6
|C_e| <= 2m.  Therefore

    2^floor((h-2)/127)  =  D(h)  <=  |M_e(a)|  <=  |C_e|  <=  2m .

Rearranging gives exactly 2m >= 2^floor((h-2)/127).  QED

--------------------------------------------------------------------------------
12.  THE MAIN THEOREM
--------------------------------------------------------------------------------

Everything is now in place.

PROOF OF THE MAIN THEOREM.  Let n >= 4, put h = n-2, let H = {1, 2, ..., h},
and let Sigma = R_H.  By Lemma 2.1 the liveness language L_H is recognized by
the n-state 2NFA A_n.

Suppose some s-state 2NFA recognizes the complement Sigma^* minus L_H.  By
Proposition 5.1 a submonoid of T_{s+1} admits a surjective, unital,
inclusion-reversing homomorphism onto R_H.  Theorem 5.2 then forces

    2(s+1)  >=  2^floor((h-2)/127)  =  2^floor((n-4)/127) ,

which rearranges to

    s  >=  (1/2) * 2^floor((n-4)/127)  -  1 .

The right-hand side grows exponentially with n and is bounded by no polynomial
(for any fixed degree d, the ratio 2^floor((n-4)/127) / n^d tends to infinity
as n grows).  Hence no single polynomial, independent of the alphabet, bounds
the number of states needed to complement an n-state 2NFA.  QED

A word of honesty about the alphabet.  The alphabet Sigma_n = R_H has
|Sigma_n| = 2^{(n-2)^2} letters and grows with n.  The theorem is about bounds
that are uniform over all finite alphabets; it does not claim a fixed-alphabet
lower bound.  The parameter being measured is the number of STATES, not the
size of the transition table.

--------------------------------------------------------------------------------
13.  THE DETERMINIZATION CONSEQUENCE
--------------------------------------------------------------------------------

The lower bound also bears on DETERMINISTIC two-way automata.

COROLLARY 13.1.  There are absolute constants c > 0 and n_0 such that, for
every n >= n_0, every 2DFA that recognizes the language of A_n has at least

    c * 2^floor((n-4)/127)

states.

PROOF.  We use one external fact (Geffert, Mereghetti, Pighizzini 2007): every
s-state 2DFA has an equivalent COMPLEMENTING automaton, again two-way and
deterministic, with at most C*s states, where C is an absolute constant
independent of the alphabet.  Crucially this holds even when some computations
fail to halt.

Suppose an s-state 2DFA M recognizes L(A_n) = L_H.  Complementing M gives a
2DFA (hence a 2NFA) with at most C*s states that recognizes Sigma^* minus L_H.
The main theorem forces any such 2NFA to have at least

    (1/2) * 2^floor((n-4)/127) - 1

states.  Therefore C*s >= (1/2) 2^floor((n-4)/127) - 1, so for all sufficiently
large n,

    s  >=  c * 2^floor((n-4)/127) ,      c = 1/(2C) > 0 .

That right-hand side is exponential, so no polynomial independent of the
alphabet can determinize all 2NFAs.  QED

Why the external fact is needed: simply exchanging the accepting and rejecting
states of a 2DFA does NOT complement it, because a computation that loops
forever is accepted by neither the machine nor its swapped version.  The cited
construction is the standard fix.

--------------------------------------------------------------------------------
14.  WHERE THE PIECES COME FROM, AND A READING LIST
--------------------------------------------------------------------------------

Only two things above are imported from outside this file:

  - The family L_H, for nonempty words, is Sakoda and Sipser's B_h.  Naming it
    is a convenience; all its properties used here are proved.
  - The linear-overhead complementation of 2DFAs (Geffert, Mereghetti,
    Pighizzini 2007) is used only in Corollary 13.1.

Everything else -- the diagram monoid, recurrent classes, missing sets,
transport, the chain bound, amplification, the representation lemma, the
reduction, and the arithmetic -- is proved from scratch here.

Reading list, with why each is relevant:

  W. J. Sakoda, M. Sipser (1978), Nondeterminism and the Size of Two Way Finite
    Automata, STOC '78.  The liveness family B_h and the state-succinctness
    question that motivates the whole problem.

  M. Y. Vardi (1989), A note on the reduction of two-way automata to one-way
    automata, Information Processing Letters 30.  An exponential-size one-way
    nondeterministic way to COMPLEMENT a 2NFA; complementation in the same
    two-way model is what we bound.

  C. Kapoutsis (2006), Small Sweeping 2NFAs Are Not Closed under Complement,
    ICALP 2006.  Exponential complementation cost for the restricted class of
    sweeping automata.

  V. Geffert, C. Mereghetti, G. Pighizzini (2007), Complementing Two-Way Finite
    Automata, Information and Computation 205.  Linear-overhead deterministic
    complementation, used in Corollary 13.1.

  B. Guillon, L. Prigioniero, J. Taheri (2026), Polynomial Complementation of
    Nondeterministic Two-Way Finite Automata by 1-Limited Automata, STACS 2026.
    A polynomial bound needs the power to rewrite each cell once on first visit;
    the read-only model here has no such power.

  P. Martin, V. Mazorchuk (2013), Partitioned binary relations, Mathematica
    Scandinavica 113.  The monoid T_m is exactly their monoid of partitioned
    binary relations, with the two signs kept as separate copies.

The exponent 127 is far from optimal.  It only has to be a positive constant.
A sharper constant would replace floor((n-4)/127) by floor((n-4)/K) for some
smaller fixed K and would not change any qualitative conclusion.