Eighty-three sublattices and planarity

TL;DR

This paper establishes a threshold for the number of sublattices in a finite lattice that guarantees its planarity, providing a sharp bound with a specific constant.

Contribution

The authors prove a new quantitative criterion linking the number of sublattices to planarity in finite lattices, with a sharp bound for all sizes.

Findings

Lattices with at least 83·2^{n-8} sublattices are planar.

The bound is sharp for n > 8, with a non-planar lattice having just below this number.

The result precisely characterizes the sublattice count threshold for planarity.

Abstract

Let $L$ be a finite $n$-element lattice. We prove that if $L$ has at least $83\cdot 2^{n-8}$ sublattices, then $L$ is planar. For $n>8$, this result is sharp since there is a non-planar lattice with exactly $83\cdot 2^{n-8}-1$ sublattices.

Equations

$$\mathbf{\sigma }(\mathcal{A}):=|\mathrm{Sub}(\mathcal{A})|\cdot 2^{8-n}.$$

$${\mathcal{L}}_{\text{KR}}:=\{A_n,E_n,E_n^{\mathbf{\delta }},F_n,G_n,H_n:n\ge 0\}\cup \{B,B^{\mathbf{\delta }},C,C^{\mathbf{\delta }},D,D^{\mathbf{\delta }}\}.$$

$$X\in \{B,C,D,E_0,E_1,F_0,G_0,H_0\},$$

$$|\mathrm{Sub}(L)|=|\mathrm{Sub}(F_0)|\cdot 2^{n-9}=(83\cdot 2^{|F_0]-8})\cdot 2^{n-9}=83\cdot 2^{n-8},$$

$$T:=\{e\vee f$$

$$j\vee k$$

$$\left.\parbox{230.46748pt}{$\varphi$ is an order-embedding, $\varphi(u)=\varphi(v)\vee\varphi(w)$ holds for every triplet $(u,v,w)\in K^{3}$ of distinct elements such that $u$ covers both $v$ and $w$, and dually.}\right\}$$

$$e\wedge f$$

$$a\wedge d$$

$$b\vee g$$

$$c\wedge e$$

$$\left.\parbox{261.76526pt}{if $x$ and $y$ are distinct atoms of $P_{8}$ and $z\in P_{8}$ such that $x\leq z$ and $y\leq z$, then $z=x\vee_{L}y$, and dually for coatoms.}\right\}$$

$$a\vee c=b,c\vee e=d,e\vee g=f,b\wedge d=c,d\wedge f=e,f\wedge h=g$$

$$d\vee f=i,c\wedge e=o,b\wedge e=o,c\wedge f=o,d\vee g=i,f\vee c=i,$$

$$\left.\parbox{256.0748pt}{if $X$ belongs to $\mathcal{L}_{\textup{KR}}$, then the second alternative (with $x$) \emph{always} yields a better (that is, smaller) estimate of $\boldsymbol{\sigma}(L)$,}\right\}$$

$$c{\vee }_{L}e=g\text{ and }g{\wedge }_{L}f=d,$$

$$\left(\begin{array}{ccccccccc}i& a& b& c& d& e& f& g& o\\ o& f& g& e& d& c& a& b& i\end{array}\right).$$

$$b\wedge c=e,e\vee g=c,c\vee d=a,d\wedge e=f,a\vee b=i,f\wedge g=o.$$

$$\ast$$

Full text

This research of was supported by the Hungarian Research, Development and Innovation Office under grant number KH 126581.

1. Our result and introduction

A finite lattice is said to be planar if it has a Hasse diagram that is also a planar representation of a graph. Our goal is to prove that finite lattices with many sublattices are planar. Namely, we are going to prove the following theorem.

Theorem 1.1**.**

Let $L$ be a finite lattice, and let $n:=|L|$ denote the number of its elements. If $L$ has at least $83\cdot 2^{n-8}$ sublattices, then it is a planar lattice.

Another variant of this result together with a comment on its sharpness will be stated in Theorem 2.2.

Notes on the dedication

As a coincidence, the number eighty-three plays a key role in Theorem 1.1, and I found this theorem recently, in the same year when professor George Grätzer, the founder of Algebra Universalis, celebrates his eighty-third birthday. For more about him, the reader is referred to my biographic paper [2] and the interview [3] with him. Furthermore, the topic of the present paper is close to his current research interest on planar lattices; this interest has been witnessed, say, by Czédli and Grätzer  [6] and [7], Czédli, Grätzer, and Lakser [8], Grätzer [11], [12], [13], [14], [15], and [16], Grätzer and Knapp [17], [18], [19], [20], and [21], Grätzer and Lakser [22], Grätzer, Lakser, and Schmidt [23], Grätzer and Quackenbush [24], Grätzer and Schmidt [25], and Grätzer and Wares [26]. These facts motivate the dedication.

Remark 1.2**.**

Although $41.5\cdot 2^{n-7}$, $20.75\cdot 2^{n-6}$, $10.375\cdot 2^{n-5}$, … and $166\cdot 2^{n-9}$, $332\cdot 2^{n-10}$, $664\cdot 2^{n-11}$, … are all equal to $83\cdot 2^{n-8}$, we want to avoid fractions as well as large coefficients of powers of 2. This explains the formulation of Theorem 1.1.

Remark 1.3**.**

For $n\geq 9$, Theorem 1.1 is sharp, since we will present an $n$-element non-planar lattice with exactly $83\cdot 2^{n-8}-1$ sublattices. For $n<9$, Theorem 1.1 can easily be made sharp as follows. Whenever $n\leq 7$, every $n$-element lattice is planar, regardless the number of its sublattices. While the eight-element boolean lattice has exactly 73 sublattices, every eight-element lattice with at least $74=74\cdot 2^{8-8}$ sublattices is planar.

Next, we mention some earlier results that motivate the present paper. As a counterpart of Theorem 1.1, finite lattices with many congruences are also planar; see Czédli [5] for details. Finite lattices with “very many” congruences or sublattices have been described by Ahmed and Horváth [1], Czédli [4], Czédli and Horváth [9], and Mureşan and Kulin [28].

Outline

The rest of the paper is devoted to the proof of Theorem 1.1. In Section 2, we recall the main result of Kelly and Rival [27]; this deep result will be the main tool used in the paper. Some easy lemmas and the proof of Remark 1.3 are also presented, and we introduce a terminology that allows us to formulate Theorem 1.1 in an equivalent and more convenient form; see Theorem 2.2. Also, this section points out some difficulties explaining why we do not see a computer-free way to prove Theorem 2.2 (equivalently, Theorem 1.1) and why a lot of human effort is needed in addition to the brutal force of computers. Section 3 gives some more details of this computer-assisted effort but the proofs of some lemmas stated there are available only from separate files or from the appendices of the paper. Also, Section 3 combines many of our lemmas and corollaries to complete the proof of Theorem 2.2 and, thus, Theorem 1.1.

2. Tools and difficulties

2.1. Relative number of subuniverses

Let $F$ be a set of binary operation symbols. By a binary partial algebra $\mathcal{A}$ of type $F$ we mean a structure $\mathcal{A}=(A;F_{A})$ such that $A$ is a nonempty set, $F_{A}=\{f_{A}:f\in F\}$, and for each $f\in F$, $f_{A}$ is a map from a subset $\textup{Dom}(f_{A})$ of $A^{2}$ to $A$. That is, $f_{A}$ is a binary partial operation on $A$. If $\textup{Dom}(f_{A})=A^{2}$ for all $f\in F$, then $\mathcal{A}$ is a binary algebra (without the adjective “partial”). In particular, every lattice is a binary algebra; note that we write $\vee$ and $\wedge$ instead of $\vee_{A}$ and $\wedge_{A}$ when the meaning is clear from the context. A subuniverse of $\mathcal{A}$ is a subset $X$ of $A$ such that $X$ is closed with respect to all partial operations, that is, whenever $x,y\in X$, $f\in F$ and $(x,y)\in\textup{Dom}(f_{A})$, then $f_{A}(x,y)\in X$. The set of subuniverses of $\mathcal{A}$ will be denoted by $\operatorname{Sub}(\mathcal{A})$. For a lattice $\mathcal{L}=(L;\{\vee,\wedge\})$, we will write $L$ rather than $\mathcal{L}$. Note that the number of sublattices of $L$ is $|\operatorname{Sub}(L)|-1$, since the set of sublattices of $L$ is $\operatorname{Sub}(L)\setminus\{\emptyset\}$. If $\mathcal{B}=(B,F_{B})$ with $B\subseteq A$ is another binary partial algebra of type $F$ such that $\textup{Dom}(F_{B})\subseteq B^{2}\cap\textup{Dom}(F_{A})$ for every $f\in F$ and $f_{B}(x,y)=f_{A}(x,y)$ for all $(x,y)\in\textup{Dom}(F_{B})$, then $\mathcal{B}$ is said to be a weak partial subalgebra of $\mathcal{A}$.

It is straightforward to drop the adjective “binary” from the concepts defined above. Even if this adjective is dropped in Lemma 2.3, to be stated soon, we will use this lemma only for the binary case. All lattices, posets, and partial algebras in this paper are automatically assumed to be finite even if this is not repeated all the time.

This paper is about lattices with many sublattices. Large lattices have a lot of subuniverses and sublattices since every singleton subset of a lattice is a sublattice. So it is reasonable to define the meaning of “many” with the help of the following notation.

Definition 2.1**.**

The relative number of subuniverses of an $n$-element finite binary partial algebra $\mathcal{A}=(A,F_{A})$ is defined to be and denoted by

[TABLE]

Furthermore, we say that a finite lattice $L$ has $\boldsymbol{\sigma}$-many sublattices or, in other words, it has $\boldsymbol{\sigma}$-many subuniverses if $\boldsymbol{\sigma}(L)>83$.

This concept and notation will play a crucial role in the rest of the paper. Since $|\operatorname{Sub}(L)|$ is larger than the number of sublattices by 1, we can reformulate Theorem 1.1 and a part of Remark 1.3 as follows.

Theorem 2.2**.**

If $L$ is a finite lattice such that $\boldsymbol{\sigma}(L)>83$, then $L$ is planar. In other words, finite lattices with $\boldsymbol{\sigma}$-many sublattices are planar. Furthermore, for every natural number $n\geq 9$, there exists an $n$-element lattice $L$ such that $\boldsymbol{\sigma}(L)=83$ and $L$ is not planar.

The importance of the concepts introduced in this section so far is well explained by the following easy lemma.

Lemma 2.3**.**

If $\mathcal{B}=(B,F_{B})$ is a weak partial subalgebra of a finite partial algebra $\mathcal{A}=(A,F_{A})$, then $\boldsymbol{\sigma}(\mathcal{A})\leq\boldsymbol{\sigma}(\mathcal{B})$.

Proof.

Let $m:=|B|$ and $n:=|A|$. Then $k:=n-m=|A\setminus B|\geq 0$. Define an equivalence relation $\sim$ on $\operatorname{Sub}(\mathcal{A})$ by letting $X\sim Y$ mean that $X\cap B=Y\cap B$. Since $X\cap B\in\operatorname{Sub}(\mathcal{B})$ for every $X\in\operatorname{Sub}(\mathcal{A})$, this equivalence has at most $|\operatorname{Sub}(\mathcal{B})|$ blocks. Every block of $\sim$ is a subset of $\{U\cup X:X\subseteq A\setminus B\}$ for some $U\in\operatorname{Sub}(\mathcal{B})$. Since $A\setminus B$ has $2^{k}$ subsets, every block of $\sim$ consists of at most $2^{k}$ elements of $\operatorname{Sub}(\mathcal{A})$. Therefore, $|\operatorname{Sub}(\mathcal{A})|\leq|\operatorname{Sub}(\mathcal{B})|\cdot 2^{k}$. Dividing this inequality by $2^{n-8}=2^{m-8}\cdot 2^{k}$, we obtain the validity of the lemma. ∎

2.2. The Kelly–Rival list

For a poset $P$, its dual will be denoted by $P^{\boldsymbol{\delta}}$. With reference to Kelly and Rival [27] or, equivalently, to Figures 1–5, the Kelly–Rival list of lattices is defined as follows.

[TABLE]

Note that $A_{n}$, $F_{n}$, $G_{n}$, and $H_{n}$ are selfdual lattices. The key tool we need is the following deep result.

Theorem 2.4** (Kelly and Rival [27]).**

A finite lattice is planar if and only if it does not contain any lattice in $\mathcal{L}_{\textup{KR}}$ as a subposet.

Lemma 2.3 and Theorem 2.4 raise the following problem; $B,C,\dots,H_{0}$ still denote lattices in $\mathcal{L}_{\textup{KR}}$. Note that being a subposet is a weaker assumption than being a sublattice.

Problem 2.5**.**

Let $X$ and $L$ be finite lattices such that $X$ is a subposet of $L$.

1. (i)

Is $\boldsymbol{\sigma}(L)\leq\boldsymbol{\sigma}(X)$ necessarily true in this case? 2. (ii)

With the additional assumption that

[TABLE]

is $\boldsymbol{\sigma}(L)\leq\boldsymbol{\sigma}(X)$ necessarily true?

If we could answer at least least part (ii) of Problem 2.5 affirmatively, then the proof of Theorem 2.2 would only require the lemmas of (the present) Section 2 and an easy application of a straightforward computer program. Later, Remark 2.20 and Example 2.21 will point out why Problem 2.5 is not as easy as it may look at first sight.

Remark 2.6**.**

There are a lot of finite lattices $X$ such that for every finite lattice $L$, $\boldsymbol{\sigma}(L)\leq\boldsymbol{\sigma}(X)$ if $X$ is a subposet of $L$. For example, $X=F_{0}$ has this property.

Proof of Remark 2.6.

Every finite chain obviously has the property above, whence there are “a lot of” such lattices. Although the proof of Lemma 3.6 will, in effect, establish the above property of $X=F_{0}$, we can present a short argument for this fact right now. (But this short argument is not independent from Lemma 3.6 and it relies on Theorem 2.2 that has not yet been proved at this stage of the paper.) For the sake of contradiction, suppose that $X=F_{0}$ is a subposet of $L$ but $\boldsymbol{\sigma}(L)>\boldsymbol{\sigma}(F_{0})$. For a computer, it is straightforward to show that $\boldsymbol{\sigma}(F_{0})=83$; see Lemma 2.8 later. So $\boldsymbol{\sigma}(L)>83$, and we obtain from Theorem 2.2 that $L$ is planar. Hence, by Theorem 2.4, $F_{0}$ cannot be a subposet of $L$, which is a contradiction. ∎

2.3. A computer program

Since it would be a very tedious task to compute $\boldsymbol{\sigma}(X)$ manually even for the smallest lattice $X\in\mathcal{L}_{\textup{KR}}$, we have developed a straightforward computer program for Windows 10 to do it. This program, called subsize, is downloadable from the authors website. The input of the program is an unformatted text file describing a finite binary partial algebra $\mathcal{A}=(A;F)$; there are several word processors that can produce such a file. In particular, the description of $\mathcal{A}$ includes a list of strings $x\ast y=z$ of length five where $\ast$ is an operation symbol in $F$, $(x,y)\in\textup{Dom}(f_{A})$ and $f_{A}(x,y)=z$; these strings are called constraints in the input file. The output, $\boldsymbol{\sigma}(\mathcal{A})$, is displayed on the screen and saved into a text file. The algorithm is trivial: the program lists all the $2^{|A|}$ subsets of $A$ and counts those that are closed with respect to all constraints.

Remark 2.7**.**

There are two kinds of difficulties we have to face. First, we could not solve Problem 2.5; see the paragraph following it. Second, the running time of our program depends exponentially on the input size $|A|$. Hence, a lot of theoretical considerations are necessary before resorting to the program and what is even worse, many cases have to be input into the program. Because of the exponential time, it is not clear (and it is not hopeful) whether the appropriate cases could be found by a much more involved (and so less reliable) computer program without a lot of human work. So the program is simple, we believe it is reliable, and it is not to hard to write another program to test our input files. On the other hand, the exceptionally tedious work to find the appropriate cases and to create the input files needed several weeks.

However, it is quite easy to obtain the following statement with the help of our computer program.

Lemma 2.8** (on small Kelly-Rival lattices).**

1. (i)

For the smallest lattices in $\mathcal{L}_{\textup{KR}}$, we have that $\boldsymbol{\sigma}(A_{0})=74$, $\boldsymbol{\sigma}(B)=54$, $\boldsymbol{\sigma}(C)=68.5$, $\boldsymbol{\sigma}(D)=76$, $\boldsymbol{\sigma}(E_{0})=60.5$, $\boldsymbol{\sigma}(F_{0})=83$, $\boldsymbol{\sigma}(G_{0})=54.25$, and $\boldsymbol{\sigma}(H_{0})=49.75$. 2. (ii)

We also have that $\boldsymbol{\sigma}(E_{1})=31.125$ and $\boldsymbol{\sigma}(F_{1})=41.125$.

Except for its equality $\boldsymbol{\sigma}(A_{0})=74$, this lemma will not be used in the proof of Theorem 2.2. However, a part of this lemma will be used in the proof of Remark 1.3 below, and it is this lemma that tells us how the theorem was conjectured. Even the proof of (part (i) of) this lemma requires more computation than a human is willing to carry out or check without a computer.

Proof of Remark 1.3.

For $n=9$, the equality $\boldsymbol{\sigma}(F_{0})=83$ from Lemma 2.8 proves the validity of Remark 1.3 since $F_{0}$ is not planar by Theorem 2.4. Assume that $n>9$, let $C$ be an $(n-9)$-element chain, and let $L$ be the ordinal sum of $F_{0}$ and $C$. That is, $L$ is the disjoint union of its ideal $F_{0}$ and its filter $C$. By Theorem 2.4, $L$ is not planar. Since a subset of $L$ is a subuniverse if and only if it is of the form $X\cup Y$ such that $X\in\operatorname{Sub}(F_{0})$ and $Y\subseteq C$, it follows that

[TABLE]

whereby $L$ has exactly $83\cdot 2^{n-8}-1$ sublattices, as required. ∎

Proof Technique 2.9**.**

For Lemma 2.8 and also for all other statements that refer to the program or mention $\boldsymbol{\sigma}(\dots)$, the corresponding input files are available from the author’s website http://www.math.u-szeged.hu/~czedli/ . The output files proving these statements are also available there and they are attached as appendices to the paper.

2.4. Lattice theoretical preparations

The proof of Theorem 2.2 will be organized as follows. Due to Theorem 2.4, it suffices to show that for each lattice $X\in\mathcal{L}_{\textup{KR}}$, whenever $L$ is a lattice with $\boldsymbol{\sigma}$-many subuniverses (that is, $\boldsymbol{\sigma}(L)>83$), then $X$ cannot be a subposet of $L$. Although we present some uniform arguments for several infinite sub-families of $\mathcal{L}_{\textup{KR}}$, separate arguments will be needed for most of the small lattices in $\mathcal{L}_{\textup{KR}}$. The following lemma is crucial.

Lemma 2.10** (Antichain Lemma).**

If $\{a_{0},a_{1},a_{2}\}$ is a three-element antichain in a finite lattice with $\boldsymbol{\sigma}$-many subuniverses, then

1. (i)

There is a $k\in\{0,1,2\}$ such that $a_{0}\vee a_{1}\vee a_{2}=\bigvee\{a_{i}:i\in\{0,1,2\}\setminus\{k\}\}$. 2. (ii)

If $\{i,j,k\}=\{0,1,2\}$ and none of $a_{i}\vee a_{j}$ and $a_{i}\vee a_{k}$ is $a_{0}\vee a_{1}\vee a_{k}$, then $a_{i}\vee a_{j}\neq a_{i}\vee a_{k}$.

Part (ii) of this lemma is trivial; we present it here to emphasize its implicit use in our considerations and in the input files of the program.

Proof.

For the sake of contradiction, suppose that (i) fails for a lattice $L$ with $\boldsymbol{\sigma}$-many subuniverses. Then $X:=\{a_{0}\vee a_{1},a_{0}\vee a_{2},a_{1}\vee a_{2}\}$ is a three-element antichain. It is well known that such an antichain generates a sublattice isomorphic to $A_{0}$, the eight-element boolean lattice; see, for example, Grätzer [10, Lemma 73]. Combining Lemmas 2.3 and 2.8, we obtain that $\boldsymbol{\sigma}(L)\leq\boldsymbol{\sigma}(A_{0})=74$, which contradicts the assumption that $\boldsymbol{\sigma}(L)>83$. ∎

Lemma 2.11**.**

If $L$ is a finite lattice with $\boldsymbol{\sigma}$-many subuniverses, then $A_{0}$ is not a subposet of $L$.

Proof.

For the sake of contradiction, suppose that $A_{0}$ is a subposet of $L$ and $\boldsymbol{\sigma}(L)>83$. Since $a,b,c$ play symmetric roles, Lemma 2.10(i) allows us to assume that $c\leq a\vee b\vee c=a\vee b$ in $L$. Then $c\leq a\vee b\leq e$ is a contradiction, as required. ∎

The following lemma needs a bit longer proof and the use of the program. This proof exemplifies many ideas that will be needed later. Note that $K_{5}$, defined by Figure 2, is a sublattice of $G_{n}$ and $H_{n}$ for $n\geq 1$, this is why it deserves our attention.

Lemma 2.12**.**

If $L$ is a finite lattice with $\boldsymbol{\sigma}$-many subuniverses, then $K_{5}$ is not a subposet of $L$.

Proof.

For the sake of contradiction, suppose that $\boldsymbol{\sigma}(L)>83$ but $K_{5}$ is a subposet of $L$. For the notation of the elements of $K_{5}$, see Figure 2.

Lattice theoretical preparatory part**.**

We modify $K_{5}$ in $L$ if necessary. The operations $\vee$ and $\wedge$ will be understood in $L$. We can assume that $e\vee f=g$, since otherwise we can replace $g$ by $e\vee f$. Of course, we have to show that this replacement results in an isomorphic subposet, but this is easy; analogous tasks will often be left to the reader. Namely, $e\vee f\leq h$ would lead to $e\leq h$, a contradiction, while $e\vee f\geq h$ combined with $g\geq e\vee f$ would lead to $g\geq h$, another contradiction. By duality, we also assume that $e\wedge f=c$. Next, we can assume $c\wedge d=b$ and, dually, $g\vee h=k$, because otherwise we can replace $b$ and $k$ by $c\wedge d$ and $g\vee h$, respectively. This is possible since, for example, $a\not\leq d$ implies that $a\not\leq c\wedge d$ while $c\wedge d\geq b$ and $a\not\geq b$ exclude that $a\geq c\wedge d$. In the next step, we assume similarly that $a\wedge b=o$ and $j\vee k=i$. Note that the equalities assumed so far and the comparability relations among the elements imply further equalities: $e\wedge d=e\wedge(f\wedge d)=(e\wedge f)\wedge d=c\wedge d=b$, $a\wedge d=a\wedge c\wedge d=a\wedge b=o$ and, dually, $e\vee h=k$ and $j\vee h=i$. The set

[TABLE]

defines a partial algebra $\mathcal{K}_{5}^{(0)}$ on the set $K_{5}$, which is a weak partial subalgebra of $L$. Note that the program calls the members of $T$ constraints.

Computational part**.**

The program proves that $\boldsymbol{\sigma}(\mathcal{K}_{5}^{(0)})=97.375$, which means that we are not ready yet. Thus, a whole hierarchy of cases have to be investigated in general. (Here, there will be only two cases.) The idea is that for incomparable elements $x$ and $y$, in notation, $x\parallel y$, such that $x\vee y$ or $x\wedge y$ is not defined in the partial algebra, the argument splits into two cases: either $x\vee y$ (or $x\wedge y$) is one of the elements already present, or it is a new element of $L$ that we add to the partial algebra. In terms of the program, we add a new constraint with or without adding a new element. Also, when we add a constraint, then we also add its consequences similarly to the previous paragraph where, say, $e\wedge d=b$. Note that if an element had three covers or three lower covers, then we would use Lemma 2.10 to split a case into three subcases, but this technique will be used later, not in the present proof. A case with name $\ast$ will be denoted by (C$\ast$).

(C1) We assume that $c\vee d=f$ and $g\wedge h=f$. Then $e\vee d=e\vee c\vee d=e\vee f=g$ and, dually, $e\wedge h=c$. Adding these four constraints to the earlier ones, we get a new partial algebra $\mathcal{K}_{5}^{(1)}$, which is a weak subalgebra of $L$. The program yields that $\boldsymbol{\sigma}(\mathcal{K}_{5}^{(1)})=79.1875$. Hence, $\boldsymbol{\sigma}(L)\leq 79.1875$ by Lemma 2.3, contradicting the initial assumption that $\boldsymbol{\sigma}(L)>83$. This excludes (C1).

Based on the argument for (C1) above, to make our style more concise, let us agree to the following terminological issue, which will usually be used implicitly in the rest of the paper.

Terminology 2.13**.**

The cases we consider describe partial algebras, which are weak partial subalgebras of $L$; the $\boldsymbol{\sigma}$-values of these partial algebras will be called the $\boldsymbol{\sigma}$-values of the corresponding cases. If the $\boldsymbol{\sigma}$-value of a case is not greater than $83$, then the case in question is excluded.

(C2) We assume that $c\vee d=:x<y:=g\wedge h$. We remove $f$ from the weak partial algebra and add $x$ and $y$. We remove the constraints of $T$ that contain $f$ but we add the new constraints $c\vee d=x$, $g\wedge h=y$, $e\vee y=g$, and $e\wedge x=c$. The last two constraints we add follow from $x\leq f\leq y$ and the previous constraints containing $f$. Note that the oval in Figure 2 reminds us that now $\{f\}$ is replaced by $\{x,y\}$. Since the $\boldsymbol{\sigma}$-value of the present situation is $80.5625$, (C2) is excluded.

After excluding both cases, that is, all possible cases, the proof of the lemma is complete. ∎

Next, for later reference, we formulate a consequence, which trivially follows from Lemma 2.12.

Corollary 2.14**.**

If $L$ is a lattice with $\boldsymbol{\sigma}$-many subuniverses and $n\geq 1$, then none of $G_{n}$ and $H_{n}$ is a subposet of $L$.

In order to formulate the following lemma about the encapsulated $2$-ladder $F_{1}^{-}$ given in Figure 4, we need the following definition. This concept will be motivated by Corollary 2.17 later.

Definition 2.15**.**

Let $L$ and $K$ be a finite lattices. A mapping $\varphi\colon K\to L$ will be called a (2.1)-embedding if

[TABLE]

Note that if $v$ and $w$ are distinct elements covered by $u$ in $K$, then $u=v\vee_{K}w$, and the dual of this observation also holds. Hence, every lattice embedding is a (2.1)-embedding but, clearly, not conversely.

Lemma 2.16** (Encapsulated 2-ladder Lemma).**

If the encapsulated 2-ladder $F_{1}^{-}$ is a subposet of a lattice $L$, then it has a (2.1)-embedding into $L$.

Proof.

We can assume that $F_{1}^{-}\subseteq L$. The notation of the elements of $F_{1}^{-}$ is given in Figure 4. We are going to modify these elements in $L$ if necessary in order to obtain a (2.1)-embedding. The operations $\vee$ and $\wedge$ will be understood in $L$. First, we let $f^{\prime}:=b\vee c$. Since $b\not\leq g$, we have that $f^{\prime}\not\leq g$. Since $f^{\prime}\leq f$ and $f\not\geq g$, we obtain that $f^{\prime}\not\geq g$. That is, $f^{\prime}$ is incomparable with $g$; in notation, $f^{\prime}\parallel g$. We obtain similarly that $f^{\prime}\parallel x$ for all $x\in F_{1}^{-}$ such that $x\parallel f$. This allows us to replace $f$ by $f^{\prime}$. To ease the notation, we will write $f$ instead of $f^{\prime}$. So, $F_{1}^{-}$ is still a subposet of $L$ but now $f=b\vee c$. Next, we replace $c$ by $c^{\prime}:=f\wedge g\geq c$; then it is straightforward to see (or it follows by duality) that we still have a poset embedding. Since $f=b\vee c\leq b\vee c^{\prime}\leq f$, we have that $f=b\vee c^{\prime}$. Thus, after writing $c$ instead of $c^{\prime}$, the notation still gives a poset embedding of $F_{1}^{-}$ into $L$ with the progress that now $b\vee c=f$ and $f\wedge g=c$. We continue in the same way step by step, always defining a new poset embedding such that the already established equalities remain true; note that the order of adjusting the elements is not at all arbitrary. In the next step, we replace $b$ by $b^{\prime}:=e\wedge f\geq b$ and $g$ by $g^{\prime}:=c\vee d\leq g$ to add $b=e\wedge f$ and $g=c\vee d$ to the list of valid equalities. We continue with setting $a=b\wedge c$ and $j=f\vee g$ similarly. Finally, redefining $i$ and $o$ as $e\vee j$ and $a\wedge d$, we complete the proof. ∎

Armed with Lemma 2.16, we can give an easy proof of the following statement.

Corollary 2.17**.**

If $L$ is a lattice with $\boldsymbol{\sigma}$-many subuniverses, then $F_{1}$ is not a subposet of $L$.

Proof.

Suppose the contrary. Then $F_{1}^{-}$, which is a sublattice of $F_{1}$, is also a subposet of $L$. By Lemma 2.16, we can assume that $F_{1}^{-}$ is a subposet of $L$ such that the inclusion map is a (2.1)-embedding. Hence, we know that

[TABLE]

The $\boldsymbol{\sigma}$-value of the situation described by (2.2)–(2.5) is $81.75$. ∎

The eight-element fence is the poset formed by the eight empty-filled elements on the right of Figure 2. If we add the dashed line to its diagram, then we obtain the diagram of the eight-crown. So the diagram of the eight-crown consists of the eight empty-filled elements $a,b,\dots,h$, seven solid edges and a dashed one. Note that the eight-crown is a subposet of $A_{1}$, see Figure 1, but the eight-element fence is not.

Lemma 2.18**.**

If $L$ is a finite lattice with $\boldsymbol{\sigma}$-many subuniverses, then neither the eight-element fence, nor the eight-crown is a subposet of $L$.

Proof.

To ease the terminology in this proof, by the eight-poset $P_{8}$ we shall mean either the eight-element fence, or the eight-crown; see Figure 2 for the notation of its elements. For the sake of contradiction, suppose that $\boldsymbol{\sigma}(L)>83$ but $P_{8}$ is a subposet of $L$.

Lattice theoretical preparatory part**.**

The set of atoms and that of coatoms of $P_{8}$ is $\{a,c,e,g\}$ and $\{b,d,f,h\}$, respectively. We claim that the subposet $P_{8}$ of $L$ can be chosen so that

[TABLE]

In particular, (2.6) implies that the equalities

[TABLE]

hold; here and later in the proof, the lattice operations are understood in $L$. In order to prove (2.6), we will modify the elements of $P_{8}$ one by one until all equalities listed in (2.6) hold. By duality, it suffices to show that for each coatom $z$ of $P_{8}$ covering two distinct atoms, $x$ and $y$ of $P_{8}$, if we replace $z$ by $z^{\prime}:=x\vee y$, then the subposet $(P_{8}\setminus\{z\})\cup\{z^{\prime}\}$ of $L$ is still isomorphic to $P_{8}$ and, in addition to the progress $x\vee y=z^{\prime}$, all the previously valid equalities from (2.6) remain true if we replace $z$ by $z^{\prime}$ in them.

If $z$ is a meetand in an equality from (2.6) that holds in $L$, then the meet is $x$ or $y$, and $x\leq z^{\prime}\leq z$ or $y\leq z^{\prime}\leq z$ shows that the equality remains true after replacing $z$ by $z^{\prime}$. As a coatom of $P_{8}$, $z$ can be neither a joinand, nor a meet in an equality from (2.6). Finally, the only stipulation of (2.6) with $z$ being a join is the equality with joinands $x$ and $y$; this fails with $z$ but becomes true after replacing $z$ by $z^{\prime}$.

Next, we show that the map $P_{8}\to(P_{8}\setminus\{z\})\cup\{z^{\prime}\}$, defined by $z\mapsto z^{\prime}$ and $u\mapsto u$ for $u\neq z$, is an order isomorphism. Let $u\in P_{8}\setminus\{z\}$. Since $z$ is a coatom of $P_{8}$, $z\not\leq u$. If we had $z^{\prime}\leq u$, then $x\leq u$, $y\leq u$, and $u\in P_{8}$ would give that $u=z$, contradicting $u\in P_{8}\setminus\{z\}$. That is, neither $u\leq z$, nor $u\leq z^{\prime}$ holds. If $u\leq z^{\prime}$, then we conclude $u\leq z$ since $z^{\prime}<z$. Conversely, if $u\leq z$, then $u\in\{x,y\}$ since $x$ and $y$ are the only elements of $P_{8}$ below $z$, whereby $u\leq z^{\prime}$. This shows that the map in question is an order isomorphism and completes the proof of (2.6). Thus, we have also proved (2.7).

Next, we define $o:=c\wedge e$ and $i:=d\vee f$ in $L$. They are distinct new elements since $\{a,c,e,g\}$ and $\{b,d,f,h\}$ are antichains. We have that

[TABLE]

since the first two of these equalities are due to definitions and the rest are easy consequences; for example, $b\wedge e=b\wedge d\wedge e=c\wedge e=o$ while the rest follow by duality or symmetry.

Computational part**.**

For the elements $a,b,\dots,h,o,i$ subject to (2.7) and (2.8), the $\boldsymbol{\sigma}$-value is $84.5$; see Terminology 2.13. In other words, we obtain with our usual technique (that is, using the program and Lemma 2.3) that $\boldsymbol{\sigma}(L)\leq 84.5$. Since this estimate is too week to derive a contradiction, we distinguish two cases.

(C1) We assume that $b\vee d=i$. Then $b\vee e=i$ also holds since $b\vee e=b\vee c\vee e=b\vee d=i$. Adding these two equalities to (2.7) and (2.8), the $\boldsymbol{\sigma}$-value is 79, which excludes this case.

(C2) We assume that $x:=b\vee d\neq i$. We also have that $b\vee e=x$ since $b\vee e=b\vee c\vee e=b\vee d$. Now we have eleven elements and, in addition to the two equalities just mentioned, (2.7), and (2.8). Since the $\boldsymbol{\sigma}$-value is $77.25$, this case is also excluded.

Both cases have been excluded, which proves Lemma 2.18.∎

The lemma we have just proved trivially implies the following statement.

Corollary 2.19**.**

If $L$ is a lattice with $\boldsymbol{\sigma}$-many subuniverses and $n\geq 1$, then none of $A_{n}$, $E_{n+1}$, and $F_{n+1}$ is a subposet of $L$.

In the rest of the paper, due to Corollaries 2.14 and 2.19 and the Duality Principle, we need to exclude only finitely many members of the infinite list $\mathcal{L}_{\textup{KR}}$ as subposets of a finite lattice $L$ with $\boldsymbol{\sigma}$-many subuniverses. After the proofs of Lemmas 2.12 and 2.18, our plan to exclude that a given member $X$ of $\mathcal{L}_{\textup{KR}}$ occurs as a subposet of a lattice $L$ with $\boldsymbol{\sigma}(L)>83$ is the following. After assuming that $X$ is a subposet of $L$, first we need some lattice theoretical preparation to ensure a feasible computational time. In the second phase, we reduce the estimate on $\boldsymbol{\sigma}(L)$ by assuming equations and introducing new elements in a systematic way until we obtain that $\boldsymbol{\sigma}(L)\leq 83$. In other words, we keep branching cases until all “leaves of our parsing tree” have $\boldsymbol{\sigma}$-values at most 83. Unfortunately, this plan requires quite a lot of work; see Table (3.2) later. In the rest of the paper, we present some of the details in order the give a better impression how our plan works. The rest of the details are given by the output files of our program and some of them in the extended version of the paper; see Proof Technique 2.9 for their coordinates.

Remark 2.20**.**

One may think of the following possibility: if $X\in\mathcal{L}_{\textup{KR}}$ is a subposet of $L$ with $\boldsymbol{\sigma}(L)>83$, $c,e\in X$, and $c\vee_{X}e=g$, then either $c\vee_{L}e=g$ in $L$, or $x:=c\vee_{L}e<g\in L\setminus X$. If we could show that

[TABLE]

then $X$ being a sublattice would give the worst estimate but even this estimate would be sufficient to imply Theorem 2.2 by Lemma 2.8. We do not know if (2.9) is true; the following example, in which $X$ happens not to be in $\mathcal{L}_{\textup{KR}}$, illustrates why (2.9) and Problem 2.5 are probably difficult.

Example 2.21** (Example to indicate difficulty).**

Let us denote by $X$ the subposet $\{c,d,e,f,g,o,i\}$ of $H_{0}$; see Figure 5. Note that $X$ is a lattice but not a sublattice of $H_{0}$. If $X$ is a subposet of a finite lattice $L$ such that

[TABLE]

then $\boldsymbol{\sigma}$ for the weak partial subalgebra of $L$ with base set $\{c,d,e,f,g,o,i\}$ and the equalities of (2.10) equals 192. So (2.10) is appropriate to show that $\boldsymbol{\sigma}(L)\leq 192$. However, if drop the first equality in (2.10) and replace it by $c\vee_{L}e=x$, where $x<g$, then the weak partial subalgebra with base set $\{c,d,e,f,g,o,i,x\}$ and equalities $c\vee e=x$ and $g\wedge f=d$ gives a worse estimate, $\boldsymbol{\sigma}(L)\leq 196$.

3. The rest of the lemmas and some proofs

In order to complete the proof of Theorem 2.2, we still need the following eight lemmas, in which $L$ denotes a finite lattice.

Lemma 3.1**.**

If $\boldsymbol{\sigma}(L)>83$, then $B$ is not a subposet of $L$.

Lemma 3.2**.**

If $\boldsymbol{\sigma}(L)>83$, then $C$ is not a subposet of $L$.

Lemma 3.3**.**

If $\boldsymbol{\sigma}(L)>83$, then $D$ is not a subposet of $L$.

Lemma 3.4**.**

If $\boldsymbol{\sigma}(L)>83$, then $E_{0}$ is not a subposet of $L$.

Lemma 3.5**.**

If $\boldsymbol{\sigma}(L)>83$, then $E_{1}$ is not a subposet of $L$.

Lemma 3.6**.**

If $\boldsymbol{\sigma}(L)>83$, then $F_{0}$ is not a subposet of $L$.

Lemma 3.7**.**

If $\boldsymbol{\sigma}(L)>83$, then $G_{0}$ is not a subposet of $L$.

Lemma 3.8**.**

If $\boldsymbol{\sigma}(L)>83$, then $H_{0}$ is not a subposet of $L$.

Proof of Lemma 3.6.

For the sake of contradiction, suppose that $\boldsymbol{\sigma}(L)>83$ but $F_{0}$ is a subposet of $L$.

Lattice theoretical preparatory part**.**

Unless otherwise stated, the lattice operations are understood in $L$; in notation, $x\vee y$ will mean $x\vee_{L}y$ and dually. Note that $F_{0}$ is a selfdual lattice and it has a unique dual automorphism

[TABLE]

Since $e\vee_{F_{0}}g=c$, we have that $e\vee g\leq c$. If $c^{\prime}:=e\vee g<c$, then we replace $c$ by $c^{\prime}$. Observe that $e\not\leq d$ and $g\not\leq b$ imply that $c^{\prime}\not\leq d$ and $c^{\prime}\not\leq b$. Since $c^{\prime}<c$ but $b\not\leq c$ and $d\not\leq c$, we also have that $b\not\leq c^{\prime}$ and $d\not\leq c^{\prime}$. So it follows that the subposet $(F_{0}\setminus\{c\})\cup\{c^{\prime}\}$ of $L$ is isomorphic to $F_{0}$. Hence, after replacing $c$ by $c^{\prime}$ if necessary, we can assume that $e\vee g=c$. In the next step, after replacing $e$ by $e^{\prime}:=b\wedge c$, we assume that $b\wedge c=e$; we still have a subposet (isomorphic to) $F_{0}$. Clearly, $e\vee g=c$ remains valid, because $c=e\vee g\leq e^{\prime}\vee g\leq c$. With $f^{\prime}:=e\wedge d\geq f$, $f^{\prime}\geq g$ would give that $e\geq g$ while $f^{\prime}\leq g$ would lead to $f\leq g$. Hence, $f^{\prime}\parallel g$. After replacing $f$ by $f^{\prime}$ if necessary, we can assume that $e\wedge d=f$. A dual argument allows us to assume that $c\vee d=a$. In the next step, we can clearly assume that $a\vee b=i$ and $f\wedge g=o$. To summarize, we have assumed that the inclusion map is a (2.1)-embedding of $F_{0}$ into $L$, that is,

[TABLE]

Computational part**.**

While splitting the possibilities into cases and subcases, we will benefit from the fact that both $F_{0}$ and (3.1) are selfdual. We keep splitting (sub)cases to more specific subcases only as long as their $\boldsymbol{\sigma}$-values are larger than 83; this tree-like splitting structure will have thirteen leaves, that is, thirteen subcases with small $\boldsymbol{\sigma}$-values that cover all possibilities. Every case below is either evaluated, that is, its $\boldsymbol{\sigma}$-value is computed by the program, or the case is split further. Of courses, we have evaluated all cases to see which of them need further splitting, but we present the $\boldsymbol{\sigma}$-values only of the non-split cases, because only the thirteen evaluated cases are needed in the proof. The (sub)cases are denoted by strings. When a case (C$\vec{\textup{x}}$) is mentioned, all the “ancestor cases”, that is, (C$\vec{\textup{y}}$) for all meaningful prefixes $\vec{y}$ of $\vec{\textup{x}}$ are automatically assumed.

(C1): $b\vee c=i$ is assumed; then $b\vee g=b\vee e\vee g=b\vee c=i$ also holds.

(C1a): $e\wedge g=o$. Since this is the dual of the previous assumption, we are in a selfdual situation. Observe that $b\wedge g=b\wedge c\wedge g=e\wedge g=o$.

(C1a.1): $d\vee e=a$, then $b\vee d=b\vee e\vee d=b\vee a=i$.

(C1a.1a): $c\wedge d=f$; then $d\wedge g=d\wedge c\wedge g=f\wedge g=o$. Again, we are in a selfdual situation.

(C1a.1a.1): $a\wedge b=e$; then $b\wedge d=b\wedge a\wedge d=e\wedge d=f$.

(C1a.1a.1a): $f\vee g=c$; then $d\vee g=d\vee f\vee g=d\vee c=a$. (Note that this case describes the situation when $F_{0}$ is a sublattice of $L$.) Since the $\sigma$-value of this case is 83, $L$ has few subuniverses, whereby (C1a.1a.1a) is excluded.

(C1a.1a.1b): $f\vee g=:x$ such that $x\neq c$. (The notation “$=:$” means that $x$ is defined as $f\vee g$ and $f\vee g=x$ is a new constraint.) Clearly, $x<c$. Using the incomparabilities among the elements of $F_{0}$, it is straightforward to see that $x$ is a new element. (In what follows in the paper, an element with a new notation will always be distinct from the rest of elements, but usually this fact will not be mentioned and its straightforward verification will be omitted.) Since $c=e\vee g\leq e\vee x\leq c$, we have that $e\vee x=c$. Since the $\boldsymbol{\sigma}$-value of this case is $74.25$, (C1a.1a.1b) is excluded. Thus, the case (C1a.1a.1) is also is excluded. Since (C1a.1a) is seldfual, the dual of (C1a.1a.1) is also excluded; this will be used in the next case.

(C1a.1a.2): $a\wedge b=:x>e$ and $f\vee g=:y<c$. Since $c\wedge b=e$ and $e\vee g=c$, it follows easily that $c\wedge x=e$ and $e\vee y=c$ Since the $\boldsymbol{\sigma}$-value is now $68$, (C1a.1a.2) is excluded. Thus, (C1a.1a) is also excluded.

(C1a.1b): $c\wedge d=:x>f$. Then $e\wedge x=f$ since $e\wedge d=f$.

(C1a.1b.1): $x\wedge g=o$. Then $d\wedge g=g\wedge c\wedge d=g\wedge x=o$.

(C1a.1b.1a) $a\wedge b=e$. Now the $\boldsymbol{\sigma}$-value is $78.25$, excluding this case.

(C1a.1b.1b): $a\wedge b=:y>e$. This case is excluded again since its $\boldsymbol{\sigma}$-value is $78.5$. Thus, (C1a.1b.1) is also excluded.

(C1a.1b.2): $x\wedge g=:y>o$. Here $y$ is a new element since $g>y>o$, and we have that $d\wedge g=d\wedge c\wedge g=x\wedge g=y$. This case is excluded, because its $\boldsymbol{\sigma}$-value is $79.375$. Thus, (C1a.1b) and so (C1a.1) are also excluded. Furthermore, since (C1a) is selfdual, we conclude that dual of (C1a.1) is also excluded; this fact will be used in the next case.

(C1a.2): $d\vee e=:v<a$ and $c\wedge d=:u>f$. Observe that $c\vee v=a$ and $e\wedge u=f$, since $c\vee d=a$ and $e\wedge d=f$. Let $x:=e\vee u$. In order to verify its novelty, observe that $e\leq x\leq c$ since $e<c$ and $u\leq c$. But $x=e$ would imply $u\leq e$, whence $u=e\wedge u=e\wedge c\wedge d=e\wedge d=f$, a contradiction. Also, $x=c$ would lead to $v=e\vee d=e\vee(u\vee d)=(e\vee u)\vee d=x\vee d=c\vee d=a$, a contradiction again. Hence, $e<x<c$, which implies easily that $x$ is a new element. We have that $d\vee x=v$ since $e\leq x\leq v$. Similarly, $b\wedge x=e$ since $e\leq x\leq c$. Now the $\boldsymbol{\sigma}$-value of the situation is $66$, whereby this case is excluded. Thus, (C1a) is also excluded.

(C1b): $e\wedge g=x>o$; then $f\wedge x=o$ since $f\wedge g=o$.

(C1b.1): $d\vee e=a$; then $b\vee d=b\vee e\vee d=b\vee a=i$.

(C1b.1a): $c\wedge d=f$; then $d\wedge g=d\wedge c\wedge g=f\wedge g=o$.

(C1b.1a.1): $a\wedge b=e$. Now $b\wedge d=b\wedge a\wedge d=e\wedge d=f$ and $\boldsymbol{\sigma}=78.25$ excludes this case.

(C1b.1a.2): $a\wedge b=:y>e$. Then $c\wedge y=e$ since $c\wedge b=e$, and $\boldsymbol{\sigma}=72$ excludes this case. Thus, (C1b.1a) is also excluded.

(C1b.1b): $c\wedge d=:u>f$; then $e\wedge u=f$ since $e\wedge d=f$, and $\boldsymbol{\sigma}=80$ excludes this case. Thus, (C1b.1) is also excluded.

(C1b.2): $d\vee e=:v<a$; then $c\vee v=a$ since $c\vee d=a$.

(C1b.2a): $c\wedge d=f$. Then $d\wedge g=d\wedge c\wedge g=f\wedge g=o$ and $\boldsymbol{\sigma}=79.375$ excludes this case.

(C1b.2b): $c\wedge d=:u>f$. Then $e\wedge u=f$ since $e\wedge d=f$, and $\boldsymbol{\sigma}=75.5$ excludes this case. Thus, (C1b.2), (C1b), and even (C1) are excluded. Furthermore, since the underlying assumption, (3.1), is selfdual, the dual of (C1) is also excluded; this fact will be used below when (C2) is analysed.

(C2) $b\vee c=:t<i$ and $e\wedge g=:s>o$. Using $a\vee b=i$ and $f\wedge g=o$, we obtain that $a\vee t=i$ and $f\wedge s=o$. Also, $b\vee g=b\vee e\vee g=b\vee c=t$ and $b\wedge g=b\wedge c\wedge g=e\wedge g=s$, and so $\boldsymbol{\sigma}=82.5$, excluding this case. All cases have been excluded, and the proof of Lemma 3.6 is complete. ∎

Note that the proof above required to compute an estimate for $\boldsymbol{\sigma}(L)$ thirteen times. Let us call these thirteen values final $\boldsymbol{\sigma}$-values. However, as mentioned previously, many more values were needed to find the proof. For example, the $\boldsymbol{\sigma}$-value of (C1a.1a.1) is $90.5$, and the inequality $90.5>83$ is the reason to split the case (C1a.1a.1) into subcases.

Remark 3.9** (Notes on the proofs of Lemmas 3.1–3.8).**

First, observe that $\boldsymbol{\sigma}(F_{0})=83$ is the largest $\boldsymbol{\sigma}$-value occurring in Lemma 2.8. Thus, Lemma 3.6 devoted to $F_{0}$ is the most crucial one in the paper. Since even the “human part” of its computer-assisted proof is long and threatens with unnoticed human errors, we have elaborated two separate proofs of Lemma 3.6. One of these proofs is optimized in some sense and it has already been given, and it is also available from the corresponding file F0-output.txt. The other proof is less optimized and it is described only by its output file called F0-alternative-output.txt.

One might think that, compared to Lemma 3.6, the seven other lemmas of this section are easier simply because while Lemma 3.6 is devoted to $F_{0}$ and $\boldsymbol{\sigma}(F_{0})=83$, the other lemmas deal with lattices $X\in\mathcal{L}_{\textup{KR}}$ with $\boldsymbol{\sigma}(X)<83$. However, some of these lemmas need even more tedious proofs than Lemma 3.6. Because such amount of straightforward technicalities would not be too exciting for the reader and because of space considerations, these proofs are not given in the concise version of this paper; some of them are appendices in the extended version of the paper, and all of them are downloadable as output files of our computer program. Assuming that the reader shares our trust in our computer program or he writes another computer program, these files constitute complete proofs. In particular, these files include lots of comments that make them almost as detailed as the proof of Lemma 3.6.

Remark 3.10** (On the lengths of the proofs of Lemmas 3.1–3.8).**

The table below gives the numbers of final $\boldsymbol{\sigma}$-values that our proofs, that is, the program output files, contain. We have already mentioned that the 3.6-labeled column gives 13. The $\ast$-labeled column refers to the second proof of Lemma 3.6 given in the downloadable file F0-alternative-output.txt.

[TABLE]

In order to explain some large numbers in the third row of the table, note the following. If $X\in\mathcal{L}_{\textup{KR}}$ contains no element with more than two covers or more than two lower covers, then the proof of the corresponding lemma is quite similar to that of Lemma 3.6; of course, we can exploit duality only if $X$ itself is selfdual. Note that symmetries with respect to automorphisms can also be exploited. However, if there are elements with more than two lower covers or dually, like in case of $H_{0}$, then there can be cases that we split into three subcases according to Lemma 2.10 as follows. Let $a_{0}$, $a_{1}$, and $a_{2}$ be the three lower covers of an element $b$ in $X\in\mathcal{L}_{\textup{KR}}$; the case of upper covers is analogous. Let $c:=a_{0}\vee a_{1}\vee a_{2}$ in $L$. (Usually, $b$ is meet-irreducible and we can let $c:=b$.) Then the following three subcases are considered. First, $a_{0}\vee a_{1}=c$. Second, $a_{0}\vee a_{1}:=x<c$ is a new element and $a_{0}\vee a_{2}=c$. Third, $a_{0}\vee a_{1}=:x<c$, $a_{0}\vee a_{2}=:y<c$, $x\neq y$ are new elements, and $a_{1}\vee a_{2}=c$. It is not surprising now that this three-direction splitting leads to more final $\boldsymbol{\sigma}$-values than the two-direction splittings in the proof of Lemma 3.6. With an opposite effect, there is another factor related to the numbers of final $\boldsymbol{\sigma}$-values. Namely, $\boldsymbol{\sigma}(X)<\boldsymbol{\sigma}(F_{0})=83$ for all $X\in\mathcal{L}_{\textup{KR}}\setminus\{F_{0}\}$ that occur in the lemmas of this section, whereby we do not have to be so efficient for these $X$ as for $F_{0}$; simply because our lemmas for these $X$ state less than an affirmative answer to Problem 2.5(ii). To conclude Remark 3.10, we mention that there are many ways to prove the eight lemmas with the help of our program, and not much effort has been devoted to reduce the numbers in the third row of Table 3.2; such an effort would have required too much work. Some of these numbers might decrease in the future.

Finally, armed with our lemmas and corollaries, we are ready to present the concluding proof of the paper.

Proof of Theorem 2.2.

For the sake of contradiction, suppose that $L$ is a finite lattice such that $\boldsymbol{\sigma}(L)>83$. By Lemmas 2.11 and 3.1–3.8 and Corollaries 2.14, 2.17, and 2.19, none of the lattices occurring as excluded subposets in these twelve statements is a subposet of $L$. Using $\boldsymbol{\sigma}(L^{\boldsymbol{\delta}})=\boldsymbol{\sigma}(L)$ and applying these twelve statements to $L^{\boldsymbol{\delta}}$, we obtain that none of the duals of the excluded lattices is a subposet of $L$. Hence, no member of $\mathcal{L}_{\textup{KR}}$ is a subposet of $L$, and Theorem 2.4 implies that $L$ is planar, as required. ∎