Luigi Santocanale

Friedrich Wehrung
email: friedrich.wehrung01@unicaen.fr

Lmno

THE EQUATIONAL THEORY OF THE WEAK BRUHAT ORDER ON FINITE SYMMETRIC GROUPS

Keywords: 2010 Mathematics Subject Classification. 06B20, 06B25, 06A07, 06B10, 06A15, 03C85, 20F55 Lattice, identity, weak order, permutohedron, Cambrian lattice, Tamari lattice, monadic second-order logic, decidability, score, bounded homomorphic image, subdirectly irreducible, splitting lattice, splitting identity, polarized measure, sub-tensor product, box product, dismantlable lattice

It is well known that the weak Bruhat order on the symmetric group on a finite number n of letters is a lattice, denoted by P(n) and often called the permutohedron on n letters, of which the Tamari lattice A(n) is a lattice retract. The equational theory of a class of lattices is the set of all lattice identities satisfied by all members of that class. We know from earlier work that the equational theory of all P(n) is properly contained in the one of all A(n). We prove the following results.

Theorem A. The equational theory of all P(n) and the one of all A(n) are both decidable.

Theorem B. There exists a lattice identity that holds in all P(n), but that fails in a certain 3,338-element lattice.

Theorem C. The equational theory of all extended permutohedra, on arbitrary (possibly infinite) posets, is trivial.

In order to prove Theorems A and B, we reduce the satisfaction of a given lattice identity in a Cambrian lattice of type A to a certain tiling problem on a finite chain. Theorem A then follows from Büchi's decidability theorem for the monadic second-order theory MSO of the successor function on the natural numbers. It can be extended to any class of Cambrian lattices of type A with MSO-definable set of orientations.

 [START_REF] Iwasawa | Einige Sätze über freie Gruppen[END_REF], using a result from Magnus [START_REF] Magnus | Über Beziehungen zwischen höheren Kommutatoren[END_REF], that every free group embeds into a product of finite symmetric groups. Consequently, a nontrivial group word cannot vanish identically on all finite symmetric groups.

Yet the set S n of all permutations on the finite set [n] = {1, 2, . . . , n} carries another fundamental algebraic structure, arising from the well known weak Bruhat ordering on S n (cf. Björner [START_REF] Björner | Orderings of Coxeter groups[END_REF]). This ordering turns out to be a lattice (see Section 3 for more detail), meaning that any two permutations x, y ∈ S n have a least upper bound x ∨ y and a greatest lower bound x ∧ y. The structure P(n) = (S n , ∨, ∧), often called the permutohedron on n letters, was first investigated in Guilbaud and Rosenstiehl [START_REF] Th | Analyse algébrique d'un scrutin[END_REF].

Lattice terms are formed like group words, starting with a set of "variables" and closing under the binary operations ∨ and ∧. A lattice identity is a formula of the form p = q, for lattice terms p and q. The equational theory of a class K of lattices is the set of all lattice identities that hold in every member of K. A lattice variety is the class of all lattices satisfying a given set of identities (cf. Grätzer [START_REF] Grätzer | Lattice Theory: Foundation[END_REF], Jipsen and Rose [START_REF] Jipsen | Varieties of Lattices[END_REF]).

In our paper [START_REF] Santocanale | Sublattices of associahedra and permutohedra[END_REF] (first posted in 2011) we stated the following problem, calling for a lattice-theoretical analogue of the above-cited Magnus-Iwasawa result.

Problem. Is the equational theory of all permutohedra decidable? Is there a nontrivial lattice identity holding in all permutohedra?

By "nontrivial" we mean not satisfied in all lattices (or, equivalently, in all free lattices). It is known since Skolem [START_REF] Skolem | Logisch-Kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit Mathematischer Sätze nebst einem Theoreme über Dichte mengen[END_REF] (reprinted in [START_REF]Selected Works in Logic[END_REF]) that the equational theory of all lattices, equivalently the word problem in free lattices, is decidable (cf. Freese, Ježek, and Nation [START_REF] Freese | Free Lattices[END_REF]Chapter I]). In our paper [START_REF] Santocanale | Sublattices of associahedra and permutohedra[END_REF] we could settle the analogue, for Tamari lattices (known since Björner and Wachs [4] to be lattice retracts of permutohedra), of the second part of the problem above, by constructing an infinite sequence of lattice identities, the Gazpacho identities, holding in all Tamari lattices. Furthermore, we proved there that the permutohedron P(4) fails at least one Gazpacho identity, thus proving that the equational theory of all Tamari lattices contains properly the one of all permutohedra. Nevertheless we could, at that time, neither achieve decidability of the equational theory of all Tamari lattices (or permutohedra), nor find a nontrivial identity holding in all permutohedra (that last part proved the trickiest of all).

In this paper we solve the Problem above, thus settling all those questions, by proving Theorems A and B stated in the Abstract. An attempt to generalize those results to "extended permutohedra" on arbitrary posets (i.e., partially ordered sets) led us to Theorem C. 1.2. Hidden identities in classes of structures. Let us present a small sample of situations where a class of algebraic structures satisfies new unexpected identities, leading to important subsequent developments in the study of those structures.

Starting with lattice structures, the most well known example is probably given by the Arguesian identity, originating in Schützenberger [START_REF] Schützenberger | Sur certains axiomes de la théorie des structures[END_REF]. A statement of that identity can be found in any textbook of lattice theory, see for example Grätzer [13, page 368]. This identity is stronger than the modular identity, and it is a latticetheoretical form of a statement of classical geometry, namely Desargues' Theorem. It gave rise to huge developments in lattice theory, establishing connections with other topics such as combinatorics, representation theory, logic. In all the situations encountered, the satisfaction of an identity was shown to be equivalent to a combinatorial, or geometrical, statement. Lattices of submodules of modules, or, more generally, lattices of commuting equivalence relations, often called linear lattices, were proved by Jónsson [START_REF] Jónsson | On the representation of lattices[END_REF] to satisfy the Arguesian identity. Jónsson proved in [START_REF]Modular lattices and Desargues' theorem[END_REF] a partial converse of that result, namely that Every complemented Arguesian lattice is linear. The case of non-complemented lattices got settled with the construction of non-linear Arguesian lattices, see Haiman [START_REF]Arguesian lattices which are not linear[END_REF][START_REF]Arguesian lattices which are not type-1[END_REF]. Haiman also proved in [START_REF] Mark | Two notes on the Arguesian identity[END_REF] that The class of all linear lattices is not finitely axiomatizable. For an overview of related results and problems, see Kung and Yan [START_REF] Joseph | Six problems of Gian-Carlo Rota in lattice theory and universal algebra[END_REF].

Moving to a completely different class of lattices, let us denote by Co(P ) the lattice of all order-convex subsets of a poset P . The sublattices of all lattices of the form Co(P ) are characterized, in Semenova and Wehrung [START_REF] Semenova | Sublattices of lattices of order-convex sets, I. The main representation theorem[END_REF], by the satisfaction of three particular identities. Furthermore, it is proved in that paper that the equational theory of all Co(P ) is decidable.

Adding a unary operation symbol for orthocomplementation, it was realized long ago that the lattice Sub H of all closed subspaces of an infinite-dimensional Hilbert space H, although failing modularity, satisfies the orthomodular identity x ∨ y = x ∨ ((x ∨ y) ∧ x ) (cf. Kalmbach [START_REF] Kalmbach | Orthomodular lattices[END_REF]). The question whether Sub H satisfies any further identity not following from orthomodularity got settled by Alan Day in 1975 with his orthoarguesian identity, see Greechie [START_REF] Greechie | A nonstandard quantum logic with a strong set of states, Current issues in quantum logic[END_REF] and Godowski and Greechie [START_REF] Law | Some equations related to states on orthomodular lattices[END_REF]. Since then many other identities have been found for Sub H, see, in particular, Megill and Pavičić [START_REF] Megill | Equations, states, and lattices of infinite-dimensional Hilbert spaces[END_REF] and their subsequent papers.

Changing the language and moving from lattices to rings, we enter the huge subject of rings with polynomial identities, of which a fundamental prototype is the Amitsur-Levitzki Theorem [START_REF] Shimshon | Minimal identities for algebras[END_REF], stating an identity holding in all matrix rings of given order over any field.

If we decree (somewhat arbitrarily) that properties like modularity stand on the bright side of the moon, then the lattices dealt with in the present paper, mainly permutohedra, would rather fit on the dark side. (A collection of results concerning identities in non-modular varieties appears in Jipsen and Rose [START_REF] Jipsen | Varieties of Lattices[END_REF]Chapter 4].) An important highlight in that direction was Caspard's result [START_REF] Caspard | The lattice of permutations is bounded[END_REF] that permutohedra are all bounded homomorphic images of free lattices, so they belong to the class B fin of Section 2.4, whose modular (or orthomodular) members are all distributive. Caspard's result got later extended to all finite Coxeter lattices (i.e., finite Coxeter groups with the weak order) in Caspard, Le Conte de Poly-Barbut, and Morvan [START_REF] Caspard | Cayley lattices of finite Coxeter groups are bounded[END_REF]; then to further lattices of regions arising from hyperplane arrangements in Reading [START_REF] Reading | Lattice and order properties of the poset of regions in a hyperplane arrangement[END_REF]; and also to "extended permutohedra" arising from posets, graphs, semilattices, and various classes of closure spaces in our works [START_REF]The extended permutohedron on a transitive binary relation[END_REF][START_REF]Lattices of regular closed subsets of closure spaces[END_REF][START_REF]Generalizations of the permutohedron: closed-open constructions[END_REF]]. Caspard's result was later refined in Santocanale [START_REF] Santocanale | On the join dependency relation in multinomial lattices[END_REF], making it possible to test on permutohedra Nation's identities β n , introduced in [START_REF] Nation | An approach to lattice varieties of finite height[END_REF], measuring the maximal length of sequences for the join-dependency relation. It was also shown in [START_REF] Santocanale | On the join dependency relation in multinomial lattices[END_REF], using combinatorial methods, that the identity β n and its dual imply together the identity SD ∧ n for semidistributivity (cf. Jipsen and Rose [25, § 4.2]). To our knowledge, the present paper is the first extensive (and complete) scrutiny of hidden identities in a combinatorially defined class of lattices on the dark side.

For a fascinating, though a bit outdated, survey on equational logic, see Taylor [START_REF] Taylor | Equational logic[END_REF].

1.3. Organization of the paper. Let us recall one by one the statements of our main theorems.

Theorem A. The equational theory of all permutohedra P(n) and the one of all Tamari lattices A(n) are both decidable.

A far more general version of Theorem A is stated in Theorem 7.8. This statement involves Reading's Cambrian lattices of type A (cf. Reading [START_REF]Cambrian lattices[END_REF]), which turn out to be the quotients of the permutohedra by their minimal meet-irreducible congruences (cf. Santocanale and Wehrung [START_REF] Santocanale | Sublattices of associahedra and permutohedra[END_REF]Corollary 6.10]) and thus they generate the same lattice variety as the permutohedra (cf. Lemma 3.1). The statement of Theorem 7.8 is sufficiently general to imply Theorem A trivially.

The first key ingredient of the proof of Theorem 7.8 originates in Reading's result [START_REF]Cambrian lattices[END_REF]Theorem 3.5], implying that the dual of a Cambrian lattice is Cambrian, and stated for Cambrian lattices of type A in Santocanale and Wehrung [START_REF] Santocanale | Sublattices of associahedra and permutohedra[END_REF]Corollary 6.11]. In Section 4 we describe that duality via an "orthogonality relation" ⊥ U between intervals of the original chain. In Section 5 (culminating in Lemma 5.5) we relate the evaluation of lattice polynomials in Cambrian lattices to new combinatorial objects that we call half-scores, which encode certain tilings of finite chains. By combining that result with the duality from Section 4, we are thus able to relate, in Lemma 6.3, the failure of a lattice identity in a Cambrian lattice to new combinatorial objects called scores. Finally, in Section 7, we translate the previously obtained statements about scores to monadic second-order logic of one successor MSO. By using a famous decidability theorem due to Büchi (cf. Theorem 7.1), we are able to reach the desired conclusion, namely Theorem 7.8.

However, the algorithm given by Büchi's Theorem, although theoretically sound, is at least one exponential away from any even remote hope for implementation, even for uncomplicated lattices such as the B(m, n) (cf. Section 2.5). In particular, this algorithm is of no help for deciding even simple lattice identities. We show, in Appendix A, a combinatorial statement, involving objects called (m, n)-scores, describing the membership problem of the lattice B(m, n) to the variety generated by a Cambrian lattice A U (E) (where E is a finite chain and U ⊆ E). This description involves certain tiling properties of the chain E.

Somehow paradoxically, it turns out that Theorem B requires far more ingenuity than Theorem A.

Theorem B. There exists a lattice identity that holds in all P(n), but that fails in a certain 3,338-element lattice.

The 3,338-element lattice L involved in Theorem B is constructed via a variant of Fraser's semilattice tensor product from [START_REF] Fraser | The tensor product of semilattices[END_REF] called complete tensor product in Wille [START_REF] Wille | Tensorial decomposition of concept lattices[END_REF], box product in Grätzer and Wehrung [START_REF] Grätzer | A new lattice construction: the box product[END_REF]. (The two concepts, although not equivalent in general, are equivalent for finite lattices.) The lattice L, represented in Figure B.1, is given as the box product of the lattices N 5 (cf. Figure 2.1) and B(3, 2) (cf. Section 2.5). Box products, and, more generally, sub-tensor products of lattices, are presented in Section 8.

The identity in question in Theorem B is the so-called splitting identity θ L of L, which turns out to be the weakest identity failing for L (cf. Section 2.4). The identity θ L can be constructed explicitly (cf. McKenzie [39, § 6], Freese, Ježek, and Nation [START_REF] Freese | Free Lattices[END_REF]Corollary 2.76]). In the present case, such a task would probably take up the space of a whole book. Fortunately, we do not need to undergo such an ordeal, and we resort instead to an "identity-free" description of lattice varieties in Section 9. The main objects of study in that section are called EA-duets; they consist of a join-homomorphism and a meet-homomorphism subject to a few simple conditions. The proof of the expanded version of Theorem B, namely Theorem 10.1, relies mostly on the description of the box product L = N 5 B(3, 2) as a sub-tensor product (cf. Definition 8.2). The only specificity of the box product, compared to other sub-tensor products, that we use in the proof of Theorem 10.1, is that it enables us to state that L is a splitting lattice (cf. Section 2.4). It is plausible that the method used in Section 10 could be extended to arbitrary sub-tensor products of N 5 and B(3, 2), however we would then lose the simplification brought by EAduets, which would bring considerable unwieldiness to the argument.

Then the question of the extension of Theorem B to more general "permutohedra" arises naturally. There are many such constructions. We shall focus on the one from our paper [START_REF]The extended permutohedron on a transitive binary relation[END_REF], which yields the "extended permutohedron" R(E) on a poset E (cf. Section 11), which turns out to be the Dedekind-MacNeille completion of a "generalized permutohedron" introduced in Pouzet et al. [START_REF] Pouzet | A generalized permutahedron[END_REF].

Theorem C. The equational theory of all extended permutohedra, on arbitrary (possibly infinite) posets, is trivial.

In fact we prove, in Theorem 11.6, a much stronger result, namely: Every finite meet-semidistributive lattice embeds into R(E), for some countable poset E. Furthermore, the poset E can be taken a directed union of finite dismantlable lattices. Theorem C is then a simple consequence of that result (cf. Corollary 11.8).

Notation and terminology

We shall mainly follow the notation and terminology from standard references on lattice theory such as Grätzer [START_REF] Grätzer | Lattice Theory: Foundation[END_REF], Freese, Ježek, and Nation [START_REF] Freese | Free Lattices[END_REF], Jipsen and Rose [START_REF] Jipsen | Varieties of Lattices[END_REF].

2.1. Basic concepts. We shall denote by [n] the set {1, 2, . . . , n}, endowed with its standard ordering. The dual poset P op of a poset P has the same universe as P , and opposite ordering (i.e., x ≤ op y if y ≤ x). We say that P is bounded if it has both a least and a largest element, then denoted by 0 P and 1 P , respectively, or 0 and 1 if P is understood. For a ≤ b in P and X ⊆ P , we set

P ↓ X = {p ∈ P | p ≤ x for some x ∈ X} and P ↓ a = P ↓ {a} , P ↑ X = {p ∈ P | p ≥ x for some x ∈ X} and P ↑ a = P ↑ {a} , [a, b] = {p ∈ P | a ≤ p ≤ b} , ]a, b] = {p ∈ P | a < p ≤ b} , [a, b[ = {p ∈ P | a ≤ p < b} , ]a, b[ = {p ∈ P | a < p < b} . An element a is a lower cover of an element b if a < b and ]a, b[ = ∅. A map f : P → Q between posets is isotone (resp., antitone) if x ≤ y implies f (x) ≤ f (y) (resp., f (y) ≤ f (x)
), for all x, y ∈ P . We denote by Con L the lattice of all congruences of a lattice L, and by Con c L the (∨, 0)-semilattice of all compact (i.e., finitely generated) congruences of L. Whenever a, b ∈ L, we denote by con(a, b), or con L (a, b) if L needs to be specified, the least congruence θ of L such that (a, b) ∈ θ.

A lattice L is subdirectly irreducible if it has a least nonzero congruence, which is then called the monolith of L.

An element p in a lattice L is • completely join-irreducible if p = X implies that p ∈ X, for all X ⊆ L;

• join-irreducible if p = X implies that p ∈ X, for all finite X ⊆ L;

• completely join-prime if p ≤ X implies that p ∈ L ↓ X, for all X ⊆ L;

• join-prime if p ≤ X implies that p ∈ L ↓ X, for all finite X ⊆ L. If p is completely join-irreducible, then it has a unique lower cover, that will be denoted by p * . In finite lattices, join-irreducibility and join-primeness are equivalent to their complete versions. Meet-irreducibility and meet-primeness are the duals of join-irreducibility and join-primeness, respectively. We denote by Ji L (resp., Mi L) the set of all join-irreducible (resp., meet-irreducible) elements of L.

We shall often write lattice identities as lattice inclusions p ≤ q (which is indeed equivalent to the identity p ∨ q = q), for lattice terms p and q. We denote by Var(K) the variety generated by a class K of lattices, and we write Var(K) instead of Var({K}).

Semidistributivity

. A lattice L is meet-semidistributive if the implication x ∧ z = y ∧ z ⇒ x ∧ z = (x ∨ y) ∧ z
holds for all x, y, z ∈ L. Join-semidistributivity is defined dually. A lattice is semidistributive if it is both join-semidistributive and meet-semidistributive.

For a completely join-irreducible element p in a lattice L, we denote by κ(p), or κ L (p) if L needs to be specified, the largest u ∈ L, if it exists, such that p * ≤ u and p u. We shall occasionally use the following easy fact (cf. Freese, Ježek, and Nation [START_REF] Freese | Free Lattices[END_REF]Lemma 2.57]):

x ≤ κ L (p) iff p p * ∨ x , for all p, x in a lattice L such that p is completely join-irreducible and κ L (p) exists. (2.1) If p is completely join-prime, then κ(p) is defined, and it is also the largest u ∈ L such that p u.

A finite lattice L is meet-semidistributive iff κ(p) exists for every p ∈ Ji L (cf. Freese, Ježek, and Nation [START_REF] Freese | Free Lattices[END_REF]Theorem 2.56]). If, in addition, L is semidistributive, then the assignment p → κ L (p) defines a bijection from Ji L onto Mi L (cf. Freese, Ježek, and Nation [START_REF] Freese | Free Lattices[END_REF]Corollary 2.55]).

2.3. Join-dependency and congruences. For more detail about Section 2.3, see Freese, Ježek, and Nation [START_REF] Freese | Free Lattices[END_REF]. The join-dependency relation, among join-irreducible elements in a finite lattice L, denoted by D (or D L if L needs to be specified), is defined by p D q if p = q and (∃x)(p ≤ q ∨ x and p q * ∨ x) , for all p, q ∈ Ji L .

Denote by L the reflexive, transitive closure of the join-dependency relation D L and set con L (p) = con L (p * , p), for all p ∈ Ji L. The following is contained in Freese, Ježek, and Nation [START_REF] Freese | Free Lattices[END_REF]Lemma 2.36]: p L q iff con L (p) ⊆ con L (q) , for all p, q ∈ Ji L .

(2.2) 2.4. Bounded homomorphic images of free lattices. For more detail about Section 2.4, see Freese, Ježek, and Nation [START_REF] Freese | Free Lattices[END_REF]. A surjective homomorphism h : K L between lattices is lower bounded (resp., bounded ) if h -1 {y} has a least element (resp., both a least and a largest element), for all y ∈ L. Denote by LB fin the class of all finite lower bounded homomorphic images of free lattices, and by B fin the class of all finite bounded homomorphic images of free lattices 1 . A lattice L belongs to B fin iff L and L op both belong to LB fin . It follows from [START_REF] Freese | Free Lattices[END_REF]Corollary 2.39] that a finite lattice L belongs to LB fin iff its join-dependency relation D L has no cycle. Every member of B fin is semidistributive. Among the lattices M 3 and N 5 represented in Figure 2.1, the first one does not belong to LB fin while the second one belongs to B fin . The labeling of N 5 introduced in Figure 2.1 will be used in Section 10. To the great puzzlement of many people, bounded homomorphic images of free lattices are often called bounded lattices. In the present paper, we revert to the original usage, by just defining bounded lattices as those with both a least and a largest element.

A lattice K is splitting if there is a largest lattice variety

C K such that K / ∈ C K . Necessarily, C K = {L | K /
∈ Var(L)} and C K is defined by a single identity θ K , called the splitting identity of K (depending not only on K, but on a given generating subset of K). Since a lattice L fails θ K iff K ∈ Var(L), it follows from Jónsson's Lemma that K has the smallest size among all lattices not satisfying θ K . The splitting lattices are exactly the finite subdirectly irreducible members of B fin , see McKenzie [39, § 5] or Freese, Ježek, and Nation [START_REF] Freese | Free Lattices[END_REF]§ II.6]. The lattice N 5 is splitting, with monolith con(p). An algorithm to compute the splitting identity of a finite splitting lattice is given in [11, § II.6].

2.5. The lattices B(m, n). Following the notation introduced in Santocanale and Wehrung [START_REF] Santocanale | Sublattices of associahedra and permutohedra[END_REF], for all positive integers m and n, we denote by B(m, n) the lattice obtained, from the Boolean lattice with m + n atoms a 1 , . . . , a m , b 1 , . . . , b n , by adding a new element q above a = m i=1 a i , such that q < a∨b j whenever 1 ≤ j ≤ n. In particular, q is join-irreducible with lower cover q * = a. The lattice B(m, n) is splitting, with monolith con(q). We set a = {a 1 , . . . , a m } and b = {b 1 , . . . , b n }.

The join-prime elements, in the lattices N 5 and B(3, 2), are exactly the atoms, that is, p * , c for N 5 and a 1 , a 2 , a 3 , b 1 , b 2 for B(3, 2). The join-irreducible elements in those lattices, represented in Figure 2.2, are the atoms together with p (for N 5 ) and q (for B(3, 2)). We will later need the following easily verified equations, valid in the lattice B(3, 2), whenever {i, j} = {1, 2} and k, l ∈ {1, 2, 3}:

b j = (q * ∨ b j ) ∧ (b 1 ∨ b 2 ) ;
(2.3)

a k = (a k ∨ b i ) ∧ (q * ∨ b j ) ; (2.4) a k ∨ a l = (a k ∨ a l ∨ b i ) ∧ (q * ∨ b j ) ;
(2.5)

Permutohedra and Cambrian lattices of type A

We shall set δ E = {(p, q) ∈ E × E | p < q}, for any poset E. That is, δ E is the strict ordering associated to E. As in our papers [START_REF] Santocanale | Sublattices of associahedra and permutohedra[END_REF][START_REF]The extended permutohedron on a transitive binary relation[END_REF], we denote by cl(a) the transitive closure of any subset a of δ E , and we set int(a) = δ E \ cl(δ E \ a). Set

P(E) = {a ⊆ δ E | a = cl(a) = int(a)} , the permutohedron on E , R(E) = {a ⊆ δ E | a = cl int(a)} ,
the extended permutohedron on E , both endowed with set containment. Although P(E) may not be a lattice for an arbitrary poset E, it is always a lattice if E is a so-called square-free poset (cf. Pouzet et al. [START_REF] Pouzet | A generalized permutahedron[END_REF], Santocanale and Wehrung [START_REF]The extended permutohedron on a transitive binary relation[END_REF]). By definition, E is square-free if it does not contain any copy of the four-element Boolean poset. For example, every chain is square-free.

On the other hand, R(E) is always a lattice, which turns out to be the Dedekind-MacNeille completion of P(E). The join, in R(E), of a family (a i | i ∈ I), is always the transitive closure of the union of the a i (cf. [START_REF]The extended permutohedron on a transitive binary relation[END_REF]).

For a positive integer n, the lattice R([n]) = P([n]), simply denoted by P(n), was first considered in Guilbaud and Rosenstiehl [START_REF] Th | Analyse algébrique d'un scrutin[END_REF]; it turns out to be isomorphic to the symmetric group on n letters endowed with its weak Bruhat ordering, see for example Bennett and Birkhoff [2,[START_REF] Bruns | Free ortholattices[END_REF]. We refer to Björner [START_REF] Björner | Orderings of Coxeter groups[END_REF] for the definition of the weak Bruhat ordering in Coxeter groups of any type.

For an arbitrary poset E, we prove in Santocanale and Wehrung [START_REF]The extended permutohedron on a transitive binary relation[END_REF] that the completely join-irreducible elements of R(E) all belong to P(E), and they are exactly the sets of the form

a, b U = (x, y) ∈ ({a} ∪ U c ) × ({b} ∪ U ) | a ≤ x < y ≤ b , (3.1)
where (a, b) ∈ δ E , U ⊆ E, and where we set U c = E\U . For notational convenience, we shall also set a, a

U = ∅. Notice that a, b U = a, b V iff U ∩ ]a, b[ = V ∩ ]a, b[. Any subset U of E defines the set D U (E) of all a ⊆ δ E such that both conditions
x < y < z and (x, z) ∈ a and y ∈ U ⇒ (x, y) ∈ a

x < y < z and (x, z) ∈ a and y / ∈ U ⇒ (y, z) ∈ a are satisfied for all x, y, z ∈ E. The set A U (E) of all transitive members of D U (E) is contained in P(E). We shall also write A(E) = A E (E). We prove in [START_REF]The extended permutohedron on a transitive binary relation[END_REF] that A U (E) is a sublattice of P(E) = R(E) whenever E is square-free (this turns out to characterise the square-freeness of E). Furthermore, the meet in A U (E) is always the set-theoretical intersection. Whenever (a, b) ∈ δ E , the set a, b U defined in (3.1) is the least element x of A U (E), with respect to containment, such that (a, b) ∈ x.

It is completely join-irreducible in R(E), with lower cover

( a, b U ) * = a, b U \ {(a, b)} , (3.2)
and both a, b U and ( a, b U ) * also belong to A U (E). In case n is a positive integer and E = [n], we shall write

A U (n) instead of A U ([n]).
As discussed in Santocanale and Wehrung [48, § 6], it turns out that the lattices A U (n) are exactly the Cambrian lattices of type A, with index n, introduced in Reading [START_REF]Cambrian lattices[END_REF]. As established in Proposition 6.7 and Corollary 6.10 of [START_REF] Santocanale | Sublattices of associahedra and permutohedra[END_REF], the A U (n) are exactly the quotients of P(n) by its minimal meet-irreducible congruences, and P(n) is a subdirect product of all the A U (n) for U ⊆ [n]. In particular, we record the following lemma.

Lemma 3.1. The class of all permutohedra P(n), for n a positive integer, and the class of all Cambrian lattices of type A, generate the same lattice variety.

Dualities between Cambrian lattices of type A

Throughout this section we fix a finite chain E and a subset U of E. As usual, we set U c = E \ U . We proved in Santocanale and Wehrung [START_REF] Santocanale | Sublattices of associahedra and permutohedra[END_REF]Corollary 6.11] that the lattices A U (E) and A U c (E) are dually isomorphic. In the present section we shall give a more precise version of that result.

For each join-irreducible

p ∈ A U (E), we set κ U (p) = κ A U (E) (p), the largest u ∈ A U (E), necessarily meet-irreducible, such that p * ⊆ u and p ⊆ u. For (a, b), (c, d) ∈ δ E , let (a, b) ∼ U (c, d) hold if a, b U ∩ c, d U c = ∅, and let (a, b) ⊥ U (c, d) hold if (a, b) ∼ U (c, d) does not hold, that is, a, b U ∩ c, d U c = ∅. Say that a closed interval [u, v] is nontrivial if u < v. Lemma 4.1. (a, b) ∼ U (c, d) iff [a, b] ∩ [c, d] is a nontrivial interval [u, v] and (u, v) ∈ a, b U ∩ c, d U c . Furthermore, if (a, b) ∼ U (c, d), then a, b U ∩ c, d U c is exactly the singleton {(u, v)}. Proof. If [a, b] ∩ [c, d] = [u, v] with (u, v) ∈ a, b U ∩ c, d U c , then, by the definition of ∼ U , we get (a, b) ∼ U (c, d). Conversely, suppose that (a, b) ∼ U (c, d) and let (x, y) ∈ a, b U ∩ c, d U c . Setting u = max{a, c} and v = min{b, d}, it follows that u ≤ x < y ≤ v while x ∈ ({a} ∪ U c ) ∩ ({c} ∪ U ) = ({a} ∩ {c}) ∪ ({a} ∩ U ) ∪ ({c} ∩ U c ) , y ∈ ({b} ∪ U ) ∩ ({d} ∪ U c ) = ({b} ∩ {d}) ∪ ({b} ∩ U c ) ∪ ({d} ∩ U ) .
We obtain nine cases to consider, for example x = a = c and y

= b ∈ U c with b < d; in each of those cases, (x, y) = (u, v). Lemma 4.2. (x, y) ∈ κ U a, b U iff (x, y) ⊥ U (a, b), for all (x, y), (a, b) ∈ δ E . Proof. We prove the contrapositive statement. Suppose first that (x, y) / ∈ κ U a, b U , that is, a, b U ⊆ ( a, b U ) * ∨ x, y U , in other words (a, b) ∈ ( a, b U ) * ∨ x, y U . There exists a subdivision a = c 0 < c 1 < • • • < c n = b such that each (c k , c k+1 ) belongs to ( a, b U ) * ∪ x, y U . We may assume that n is least possible. Since (a, b) / ∈ ( a, b U ) * , we deduce that (c k , c k+1 ) ∈ x, y U for some k ∈ [0, n -1]. By the minimality of n, either c k = a, or k > 0 and (c k-1 , c k ) ∈ ( a, b U ) * . In the latter case, c k ∈ U . In any case, c k ∈ U ∪ {a}. Symmetrically, c k+1 ∈ U c ∪ {b}, whence (c k , c k+1 ) ∈ a, b U c . Therefore, (c k , c k+1 ) belongs to x, y U ∩ a, b U c , so (x, y) ∼ U (a, b). Suppose, conversely, that (x, y) ∼ U (a, b) and let (u, v) ∈ x, y U ∩ a, b U c . Since (u, v) ∈ a, b U c , both (a, u) and (v, b) belong to the union of ( a, b U ) * with the diagonal. Since (u, v) ∈ x, y U , it follows that a, b U ⊆ ( a, b U ) * ∨ x, y U , thus (x, y) / ∈ κ U a, b U . Set ϕ(x) = {(i, j) ∈ δ E | x ∩ i, j U c = ∅}, for every x ∈ A U (E). Notice that ϕ(x) = {(i, j) ∈ δ E | (u, v) ⊥ U (i, j) for all (u, v) ∈ x}. It is trivial that ϕ(x) belongs to D U c (E). Furthermore, x c is transitive, and (i, j) ∈ ϕ(x) iff i, j U c ⊆ x c , hence, if (i, j) and (j, k) both belong to ϕ(x), then i, k U c ⊆ i, j U c ∨ j, k U c ⊆ x c , that is, (i, k) ∈ ϕ(x), and so ϕ(x) is transitive. Therefore, ϕ(x) ∈ A U c (E), and ϕ(x) is the largest y ∈ A U c (E) such that x ∩ y = ∅.
Symmetrically, for every

y ∈ A U c (E), ψ(y) = {(i, j) ∈ δ E | i, j U ∩ y = ∅} is the largest x ∈ A U (E) such that x ∩ y = ∅.
Proposition 4.3. The maps ϕ and ψ are mutually inverse dual isomorphisms between A U (E) and A U c (E).

Proof. The maps ϕ and ψ are both antitone, thus, by symmetry, it suffices to prove that ψ

• ϕ = id A U (E) . It is obvious that (ψ • ϕ)(c) contains c, for every c ∈ A U (E), so it suffices to prove that (ψ • ϕ)(c) is contained in c. Furthermore, it suffices to establish this fact in case c is meet-irreducible, that is, c = κ U ( a, b U ) for some (a, b) ∈ δ E . Let (x, y) ∈ (ψ • ϕ)(c)
; it is easily argued that this condition is equivalent to

∀(i, j) ∈ x, y U c ∩ i, j U c = ∅ . (4.1) Suppose that (x, y) / ∈ c = κ U ( a, b U ). By Lemma 4.2, (x, y) ∼ U (a, b), that is, there exists (i, j) ∈ x, y U ∩ a, b U c . By (4.1), there exists (u, v) ∈ c ∩ i, j U c . Since (i, j) ∈ a, b U c , we get (u, v) ∈ a, b U c . Thus, both (a, u) and (v, b) belong to the union of ( a, b U ) * with the diagonal, and thus, since (u, v) ∈ c, it follows that (a, b) belongs to ( a, b U ) * ∨ c = ( a, b U ) * ∨ κ U ( a, b U ) = κ U ( a, b U ), a contradiction. Notation 4.4. Denote 2 by ψ U : A U c (E) → A U (E) op the map denoted by ψ in the text above. It follows from the definition of ϕ that ϕ = ψ U c . Hence, by Proposition 4.3, ψ U is a dual isomorphism from A U c (E) onto A U (E), with inverse ψ U c . Whenever y ∈ A U c (E), ψ U (y) is the largest x ∈ A U (E) such that x ∩ y = ∅.
As an immediate consequence of Lemma 4.2, we obtain that

ψ U a, b U c = κ U a, b U , for all (a, b) ∈ δ E . (4.2)

Half-scores and alternating words

Throughout this section we shall fix a finite set Ω = {z 1 , . . . , z } (the "variables") of cardinality a positive integer , and we shall denote by T L (Ω) the set of lattice terms whose variables belong to Ω. Elements of T L (Ω) are generated from variables in Ω by applying the binary symbols ∧ and ∨. The rank of a term is defined in standard way, in such a way that subterms of a given term have (strictly) smaller ranks than the rank of the term.

Let p ∈ T L (Ω); the set Cov(p) of canonical join-covers of p is inductively defined as follows:

• If p = z i ∈ Ω, then we set Cov(z i ) = {{z i }}. • If p = p 0 ∨ p 1 , then we set Cov(p) = {{p 0 , p 1 }}. • If p = p 0 ∧ p 1 , then we set Cov(p) = Cov(p 0 ) ∪ Cov(p 1
). A number of induction proofs will be based on the simple observation that, for every p ∈ T L (Ω) \ Ω, Cov(p) is a nonempty finite set of nonempty finite subsets of T L (Ω) whose elements have all smaller rank than p. This observation will be used implicitly, throughout the text.

We consider, in the following lemma, terms formed using joins and meets indexed by nonempty subsets. This is achieved as usual, by considering the identity as the unary meet and unary join and, otherwise, by coding indexed joins (resp. meets) by an arbitrary parenthesizing of the binary join (resp. meet) operator. The lemma is proved by a straightforward induction argument.

2 Strictly speaking, we should write something like ψ E,U instead of just ψ U ; however, E will always be clear from the context. Lemma 5.1. The identity p = C∈Cov(p) C holds in every lattice, for every p ∈ T L (Ω). In particular, p ≤ C is a valid lattice inclusion, whenever C ∈ Cov(p). Definition 5.2. An alternating word on a term p in T L (Ω) is a finite sequence α = (C 0 , p 1 , C 1 , . . . , p n , C n ), where n is a nonnegative integer and the following conditions hold:

(i) C 0 is the one-element set {p}.

(ii) p j / ∈ Ω and C j ∈ Cov(p j ) whenever 1 ≤ j ≤ n. (iii) p j+1 ∈ C j whenever 0 ≤ j < n.
We denote by Alt(p) the set of all alternating words on p, and we set

C α = C n . For α, β ∈ Alt(p), let α β hold if α is a proper prefix of β.
Observe that the definition above implies that if n > 0, then p 1 = p. Furthermore, Alt(p) is finite. Definition 5.3. A subdivision of an interval [x, y], for integers x < y, is a subset of [x, y] containing the pair {x, y}. We set

cvs(P ) = {(u, v) ∈ P ×P | u < v and ]u, v[∩P = ∅} , for every set P of integers.
We shall denote by α β the concatenation of words α and β. Definition 5.4. Let E be a finite chain and let p ∈ T L (Ω). Denote by ⊥ any object outside T L (Ω) (thought of as the "undefined" symbol). A half p-score on E is a family P = ((P α , τ α ) | α ∈ Alt(p)) satisfying the following conditions:

(i) P α ⊆ E and τ α : cvs(P α ) → C α ∪ {⊥} (the valuation of index α), for every α ∈ Alt(p). (ii) P ({p}) = {0 E , 1 E } and τ ({p}) (0 E , 1 E ) = p (note that this implies that E has at least two elements). (iii) For all α ∈ Alt(p), all (x, y) ∈ cvs(P α ), all q = τ α (x, y) /

∈ Ω ∪ {⊥}, and all C ∈ Cov(q), the pair {x, y} is contained in P α (q,C) and τ α (q,C) (u, v) ∈ C for every (u, v) ∈ cvs(P α (q,C) ∩ [x, y]).

For a half p-score P as above, we shall set

P α [q] = {(x, y) ∈ cvs(P α ) | τ α (x, y) = q} , whenever α ∈ Alt(p) and q ∈ C α .
(5.1) The main lemma of this section, relating half p-scores and evaluations of lattice terms in Cambrian lattices A U (E), is the following. Lemma 5.5. Let p be a lattice term on Ω, let E be a finite chain, let U ⊆ E, and let a 1 , . . . , a ∈ A U (E). The following are equivalent:

(i) (0 E , 1 E ) ∈ p(a 1 , . . . , a )
, where p(a 1 , . . . , a ) is evaluated within A U (E).

(ii) There exists a half p-score P on E such that

P α [z i ] ⊆ a i , whenever α ∈ Alt(p) and i ∈ [ ] .
From now on we shall use the abbreviation a = (a 1 , . . . , a ).

Proof. (i)⇒(ii). We construct the finite subsets P α of E and the valuations τ α : cvs(P α ) → C α ∪ {⊥}, with P ({p}) = {0 E , 1 E } and τ ({p}) (0 E , 1 E ) = p, subject to the following induction hypothesis (relatively to the strict ordering of Alt(p)):

P α [q] ⊆ q( a) , for every q ∈ C α .

(5.

2)

The statement (5.2) holds at α = ({p}) by Assumption (i). Suppose that P α and τ α are constructed in such a way that (5.2) holds at α. The finite sequence β = α (q, C) belongs to Alt(p), whenever q ∈ C α \ Ω and C ∈ Cov(q). Let (x, y) ∈ P α [q]. By our induction hypothesis, (x, y) belongs to q( a), thus (by Lemma 5.1) to r∈C r( a), and therefore there exists a subdivision P x,y β of [x, y] such that cvs(P x,y β ) ⊆ r∈C r( a) .

(5.3)

Set

P β = (P x,y β | (x, y) ∈ P α [q]
) .

(5.4)

Observe that P β ∩ [x, y] = P x,y β , for every (x, y) ∈ cvs(P α ). Now let (u, v) ∈ cvs(P β ). If (u, v) ∈ cvs(P x,y β ) for some (necessarily unique) (x, y) ∈ P α [q], it follows from (5.3) that there exists r ∈ C such that (u, v) ∈ r( a); define τ β (u, v) as any such r. In all other cases, that is, when there is no (x, y) ∈ P α [q] such that (u, v) ∈ cvs(P x,y β ), we set τ β (u, v) = ⊥. By construction, the induction hypothesis (5.2) still holds at β. The family of all pairs (P α , τ α ) is therefore a half p-score on E and, moreover, it satisfies (5.2), for all α ∈ Alt(p). By applying (5.2) to the case where q = z i , we get the condition (ii).

(ii)⇒(i). We prove again the statement (5.2), this time by downward -induction on α ∈ Alt(p). Let α ∈ Alt(p) and suppose that (5.2) holds at every β ∈ Alt(p) with α β. Let q ∈ C α and let (x, y) ∈ P α [q], we must prove that (x, y) ∈ q( a). If q ∈ Ω, then this follows from Assumption (ii). Suppose from now on that q / ∈ Ω. Let C ∈ Cov(q). The finite sequence β = α (q, C) belongs to Alt(p). Since P is a half pscore, {x, y} is contained in P β and τ β (u, v) ∈ C whenever (u, v) ∈ cvs(P β ∩ [x, y]). Setting r = τ β (u, v), it follows from our induction hypothesis that (u, v) ∈ r( a). This holds for all (u, v) ∈ cvs(P β ∩ [x, y]), whence (x, y) ∈ r∈C r( a). This holds for every C ∈ Cov(q), thus, since the meet in A U (E) is the intersection, we get (x, y) ∈ C∈Cov(q) r∈C r( a) . By Lemma 5.1, this means that (x, y) ∈ q( a), thus completing the proof of the induction step of (5.2). By applying (5.2) to α = ({p}), we get the desired conclusion.

Scores and lattice inclusions

In this section we fix a set Ω = {z i | i ∈ [ ]} of cardinality a positive integer . We leave to the reader the straightforward proof of the following lemma. Lemma 6.1. Let F be an interval in a chain E. Then A U ∩F (F ) is a lattice retract of A U (E), with retraction defined by

π : A U (E) → A U ∩F (F ) , x → x ∩ δ F .
In the context of Lemma 6.1, we shall call π the projection map from A U (E) onto A U ∩F (F ).

From now on we shall denote by q op the dual of a term q ∈ T L (Ω), that is, q with meets and joins interchanged. Definition 6.2. Let p, q ∈ T L (Ω), let E be a finite chain, and let U ⊆ E. A (p, q, U )-score on E is a pair ( P , Q), where

P = ((P α , µ α ) | α ∈ Alt(p)) is a half p-score on E , Q = ((Q β , ν β ) | β ∈ Alt(q op )) is a half q op -score on E ,
and the following condition holds:

Whenever i ∈ [ ] , α ∈ Alt(p) , β ∈ Alt(q op ) , (x, y) ∈ P α [z i ] , (u, v) ∈ Q β [z i ] ,
the condition (x, y) ⊥ U (u, v) holds. (6.1)

We refer to Section 4 for the definition of the binary relation ⊥ U and the iso-

morphism ψ = ψ U : A U c (E) → A U (E) op . The notation P α [q] is defined in (5.1).
The following crucial lemma states the equivalence between a negated lattice inclusion p q, in A U (E), and the existence of a (p, q, U )-score on E.

Recall, in the statement and proof of the following Lemma, that ψ U : A U c (E) → A U (E) op is the canonical isomorphism defined in Section 4. Lemma 6.3. Let p, q ∈ T L (Ω), let E be a finite chain, and let U be a subset of E.

The following are equivalent:

(i) There are a 1 , . . . , a ∈ A U (E) such that p( a) ⊆ q( a).

(ii) There are a 1 , . . . ,

a ∈ A U (E) such that (0 E , 1 E ) ∈ p( a) ∩ ψ -1 U (q( a)). (iii) There exists a (p, q, U )-score on E. Proof. (iii)⇒(ii). We set a i = ( x, y U | α ∈ Alt(p) and (x, y) ∈ P α [z i ]), when- ever i ∈ [ ]. It follows from Lemma 5.5[(ii)⇒(i)] that (0 E , 1 E ) ∈ p( a).
We must prove that (0

E , 1 E ) ∈ q op (ψ -1 U a). By Lemma 5.5[(ii)⇒(i)], it suffices to prove that Q β [z i ] ⊆ ψ -1 U (a i ) whenever i ∈ [ ] and β ∈ Alt(q op ). Let (u, v) ∈ Q β [z i ]. We must prove that a i ⊆ ψ U ( u, v U c ), that is, (x, y) ⊥ U (u, v) whenever α ∈ Alt(p)
and (x, y) ∈ P α [z i ]. However, this follows from the definition of a score.

(ii)⇒(i). Suppose that p( a) ⊆ q( a) and set b = q( a). Then 0

E , 1 E U ⊆ b and 0 E , 1 E U c ⊆ ψ -1 U (b). The second containment can be written b ⊆ ψ U ( 0 E , 1 E U c ). It follows that 0 E , 1 E U ⊆ ψ U ( 0 E , 1 E U c ), that is, 0 E , 1 E U ⊆ κ U ( 0 E , 1 E U ) (use (4.2)), a contradiction. (i)⇒(iii). Pick a minimal interval F of E such that (0 F , 1 F ) ∈ p( a)
\ q( a) and, using the projection homomorphism π : A U (E)

A U ∩F (F ) (cf. Lemma 6.1), set

a i = π(a i ) for each i ∈ [ ]. Set V = U ∩ F and V c = F \ V . Observe that (0 F , 1 F ) ∈ p( a ) \ q( a ) (within A V (F )); thus F has at least two elements. Suppose that 0 F , 1 F V c ⊆ ψ -1 V (q( a )). Then q( a ) ⊆ ψ V ( 0 F , 1 F V c ). By (4.2), it follows that q( a ) ⊆ κ V ( 0 F , 1 F V ). Hence, by (2.1), 0 F , 1 F V ⊆ ( 0 F , 1 F V ) * ∨ q( a ) . (6.2) Since 0 F , 1 F V ⊆ p( a ), every (x, y) ∈ ( 0 F , 1 F V ) * belongs to p( a ); moreover, since (x, y) = (0 F , 1 F
) for every such (x, y), we obtain, by projecting onto [x, y] as in the paragraph above and by the minimality assumption on [0 F , 1 F ], the relation (x, y) ∈ q( a ); hence we get ( 0 F , 1 F V ) * ⊆ q( a ). Therefore, by (6.2), we obtain that 0 F ,

1 F V ⊆ q( a ), hence (0 F , 1 F ) ∈ q( a ), a contradiction; thus proving that 0 F , 1 F V c ⊆ ψ -1 V (q( a )). Since (0 F , 1 F ) ∈ p( a ), it follows from Lemma 5.5[(i)⇒(ii)] that there exists a half p-score P = ((P α , µ α ) | α ∈ Alt(p))
on F such that

P α [z i ] ⊆ a i , whenever α ∈ Alt(p) and i ∈ [ ] . (6.3)
Similarly, since (0

F , 1 F ) ∈ ψ -1 V (q( a )) = q op (ψ -1 V a
), there exists a half q op -score

Q = ((Q β , ν β ) | β ∈ Alt(q op )) on F such that Q β [z i ] ⊆ ψ -1 V (a i ) , whenever β ∈ Alt(q op ) and i ∈ [ ] . (6.4) Let i ∈ [ ], α ∈ Alt(p), β ∈ Alt(q op ), (x, y) ∈ P α [z i ], and (u, v) ∈ Q β [z i ]
. By (6.3) and ( 6.4), it follows that (x, y) ∈ a i and (u,

v) ∈ ψ -1 V (a i ), that is, x, y V ⊆ a i and u, v V c ⊆ ψ -1 V (a i ). By the definition of the map ψ V (cf. Section 4), it follows that x, y V ∩ u, v V c = ∅, that is, (x, y) ⊥ V (0 F , 1 F ). Therefore, ( P , Q) is a (p, q, V )-score on F .
It remains to extend the (p, q, V )-score ( P , Q) on F to a (p, q, U )-score on E. To this end let ξ : F → E be the map extending the identity on

F \ {0 F , 1 F } such that ξ(0 F ) = 0 E and ξ(1 F ) = 1 E .
Observe that ξ is an order-embedding. The proof of the following claim is a straightforward application of Lemma 4.1.

Claim. Let (x, y), (u, v) ∈ δ F . Then (x, y) ⊥ V (u, v) iff (ξ(x), ξ(y)) ⊥ U (ξ(u), ξ(v)).
Now we set P α = ξ(P α ) and µ α (ξ(x), ξ(y)) = µ α (x, y), for all α ∈ Alt(p) and all (x, y) ∈ cvs(P α ). Likewise, we set Q β = ξ(Q β ) and ν β (ξ(x), ξ(y)) = ν β (x, y), for all β ∈ Alt(q op ) and all (x, y) ∈ cvs(Q β ). It is straightforward to verify that the families

P = ((P α , µ α ) | α ∈ Alt(p)) , Q = ((Q β , ν β ) | β ∈ Alt(q op ))
are a half p-score and a half q op -score on E, respectively. Furthermore, by the Claim above, ( P , Q ) satisfies (6.1), so it is a (p, q, U )-score on E.

Expressing scores within monadic second-order logic: proving

Theorem A

We consider the monadic second-order language MSO of one successor (cf. Büchi [START_REF] Büchi | On a decision method in restricted second order arithmetic[END_REF]). We denote by u, v, w, x, y, . . . the variables of the first-order language (s) consisting of one unary function symbol s. In addition to that language, MSO has a binary relation symbol ∈, second-order variables U , V , W , X, Y , . . . , and new atomic formulas t ∈ X, where t is a term of the first-order language (s) and X is a second-order variable. The formulas of MSO are obtained by closing the atomic formulas under propositional connectives and quantification both on first-and secondorder variables. The standard model of MSO is (ω, s), where s is the successor function on the set ω of all nonnegative integers. The satisfaction by (ω, s) of a formula of MSO is defined inductively on the complexity of the formula, in a standard fashion. The following fundamental result is due to Büchi [START_REF] Büchi | On a decision method in restricted second order arithmetic[END_REF].

Theorem 7.1 (Büchi's Theorem). The theory S1S consisting of all statements of MSO valid in (ω, s) is decidable (i.e., recursive). By Büchi's Theorem, in order to decide the validity of a statement θ (in any mathematical field), it suffices to find a statement θ of MSO which is equivalent to θ (i.e., θ holds iff the structure (ω, s) satisfies θ), and then apply Büchi's decision procedure to θ. A standard fact, that we shall use repeatedly, is that the binary relations x < y and x ≤ y on ω are both MSO-definable, respectively by the statements

(∃X) (∀z)(z ∈ X ⇒ s(z) ∈ X) ∧ y ∈ X ∧ ¬(x ∈ X) , x < y ∨ x = y .
Let Ω = {z i | i ∈ [ ]} be a set of cardinality a positive integer , and let p ∈ T L (Ω). In order to be able to code half p-scores (cf. Definition 5.4) in MSO, a necessary preliminary step is to describe such objets by finite collections of subsets of ω.

For the P α nothing needs to be done (they are already sets of integers).

For a subset P of ω, the set cvs(P ) of all covers in P (cf. Definition 5.

3) is in one-to-one correspondence with the set P * defined as P , if P has no largest element, and as P \ {max P }, otherwise. Hence, for a finite set C, a map τ : cvs(P ) → C can be described by the collection of all subsets P c = {x ∈ P * | (∃y)(τ (x, y) = c)}, where c ∈ C. Accordingly, we set the following definition.

Definition 7.2. The code of a half p-score P as above is the family

(P α , P α,q | α ∈ Alt(p) , q ∈ C α ∪ {⊥}) ,
where we set P α,q = x ∈ P α | (∃y) (x, y) ∈ cvs(P α ) and τ α (x, y) = q .

Since the code of a half p-score is a finite family of sets of integers (viz. the P α and the P α,q ), its entries can be used as parameters for MSO formulas.

Lemma 7.3. The statement, saying that a given family

P = (P α , P α,q | α ∈ Alt(p) and q ∈ C α ∪ {⊥})
is the code of a half p-score on an interval [u, v] of ω, is equivalent to an MSO statement.

Proof. Axiom (i) of Definition 5.4, with 0 E replaced by u and 1 E by v, can be expressed by the conjunction of u < v and the following statements:

P α ⊆ [u, v] ,
for α ∈ Alt(p) , (7.1)

P * α = q∈Cα∪{⊥} P α,q , for α ∈ Alt(p) , (7.2)
P α,q ∩ P α,r = ∅ , for α ∈ Alt(p) and distinct q, r ∈ C α . (7.
3)

The statement (7.1) is equivalent to the MSO formula

α∈Alt(p) (∀x) x ∈ P α ⇒ (u ≤ x ∧ x ≤ v) .
Now the statement "(x, y) ∈ cvs(P α )" is equivalent to the following MSO formula:

x ∈ P α ∧ y ∈ P α ∧ x < y ∧ (∀z)¬(x < z ∧ z < y ∧ z ∈ P α ) ;
(The symbols ∧ and ¬ stand for conjunction and negation, respectively. The quotes in what follows will mean that we are replacing the statement (x, y) ∈ cvs(P ) by its MSO equivalent found previously, so we are reminded that the work is already done for that statement.) This yields immediately that (7.2) is equivalent to the conjunction of the two following MSO statements:

α∈Alt(p) , q∈Cα∪{⊥}
x ∈ P α,q ⇒ (∃y)"(x, y) ∈ cvs(P α )" ,

α∈Alt(p) (∀x)(∀y) "(x, y) ∈ cvs(P α )" ⇒ q∈Cα∪{⊥} x ∈ P α,q
(following the usual convention, and stand for conjunction and disjunction over a given index set, respectively). The translation of (7.3) to an MSO statement is even more straightforward.

Axiom (ii) of Definition 5.4 can be expressed by the statement

u ∈ P ({p}),p ∧ (∀x) x ∈ P ({p}) ⇔ (x = u ∨ x = v) .
Finally, Axiom (iii) of Definition 5.4 is equivalent to the conjunction, over all (α, q, C) with α ∈ Alt(p), q ∈ C α \ Ω, and C ∈ Cov(q), of the statements (∀x)(∀y) "(x, y) ∈ cvs(P α )" ∧ x ∈ P α,q ⇒

x ∈ P α (q,C) ∧ y ∈ P α (q,C) ∧ ϑ α,q,C (x, y) ,

where ϑ α,q,C (x, y) is the statement

(∀u)(∀v) "(u, v) ∈ cvs(P α (q,C) )" ∧ x ≤ u ∧ v ≤ y ⇒ r∈C u ∈ P α (q,C),r .
This concludes the proof. Now we formulate the following analogue of Definition 7.2 for scores.

Definition 7.4. Let p, q ∈ T L (Ω). Consider families Ṗ = (P α , P α,r | α ∈ Alt(p) and q ∈ C α ∪ {⊥}) ,

Q = (Q β , Q β,s | β ∈ Alt(q op ) and s ∈ C β ∪ {⊥}) . (7.4)
The pair ( Ṗ , Q) is the code for a (p, q, U )-score if Ṗ is the code of a half p-score P , Q is the code of a half q op -score Q, and ( P , Q) is a (p, q, U )-score.

The analogue of Lemma 7.3 for scores is the following.

Lemma 7.5. The statement, saying that a pair ( Ṗ , Q) is the code of a (p, q, U )score on an interval [u, v] of ω, is equivalent to an MSO statement.

Proof. Let Ṗ and Q be given by (7.4) and (7.5). By Lemma 7.3, the statements that Ṗ and Q are codes of a half p-score and a half q op -score on [u, v], respectively, are equivalent to MSO formulas. Next, the relations (x, y) ∈ x , y U and (x, y) ∈ x , y U c are, respectively, equivalent to the following MSO formulas:

x ≤ x ∧ x < y ∧ y ≤ y ∧ (x = x ∨ ¬(x ∈ U )) ∧ (y = y ∨ y ∈ U ) , x ≤ x ∧ x < y ∧ y ≤ y ∧ (x = x ∨ x ∈ U ) ∧ (y = y ∨ ¬(y ∈ U )) .
From this we can thus deduce the following MSO equivalent of (x 0 , y 0 ) ⊥ U (x 1 , y 1 ):

¬(∃x, y) x < y ∧ "(x, y) ∈ x 0 , y 0 U " ∧ "(x, y) ∈ x 1 , y 1 U c " .
Therefore, an MSO equivalent of the statement (6.1) is the conjunction, over all i ∈ [ ], α ∈ Alt(p), and β ∈ Alt(q op ), of the following formulas:

(∀x 0 )(∀y 0 )(∀x 1 )(∀y 1 ) "(x 0 , y 0 ) ∈ cvs(P α )" ∧ "(x 1 , y 1 ) ∈ cvs(Q β )"

∧ x 0 ∈ P α,zi ∧ x 1 ∈ Q β,zi ⇒ "(x 0 , y 0 ) ⊥ U (x 1 , y 1 )" .
Lemma 7.6. Let p, q ∈ T L (Ω). The statement, depending on two first-order variables x and y and a second-order predicate U , saying that A U ([x, y]) satisfies the lattice inclusion p ≤ q, is equivalent to an MSO statement.

Proof. By Lemma 6.3, A U ([x, y]) does not satisfy the lattice inclusion p ≤ q iff there is a (p, q, U )-score on [x, y]. Now the existence of a score can be expressed via existential quantification, over all second-order predicates P α , P α,r , Q β , Q β,s , of the MSO formula, obtained from Lemma 7.5, that expresses being a (p, q, U )-score. Therefore, the following formula is equivalent to A U ([x, y]) not satisfying p ≤ q:

(∃ Ṗ )(∃ Q) "( Ṗ , Q) is the code of a (p, q, U )-score on [x, y]" ,
where, in an obvious sense, ∃ Ṗ stands for a string of quantifiers of the form ∃P α or ∃P α,r , for α ∈ Alt(p) and r ∈ C α ∪ {⊥} (and similarly for ∃ Q). We can now state an expanded form of Theorem A.

Theorem 7.8. Let U be an MSO-definable set of orientations. Then the equational theory of all lattices A U ([x, y]), where (x, y, U ) ∈ U, is decidable.

Proof. For all (x, y, U ) ∈ U, the Cambrian lattice A U ([x, y]) satisfies the lattice inclusion p ≤ q iff the following MSO formula θ p,q (obtained from the proof of Lemma 7.6) is in S1S:

(∀x)(∀y)(∀U ) "(x, y, U ) ∈ U" ⇒ "A U ([x, y]) satisfies the inclusion p ≤ q" .
Further, the assignment (p, q) → θ p,q is given by an effectively computable procedure, that is, it is recursive. The desired conclusion follows from Theorem 7.1.

Defining U as the set of all (x, y, U ) with x < y and U ⊆ [x, y], we obtain the equational theory of all Cambrian lattices of type A, which, by Lemma 3.1, is the same as the equational theory of all permutohedra.

Corollary 7.9. The equational theory of all permutohedra lattices is decidable.

By defining U as the set of all triples (x, y, U ) with U = [x, y], we obtain the following.

Corollary 7.10. The equational theory of all Tamari lattices is decidable.

Tensor products and box products

Sections 8-10 will be mainly devoted to a proof of Theorem B, more precisely Theorem 10.1, showing that the equational theory of all permutohedra is non-trivial. We shall show that every Cambrian lattice of type A satisfies the splitting identity of the lattice N 5 B(3, 2); we give in this section the background and the tools for constructing and handling that lattice.

Our presentation originates from the tensor product of (∨, 0)-semilattices considered in Grätzer, Lakser, and Quackenbush [START_REF] Grätzer | The structure of tensor products of semilattices with zero[END_REF], which is a variant of Fraser's tensor product of join-semilattices considered in [START_REF] Fraser | The tensor product of semilattices[END_REF]. If A and B are finite lattices, then A ⊗ B = A ⊗ B is a finite lattice as well. In the infinite case, A ⊗ B may not be a lattice. For example, if F(3) denotes the free lattice on three generators, then M 3 ⊗ F(3) is not a lattice (cf. Grätzer and Wehrung [START_REF]Tensor products and transferability of semilattices[END_REF]). The following is stated in Grätzer and Wehrung [START_REF]Tensor products of semilattices with zero, revisited[END_REF]Definition 4.1]. Definition 8.2. For (∨, 0)-semilattices A and B, a subset C of A ⊗ B is a subtensor product if it contains all mixed tensors, C is closed under nonempty finite intersection, and C is a lattice under set inclusion. We say that C is capped if every member of C is a finite union of pure tensors.

If A and B are both finite, then every sub-tensor product is, trivially, capped. Grätzer and Wehrung posed in [START_REF]Tensor products of semilattices with zero, revisited[END_REF] the problem whether A ⊗ B a lattice implies that A ⊗ B is a capped tensor product, for any lattices A and B with zero. This problem appeared to be difficult, and was finally solved, with a sophisticated counterexample, in a recent preprint by Chornomaz [START_REF] Chornomaz | A non-capped tensor product of lattices[END_REF].

A key property of sub-tensor products, with trivial proof, is the following.

Lemma 8.3. Let A and B be lattices with zero, let C be a sub-tensor product of A and B, and let a ∈ A. Then the map (B → C, x → a ⊗ x) is a zero-preserving lattice homomorphism.

While even in the finite case, the ordinary tensor product A ⊗ B will not be satisfactory for our current purposes, a variant called box product will do the trick. The box product is an analogue, for lattices that are not necessarily complete, of Wille's tensor product of concept lattices [START_REF] Wille | Tensorial decomposition of concept lattices[END_REF]. Although the two concepts are, for finite lattices, equivalent, we found the box product presentation and results from Grätzer and Wehrung [START_REF] Grätzer | A new lattice construction: the box product[END_REF] more suited to our approach, heavily relying on join-coverings, in our lattices.

The box product of A and B behaves well only in case both lattices A and B are bounded 3 . The following result is contained in Proposition 2.9 and Lemma 3.8 of Grätzer and Wehrung [START_REF] Grätzer | A new lattice construction: the box product[END_REF].

c ⊗ b j = c ⊗ (q * ∨ b j ) ∧ c ⊗ (b 1 ∨ b 2 ) ; (8.1) c ⊗ a k = c ⊗ (a k ∨ b i ) ∧ c ⊗ (q * ∨ b j ) ; (8.2) c ⊗ (a k ∨ a l ) = c ⊗ (a k ∨ a l ∨ b i ) ∧ c ⊗ (q * ∨ b j ) ; (8.3)
The behavior of capped tensor products with respect to congruences will be especially important to us. The following is a consequence of Lemma 5.3 and Theorem 2 in Grätzer and Wehrung [START_REF]Tensor products of semilattices with zero, revisited[END_REF]. (i) The join-irreducible elements of C are exactly the p ⊗ q, where p ∈ Ji A and q ∈ Ji B. Furthermore, (p ⊗ q) * = (p * ⊗ q) ∪ (p ⊗ q * ). (ii) The join-prime elements of C are exactly the p ⊗ q, where p and q are joinprime in A and B, respectively. 3 The box product A B is a precursor of the further "lattice tensor product" construction A B, that may be defined even in some unbounded cases. This will be here of no concern to us.

Proof. The (easy) first part of (i) is contained in Wehrung [59, Lemma 7.2]. (ii). It is an easy exercise to verify that if p ⊗ q is join-prime, then so are p and q. Conversely, suppose that p and q are both join-prime. The box H = κ A (p) κ B (q) belongs to C, and p⊗q ⊆ H. Let I ∈ C such that p⊗q ⊆ I, and suppose that I ⊆ H. There exists (x, y) ∈ I \ H. By the definition of H, x κ A (p) and y κ B (q), that is, p ≤ x and q ≤ y, so (p, q) ∈ x ⊗ y ⊆ I, a contradiction. Therefore, H is the largest element of C not containing p ⊗ q.

A simple application of Proposition 8.5 and Lemma 8.6 yields, with the notational convention introduced in (8.5), the formula con C (p ⊗ q) = con A (p) ⊗ con B (q) , for all p ∈ Ji A and all q ∈ Ji B , (

whenever C is a sub-tensor product of finite lattices A and B.

Lemma 8.7. The following statements hold, for any capped sub-tensor product C of lattices A and B with zero:

(i) If A and B are both subdirectly irreducible, then so is C. Furthermore, if con A (p) is the monolith of A and con B (q) is the monolith of B, then con C (p ⊗ q) is the monolith of C. (ii) If A and B both belong to LB fin , then so does C. (iii) If A and B both belong to B fin , then so does A B. Further, κ A B (p ⊗ q) = κ A (p) κ B (q), for all p ∈ Ji A and all q ∈ Ji B. (iv) If A and B are both splitting, then so is A B.

Proof. (i) (see also Wille [60,Corollary 15]). It follows from Proposition 8.5 that if α is the monolith of A and β is the monolith of B, then α ⊗ β is the monolith of C. If α = con A (p) and β = con B (q), then α ⊗ β = con C (p ⊗ q) (use (8.6)).

(ii). Since the relations A and B are both antisymmetric, it follows from (8.6) and (2.2) that C is also antisymmetric.

(iii). By (ii) together with Theorems 2.56 and 2.64 in Freese, Ježek, and Nation [START_REF] Freese | Free Lattices[END_REF], it suffices to prove the second statement. Let H = i<n (a i b i ) with p ⊗ q ⊆ H (i.e., (p, q) / ∈ H) and (p ⊗ q) * ⊆ H. There exists i < n such that (p, q) / ∈ a i b i , that is, p a i and q b i . By Lemma 8.6(i), (p * , q) and (p, q * ) both belong to a i b i . It follows that p * ≤ a i and q * ≤ b i , hence

a i ≤ κ A (p) and b i ≤ κ B (q). Therefore, H ⊆ a i b i ⊆ κ A (p) κ B (q).
(iv) follows trivially from (i) and (iii) above.

Denote by λ(L) (resp., µ(L)) the cardinality of Ji L (resp., Mi L), for any finite lattice L. It follows from Freese, Ježek, and Nation [START_REF] Freese | Free Lattices[END_REF]Theorem 2.40] that L belongs to LB fin iff λ(L) = λ(Con L), and it follows from [START_REF] Freese | Free Lattices[END_REF]Theorem 2.67] that L belongs to B fin iff λ(L) = µ(L) = λ(Con L). While Lemma 8.7(ii) trivially implies that (A ∈ LB fin and B ∈ LB fin ) implies that A ⊗ B ∈ LB fin , the analogue result for B fin does not hold in general. For example, N 5 ⊗ N 5 has 9 join-irreducible elements and 10 meet-irreducible elements (for the union (p ⊗ p * ) ∪ (p * ⊗ p) ∪ (c ⊗ c) is meet-irreducible, but it is not a box), thus it does not belong to B fin . Hence, neither (iii) nor (iv) in Lemma 8.7, stated for the box product A B, can be extended to arbitrary capped sub-tensor products, even in the finite case.

Tight EA-duets of maps

In the present section we shall introduce an "equation-free" view of lattice varieties, in a great extent inspired by McKenzie [START_REF]Equational bases and nonmodular lattice varieties[END_REF]. This will enable us to prove Theorem B without needing to write huge equations.

Following Keimel and Lawson [START_REF] Keimel | Continuous and completely distributive lattices[END_REF], a Galois adjunction between posets K and L is a pair (f, h) of maps, where f : K → L and h : L → K, such that

f (x) ≤ y ⇐⇒ x ≤ h(y) , for all (x, y) ∈ K × L .
In such a case, each of the maps f and h is uniquely determined by the other. We say that f is the lower adjoint of h and h is the upper adjoint of f . Definition 9.1. Let K and L be lattices. A pair (f, g) of maps from K to L is an EA-duet 4 if there are a sublattice H of L and a surjective lattice homomorphism h : H K such that f is the lower adjoint of h and g is the upper adjoint of h.

Lemma 9.2. Let K and L be lattices and let f, g : K → L. Then (f, g) is an EA-duet iff f is a join-homomorphism, g is a meet-homomorphism, and

f (x) ≤ g(y) ⇔ x ≤ y , for all x, y ∈ K . (9.1)
Proof. If (f, g) is an EA-duet with respect to h : H K, then it is straightforward to verify that f is a join-homomorphism and g is a meet-homomorphism. Furthermore, f ≤ g, so x ≤ y implies f (x) ≤ g(y) and, conversely, for all x, y ∈ K, f (x) ≤ g(y) implies that x = hf (x) ≤ hg(y) = y.

Conversely, suppose that f is a join-homomorphism, g is a meet-homomorphism, and (9.1) holds. We set

H = x∈K [f (x), g(x)] . (9.2) For y ∈ H, let x 0 , x 1 ∈ K such that y ∈ [f (x 0 ), g(x 0 )] ∩ [f (x 1 ), g(x 1 )]. From f (x 0 ) ≤ y ≤ g(x 1
) and our assumptions it follows that x 0 ≤ x 1 . Likewise, x 1 ≤ x 0 , whence x 0 = x 1 . This entitles us to define a map h : H → K by the rule

h(y) = unique x ∈ K such that f (x) ≤ y ≤ g(x) , for each y ∈ H . (9.3) Observe, in particular, that h • f = h • g = id K (so h is surjective). Furthermore, f • h ≤ id H ≤ g • h.
It is also easily seen that h is isotone. Therefore the previous relations determine h as the upper adjoint of f and as the lower adjoint of g; it follows that h preserves all the meets and joins that exist in H. We are therefore left to argue that H is a sublattice of L.

If x i ∈ H and x i = h(y i ), for i ∈ {0, 1}, then f (x 0 ∧ x 1 ) ≤ f (x 0 ) ∧ f (x 1 ) ≤ y 0 ∧ y 1 ≤ g(x 0 ) ∧ g(x 1 ) = g(x 0 ∧ x 1 ) (because g is a meet-homomorphism),
whence y 0 ∧ y 1 ∈ H. The proof that y 0 ∨ y 1 ∈ H is similar.

Remark 9.3. It is an easy exercise to verify that in the context of Lemma 9.2 above, the sublattice H of L and the homomorphism h : H K are uniquely determined, by the formulas (9.2) and (9.3), respectively. 4 After the Soprano singer Aloysia Weber (1760-1839) and the Bass singer Édouard de Reske (1853-1917), moreover following the categorical logic notation ∃ h and ∀ h for the left and right adjoint of h, respectively. Calling "scores" the main objects of Section 6 and Appendix A stays in line with that musical spirit.

(ii)⇒(i) follows trivially from Lemma 9.2.

For every map f : K → L, the pointwise supremum f ∨ of all join-homomorphisms below f (for the componentwise ordering) is itself a join-homomorphism, and thus it is the largest join-homomorphism below f . We denote it by f ∨ . Likewise, we denote by f ∧ the least meet-homomorphism above f for the componentwise ordering. In particular,

f ∨ ≤ f ≤ f ∧ . Definition 9.8. A pair (f, g) of maps from K to L is tight if f = g ∨ and g = f ∧ .
In particular, if (f, g) is tight, then f is a join-homomorphism, g is a meet-homomorphism, and f ≤ g. Lemma 9.9. For every pair (f, g) of maps from K to L such that f is a join-homomorphism, g is a meet-homomorphism, and f ≤ g, there exists a tight pair (f , g)

such that f ≤ f ≤ g ≤ g. If (f, g) is an EA-duet, then so is (f , g).
Proof. Since f ≤ g and g is a meet-homomorphism, we get f ≤ f ∧ ≤ g. Now, since f is a join-homomorphism, we get f = f ∨ ≤ f ∧∨ ≤ f ∧ ≤ g, so it suffices to prove that the pair (f ∧∨ , f ∧ ) is tight, for which we shall argue that f ∧ = f ∧∨∧ . Here it goes:

f ∧∨∧ ≤ f ∧∧ = f ∧ , f ∧∨∧ ≥ f ∨∧ = f ∧ ,
the last equation following from the assumption that f ∨ = f . Finally, if (f, g) satisfies (9.1), then, since f ≤ f ≤ g ≤ g, (f , g) also satisfies (9.1).

By applying Lemma 9.2 and Lemma 9.9, we obtain immediately the following corollary.

Corollary 9.10. The following are equivalent:

(i) L is a homomorphic image of a sublattice of K.

(ii) There is an EA-duet of maps from K to L.

(iii) There exists a tight EA-duet of maps from K to L.

Although the two components of a tight pair may not be identical, we shall see that they agree on join-prime or meet-prime elements (cf. Corollary 9.12). In order to see this, the key lemma is the following. Lemma 9.11. Let g : K → L be an isotone map. Then g(0) = g ∨ (0). Furthermore, g(p) = g ∨ (p), for any join-prime element p of K.

Proof. Whenever p is join-prime, the map f : K → L defined by

f (x) = g(p) , if p ≤ x g(0 K ) , otherwise
, for all x ∈ K , is a join-homomorphism. (If there is no join-prime, define f (x) = g(0 K ) everywhere.) From the assumption that g is isotone it follows that f ≤ g, thus f ≤ g ∨ . Hence, g(0

K ) = f (0 K ) ≤ g ∨ (0 K ) ≤ g(0 K ) and g(p) = f (p) ≤ g ∨ (p) ≤ g(p).
Corollary 9.12. Let (f, g) be a tight EA-duet of maps from K to L. Then f and g agree on all elements of K that are either 0 K , 1 K , join-prime, or meet-prime.

Proof. Apply Lemma 9.11 to g : K → L and f : K op → L op .

10. An identity for all permutohedra: proving Theorem B

Throughout this section we shall set B = B(3, 2) and L = N 5 B. Since N 5 and B(3, 2) are both splitting lattices, it follows from Lemma 8.7 that L is also splitting. This section will be devoted to a proof of the following more precise form of Theorem B.

Theorem 10.1. Every permutohedron P(n) satisfies the splitting identity θ L of L.

Brute force calculation, based on the Mace4 component of McCune's wonderful

Prover9-Mace4 software [START_REF] Mccune | Prover9 and Mace4 [computer software[END_REF], shows that L has 3,338 elements, so θ L , although failing in L, holds in all lattices with at most 3,337 elements (cf. Section 2.4).

We argue by contradiction, assuming that not every permutohedron satisfies the splitting identity of L. By Lemma 3.1, it follows that there are a finite chain E and a subset U of E such that A U (E) does not satisfy the splitting identity of L, that is, L belongs to the lattice variety generated by A U (E). Since L is subdirectly irreducible and A U (E) is finite, it follows from Jónsson's Lemma (cf. Jónsson [START_REF]Algebras whose congruence lattices are distributive[END_REF], Jipsen and Rose [25, Chapter 1, Corollary 1.7]) that L is a homomorphic image of a sublattice of A U (E). By Corollary 9.10, it follows that there is a tight EA-duet (f, g) of maps from L to A U (E).

Since con N5 (p) is the monolith of N 5 and con B (q) is the monolith of B, it follows from Lemma 8.7(i) that con L (p ⊗ q) is the monolith of L. It follows that the pair (p ⊗ q, κ L (p ⊗ q)) is prime critical in L (cf. Definition 9.5). Further, it follows from Lemma 8.7(iii) that κ L (p ⊗ q) = κ N5 (p) κ B (q) = p * q * . By Lemma 9.6, (f, g) being an EA-duet means that f is a join-homomorphism, g is a meet-homomorphism, f ≤ g, and f (p ⊗ q) ⊆ g(p * q * ).

Take E of least possible cardinality and pick a pair

(u, v) ∈ f (p ⊗ q) \ g(p * q * ) .
It is easy to verify that the canonical projection π :

A U (E) → A U ∩[u,v] ([u, v]), a → a ∩ δ [u,v
] is a lattice homomorphism. Furthermore, the maps f = π • f and g = π • g are, respectively, a join-homomorphism and a meet-homomorphism from

L to A U ∩[u,v] ([u, v]) with f ≤ g and (u, v) ∈ f (p ⊗ q) \ g (p * q * ).
In particular, (f , g ) is also an EA-duet. By the minimality assumption on E, it follows that u and v are the least and the largest element of E, respectively. Hence, we may assume that E = [N ], for some positive integer N with (1, N ) ∈ f (p⊗q)\g(p * q * ), and that N is least possible.

Lemma 10.2. Let (x, y) ∈ 1, N U . If (x, y) ∈ f (c ⊗ q), then (x, y) ∈ g(0).
Proof. From (x, y) ∈ 1, N U and 1, N U ⊆ f (p⊗q) it follows that (x, y) ∈ f (p⊗q), thus, since f ≤ g, also (x, y) ∈ g(p⊗q). From (x, y) ∈ f (c⊗q) it follows that (x, y) ∈ g(c⊗q). Since g is a meet-homomorphism and (p⊗q)∧(c⊗q) = (p∧c)⊗q = 0⊗q = 0, (x, y) belongs to g(p ⊗ q) ∧ g(c ⊗ q) = g (p ⊗ q) ∧ (c ⊗ q) = g(0).

Let (x, y) ∈ f (c ⊗ q). Whenever j ∈ {1, 2}, the inequality q ≤ a 1 ∨ a 2 ∨ a 3 ∨ b j (within B) entails c ⊗ q ≤ (c ⊗ a 1 ) ∨ (c ⊗ a 2 ) ∨ (c ⊗ a 3 ) ∨ (c ⊗ b j ) (within L), thus there exists a subdivision x = z j 0 < z j 1 < • • • < z j nj = y such that whenever 0 ≤ i < n j , there exists d ∈ a ∪ {b j } such that (z j i , z j i+1 ) ∈ f (c ⊗ d) .
(10.1) Denote by ν j (x, y) the least possible value of n j . Our main lemma is the following.

Lemma 10.3. f (c ⊗ q) is contained in g(c ⊗ q * ).
Proof. Let (x, y) ∈ f (c ⊗ q), we argue by induction on y -x that (x, y) ∈ g(c ⊗ q * ). Consider subdivisions (z j i | 0 ≤ i ≤ n j ) of [x, y] satisfying (10.1), with n j = ν j (x, y). Set S j = {(z j i , z j i+1 ) | 0 ≤ i < n j } and Z j = {z j i | 0 ≤ i ≤ n j }, for each j ∈ {1, 2}. Suppose first that n j = 1 for some j ∈ {1, 2}, say n 1 = 1. It follows from (10.1) that (x, y) ∈ f (c ⊗ d) for some d ∈ a ∪ {b 1 }. Hence (x, y) ∈ g(c ⊗ d). Since (x, y) ∈ f (c ⊗ q) ⊆ g(c ⊗ q), g is a meet-homomorphism, and d ∧ q ≤ q * , it follows that (x, y) belongs to g (c ⊗ d) ∧ (c ⊗ q) = g c ⊗ (d ∧ q) ⊆ g(c ⊗ q * ), and we are done. Therefore we can suppose that n j > 1 for every j ∈ {1, 2}.

Claim 1. There is no i such that 0 ≤ i < n j , z j i / ∈ U , and z j i+1 ∈ U .

Proof of Claim. Suppose that 0 ≤ i < n j with z j i / ∈ U and z j i+1 ∈ U . It follows that (z j i , z j i+1 ) ∈ 1, N U . Without loss of generality, we can suppose that i > 0; let then d ∈ a ∪ {b j } be such that (

z j i-1 , z j i ) ∈ f (c ⊗ d). Recall that (x, y) ∈ f (c ⊗ q), thus (z j i , z j i+1 ) ∈ f (c ⊗ q)
as well; by using Lemma 10.2, we get (z j i , z j i+1 ) ∈ g(0), thus, a fortiori, (z j i , z j i+1 ) ∈ g(c ⊗ d). Since (f, g) is a tight pair and c ⊗ d is join-prime in L, we obtain, using Lemma 9.11, that f

(c ⊗ d) = g(c ⊗ d), thus (z j i , z j i+1 ) ∈ f (c ⊗ d), and thus (z j i-1 , z j i+1 ) ∈ f (c ⊗ d), and the subdivision x = z j 0 < • • • < z j i-1 < z j i+1 < • • • < z j nj =
y fills the same purpose as Z j while it has length n j -1, in contradiction with the minimality assumption on n j . Claim 1.

Claim 1 means that Z j \ {x, y} consists of a (possibly empty) bunch of elements of U , followed by a (possibly empty) bunch of elements of U c . This can be formally expressed by saying that for each j ∈ {1, 2}, there exists a unique integer m j ∈ [0, n j -1] such that z j i ∈ U whenever 0 < i ≤ m j and z j i / ∈ U whenever m j + 1 ≤ i < n j .

To ease the notation, we shall from now on set x j = z j mj and y j = z j mj +1 whenever j ∈ {1, 2}. We shall also set

∆ = {(t, t) | t ∈ [N ]} .
Claim 2. Suppose that (x j , y j ) belongs to f (c ⊗ a k ) for some j ∈ {1, 2} and some k ∈ {1, 2, 3}. Then (x, y) ∈ g(c ⊗ q * ).

Proof of Claim. From (x, y) ∈ f (c ⊗ q), x ≤ x j ≤ y, and x j ∈ {x} ∪ U it follows that (x, x j ) ∈ f (c ⊗ q) ∪ ∆. Likewise, (y j , y) ∈ f (c ⊗ q) ∪ ∆. By our induction hypothesis (on y -x), it follows that (x, x j ) and (y j , y) both belong to g(c ⊗ q * ) ∪ ∆. Furthermore, from a k ≤ q * it follows that c ⊗ a k ≤ c ⊗ q * , thus

(x j , y j ) ∈ f (c ⊗ a k ) ⊆ f (c ⊗ q * ) ⊆ g(c ⊗ q * ) .
Since (x, y) is contained in x, x j U ∨ x j , y j U ∨ y j , y U , we are done.

Claim 2.

From now on, until the end of the proof of Lemma 10.3, we shall thus assume that (x j , y j ) / ∈ f (c ⊗ a k ) whenever j ∈ {1, 2} and k ∈ {1, 2, 3}. By (10.1), the only remaining possibility is that (x j , y j ) ∈ f (c ⊗ b j ) for each j ∈ {1, 2}.

If {i, j} = {1, 2} and x i ≤ x j , define the left fin of S j as (x j , x j ), if x i = x j , and the unique (u, v) ∈ S j such that u ≤ x i < v, if x i < x j . Necessarily, {u, v} ⊆ U .

Symmetrically, the right fin of S j , defined in case y j ≤ y i , is (y j , y j ), if y i = y j , and the unique (u, v) ∈ S j such that u < y i ≤ v, if y j < y i . Necessarily, {u, v} ⊆ U c .

Observe that any (left or right) fin of S j belongs to S j ∪ ∆.

Claim 3. The following statements hold whenever {i, j} = {1, 2}.

(i) If x i ≤ x j , then the left fin (u, v) of S j belongs to f (c ⊗ a k ) ∪ ∆ for some k ∈ {1, 2, 3}; furthermore, v = x j . (ii) If y j ≤ y i , then the right fin (u, v) of S j belongs to f (c ⊗ a k ) ∪ ∆ for some k ∈ {1, 2, 3}; furthermore, u = y j .
Proof of Claim. We prove (i); the proof of (ii) is symmetric. The case where x i = x j is trivial, so we shall suppose that

x i < x j ; hence u ≤ x i < v ≤ x j . Suppose first that (u, v) / ∈ f (c ⊗ a k ) for any k ∈ {1, 2, 3}. It follows from (10.1) that (u, v) ∈ f (c ⊗ b j ). Since u ≤ x i < v and x i ∈ U , it follows that (u, x i ) ∈ f (c ⊗ b j ) ∪ ∆ . (10.2)
Moreover, from {u, x j , y j } ⊆ Z j and u < x j < y j it follows that

(u, x j ) ∈ f c ⊗ (q * ∨ b j ) and (u, y j ) ∈ f c ⊗ (q * ∨ b j ) . (10.3)
Now we argue by separating cases. In all cases, the key point is here to prove that (u,

y j ) ∈ f (c ⊗ (b 1 ∨ b 2 )).
Case 1. y i ≤ y j . This case is illustrated on the two top diagrams in Figure 10.1.

In this figure and all the following ones, the notation -→ z reminds us that z ∈ {x} ∪ U c , while the notation ←z reminds us that z ∈ {y} ∪ U . (a) If x j ≤ y i , then, since y i ≤ y j ≤ y, y i ∈ {y} ∪ U c , and (x j , y j ) ∈ f (c ⊗ b j ), we get

(y i , y j ) ∈ f (c ⊗ b j ) ∪ ∆ . (10.4) (b)
If y i < x j , then, since y i / ∈ U and x j ∈ U , we get (y i , x j ) ∈ 1, N U , thus, since (y i , x j ) ∈ x, y U ⊆ f (c ⊗ q) and by Lemma 10.2, (y i , x j ) ∈ g(0), and thus, a fortiori, (y i , x j ) ∈ g(c ⊗ b j ). Since c ⊗ b j is joinprime, it follows from Lemma 9.11 that (y i , x j ) ∈ f (c ⊗ b j ). Since (x j , y j ) ∈ f (c ⊗ b j ), (10.4) follows again. Hence, (10.4) is valid in any case. Now it follows from (x i , y i ) ∈ f (c⊗b i ), together with (10.2) and (10.4), that (u,

y j ) ∈ f (c⊗(b 1 ∨b 2 )), thus (u, y j ) ∈ g(c ⊗ (b 1 ∨ b 2 ))
. By applying the meet-homomorphism g to (8.1) and by using (10.3), we obtain that (u, y j ) belongs to

g c ⊗ (q * ∨ b j ) ∧ g c ⊗ (b 1 ∨ b 2 ) = g c ⊗ (q * ∨ b j ) ∧ c ⊗ (b 1 ∨ b 2 ) = g(c ⊗ b j ) = f (c ⊗ b j )
(use again Lemma 9.11) .

It follows that the subdivision, obtained from Z j by removing all the elements of Z j ∩ ]u, y j [ (in particular, x j ), fills the same purpose as Z j ; a contradiction by the minimality assumption on n j . Case 2. y j < y i . From x i < x j < y i , x j ∈ U , and (x i , y i ) ∈ f (c ⊗ b i ) it follows that (x i , x j ) ∈ f (c ⊗ b i ). By (10.2) together with (x j , y j ) ∈ f (c ⊗ b j ), it follows that (u,

u ←- x i c⊗bj -→ y i c⊗bi y j c⊗bj u v c⊗bj y j x j c⊗bj u ←- x i c⊗bj -→ y i c⊗bi ← -- x j 0 y j c⊗bj u v c⊗bj u ← - x i c⊗bj ← - x j c⊗bi y j c⊗bj u v c⊗bj x i y i c⊗bi
(u, v) ∈ f (c ⊗ a k ) ∪ ∆ in Claim 3 u ← - x i c⊗a k ← - x j c⊗bi x i y i c⊗bi u v c⊗a k u ← - x i c⊗a k -→ y i c⊗bi ← - x j 0 u v c⊗a k
y j ) ∈ f (c ⊗ (b 1 ∨ b 2 )), thus (u, y j ) ∈ g(c ⊗ (b 1 ∨ b 2 ))
. By applying the meet-homomorphism g to (8.1) and by using (10.3), it follows again, as in Case 1 above, that (u, y j ) ∈ f (c ⊗ b j ), which leads to the same contradiction as at the end of the proof of Case 1. This completes the proof that (u, v)

∈ f (c ⊗ a k ) for some k ∈ {1, 2, Since x ≤ u ≤ x i < v and x i ∈ {x} ∪ U , it follows that (u, x i ) ∈ f (c ⊗ a k ) ∪ ∆ . ( 10.5)
Now we must prove that v = x j . We argue by separating cases. In all cases, the key point is to show that (u, x j ) ∈ f (c ⊗ (a k ∨ b i )); see Figure 10.2. Case 1. x j ≤ y i . From (x i , y i ) ∈ f (c ⊗ b i ), x i < x j ≤ y i , and x j ∈ U it follows that (x i , x j ) ∈ f (c ⊗ b i ). Hence, by (10.5), it follows that (u,

x j ) ∈ f c ⊗ (a k ∨ b i ) , thus (u, x j ) ∈ g c ⊗ (a k ∨ b i )
. By using (10.3) and by applying the meet-homomorphism g to (8.2), it follows that (u, x j ) ∈ g(c ⊗ a k ), thus, by Lemma 9.11, (u, x j ) ∈ f (c ⊗ a k ). It follows that the subdivision, obtained by removing from Z j all the elements of fills the same purpose as Z j ; whence, by the minimality assumption on Z j , we get v = x j . Case 2. y i < x j . Then (y i , x j ) ∈ 1, N U , thus, since (y i , x j ) ∈ x, y U ⊆ f (c ⊗ q)

Z j ∩ ]u, x j [, u ← - x 2 c⊗ai -→ y 2 c⊗b2 v c⊗aj u x 1 c⊗ai y 1 v c⊗aj u ← - x 1 c⊗ai y 1 c⊗b1 v c⊗aj u x 2 c⊗ai -→ y 2 c⊗b2 v c⊗aj
and by Lemma 10.2, (y i , x j ) ∈ g(0), and thus, a fortiori, (y i , x j ) ∈ g(c⊗b i ), and hence, by Lemma 9.11, (

y i , x j ) ∈ f (c ⊗ b i ). Since (x i , y i ) ∈ f (c ⊗ b i )
and by (10.5), it follows that (u,

x j ) ∈ f (c ⊗ (a k ∨ b i ))
. The conclusion v = x j is then obtained in the same way as in Case 1 above.

This completes the proof of Claim 3. Claim 3.

In order to finish the proof of Lemma 10.3, we argue by separating cases, according to the relative positions of the intervals [x 1 , y 1 ] and [x 2 , y 2 ]. By symmetry, there are two cases to consider (see Figure 10.3).

Case 1. [x 1 , y 1 ] ⊆ [x 2 , y 2 ]
. Denote by (u, x 1 ) and (y 1 , v) the left fin and the right fin of S 1 , respectively (cf. Claim 3). In particular, u ≤

x 2 ≤ x 1 < y 1 ≤ y 2 ≤ v.
Furthermore, by Claim 3, there are i, j ∈ {1, 2, 3} such that (u,

x 1 ) ∈ f (c ⊗ a i ) ∪ ∆ and (y 1 , v) ∈ f (c ⊗ a j ) ∪ ∆. From x ≤ u ≤ x 2 ≤ x 1 , (u, x 1 ) ∈ f (c ⊗ a i ) ∪ ∆, and x 2 ∈ {x} ∪ U it follows that (u, x 2 ) ∈ f (c ⊗ a i ) ∪ ∆. Symmetrically, (y 2 , v) ∈ f (c ⊗ a j ) ∪ ∆. Since (x 2 , y 2 ) ∈ f (c ⊗ b 2 ) ∪ ∆, it follows that (u, v) ∈ f c ⊗ (a i ∨ a j ∨ b 2
) . On the other hand, from {u, v} ⊆ Z 1 and u < v it follows that (u, v) ∈ f c ⊗ (q * ∨ b 1 ) . Since f ≤ g and by applying the meet-homomorphism g to (8.3), it follows that (u, v) ∈ g c ⊗ (a i ∨ a j ) ; whence (u, v) ∈ g(c ⊗ q * ). Now, from the induction hypothesis it follows that (x, u) and (v, y) both belong to the set g(c ⊗ q * ) ∪ ∆; whence (x, y) ∈ g(c ⊗ q * ). Case 2. x 1 < x 2 and y 1 < y 2 . Denote by (u, x 2 ) the left fin of S 2 and by (y 1 , v) the right fin of S 1 (cf. Claim 3). It follows from Claim 3 that there are i, j ∈ {1, 2, 3} such that (u,

x 2 ) ∈ f (c ⊗ a i ) ∪ ∆ and (y 1 , v) ∈ f (c ⊗ a j ) ∪ ∆. From u ≤ x 1 < x 2 , (u, x 2 ) ∈ f (c ⊗ a i ) ∪ ∆, and x 1 ∈ U it follows that (u, x 1 ) ∈ f (c ⊗ a i ) ∪ ∆. Since (x 1 , y 1 ) ∈ f (c ⊗ b 1 ) and (y 1 , v) ∈ f (c ⊗ a j ) it thus follows that (u, v) ∈ f c ⊗ (a i ∨ a j ∨ b 1 )
. A similar proof, using this time the subdivision u < x 2 < y 2 ≤ v, yields the relation (u, v) ∈ f c ⊗ (a i ∨ a j ∨ b 2 ) . Since f ≤ g and by applying the meet-homomorphism g to (8.3), it follows that (u, v) ∈ g c ⊗ (a i ∨ a j ) . We conclude that (x, y) ∈ g(c ⊗ q * ) as in the last part of the proof of Case 1 above.

This concludes the proof of Lemma 10.3.

The conclusion of Lemma 10.3, together with c ⊗ q ⊆ c ⊗ q * , implies that (f, g) cannot be an EA-duet. This contradiction concludes the proof of Theorem 10.1.

It is plausible that a more detailed argument, based on the same idea, would yield that no sub-tensor product of N 5 ⊗ B(3, 2) belongs to the variety generated by all P(n). There would be some difficulties in checking this, for instance the other sub-tensor products (than the box product) are no longer splitting lattices.

11. Permutohedra on locally dismantlable lattices: proving Theorem C

The present section will deal with the extended permutohedron R(E) on a (possibly infinite) poset E, as introduced in Santocanale and Wehrung [START_REF]The extended permutohedron on a transitive binary relation[END_REF] (cf. Section 3), and prove that those R(E) satisfy no nontrivial lattice identity. The posets in question will actually be lattices of a very special kind. Definition 11.1. A lattice L is dismantlable (cf. Rival [START_REF] Rival | Lattices with doubly irreducible elements[END_REF], Kelly and Rival [START_REF] Kelly | Crowns, fences, and dismantlable lattices[END_REF]) if it is finite and every sublattice of L with at least three elements has an element which is doubly irreducible, that is, both meet-and join-irreducible; locally dismantlable if every finite subset of L is contained in a dismantlable sublattice of L.

A poset S is a sub-poset of a poset T if S is contained in T and the inclusion mapping of S into T is an order-embedding. The proof of the following lemma is straightforward.

Lemma 11.3. The following statements hold, for any segment extension T of a poset S.

(i) If S is a lattice, then so is T . Furthermore, S is a sublattice of T .

(ii) If S is a dismantlable lattice, then so is T .

The following definition is mainly taken from Santocanale and Wehrung [48, § 10]. Definition 11.4. Let S be a poset and let L be a lattice.

• A map µ : δ S → L is an L-valued polarized measure on S if µ(x, y) ≤ µ(x, z) ≤ µ(x, y) ∨ µ(y, z) whenever x < y < z in S. • A refinement problem for a polarized measure µ is a quadruple (x, y, a 0 , a 1 ), where (x, y) ∈ δ S and a 0 , a 1 ∈ L, such that µ(x, y) ≤ a 0 ∨ a 1 . • A solution of the refinement problem above is a subdivision

x = z 0 < z 1 < • • • < z n = y in S such that each µ(z i , z i+1 ) is contained in some a j .
The main lemma of this section is the following.

Lemma 11.5. Let S be a finite poset, let u < v in S, let L be a finite meet-semidistributive lattice, let µ : δ S → L be a polarized measure, and let a 0 , a 1 ∈ L such that µ(u, v) ≤ a 0 ∨ a 1 . Then there are a finite segment extension T of S and a polarized measure ν : δ T → L extending µ such that: (i) The refinement problem ν(u, v) ≤ a 0 ∨ a 1 can be solved in T .

(ii) If the range of µ does not contain zero, then neither does the range of ν.

Proof. As the conclusion is trivial if µ(u, v) ≤ a j for some j < 2 (take T = S and ν = µ), we shall assume that µ(u, v) a j for all j < 2. In particular, both a 0 and a 1 are nonzero; furthermore, it is ruled out that µ(u, v) ∧ a j = 0 for each j < 2, for then we would infer, by the meet-semidistributivity of L, that µ(u, v) = µ(u, v) ∧ (a 0 ∨ a 1 ) = 0, a contradiction. Hence we may assume that µ(u, v) ∧ a 0 is nonzero.

An intuitive description of what follows is that we first attach an infinite copy of the chain ω of all nonnegative integers to S between u and v; then we show that all large enough members of that ω are redundant, so we get rid of them.

We shall also use the convention µ(x, x) = 0 for each x ∈ S. We shall set ε(n) = n mod 2 for each integer n, and we shall endow the cartesian product (S ↓ u) × ω with the partial ordering ≤ * defined by (x, k) ≤ * (y, l) ⇐⇒ (y ≤ x and k ≤ l) , for all (x, k), (y, l) ∈ (S ↓ u) × ω .

We define, by ≤ * -induction, a map f : (S ↓ u) × ω → L by the rule f (x, 0) = µ(x, u) , (11.1)

f (x, k + 1) = µ(x, t) ∨ f (t, k + 1) | t ∈ ]x, u] ∧ f (x, k) ∨ a ε(k) ∧ µ(x, v) , (11.2)
for each (x, k) ∈ (S ↓ u) × ω. As usual, empty meets are identified with the top element of L.

Claim 1. The inequality f (x, k) ≤ µ(x, y) ∨ f (y, k) holds, for all x < y in S ↓ u and all k < ω.

Proof of Claim. We argue by induction on k. The conclusion holds for k = 0 because µ is a polarized measure. If the statement holds at k, then, setting t = y in the meet in the defining equation (11.2), we obtain the inequality f (x, k + 1) ≤ µ(x, y) ∨ f (y, k + 1). Claim 1.

Claim 2. µ(x, u) ≤ f (x, k) ≤ µ(x, v), for each (x, k) ∈ (S ↓ u) × ω.
Proof of Claim. The inequality f (x, k) ≤ µ(x, v) is trivial. For the inequality µ(x, u) ≤ f (x, k), we argue by ≤ * -induction on (x, k). The result is trivial for k = 0. Suppose that it holds at every pair ≤ * -smaller than (x, k + 1). For each t ∈ ]x, u], it follows from the induction hypothesis that µ(t, u) ≤ f (t, k + 1), thus µ(x, u) ≤ µ(x, t) ∨ µ(t, u) ≤ µ(x, t) ∨ f (t, k + 1). Furthermore, from the induction hypothesis it follows that µ(x, u) ≤ f (x, k), whence µ(x, u) ≤ f (x, k)∨a ε(k) . Recalling also that µ(x, u) ≤ µ(x, v), the result follows immediately from equation (11.2) defining f (x, k + 1). Claim 2.

Claim 3. The inequality f (x, k) ≤ f (x, k + 1) holds, for each (x, k) ∈ (S ↓ u) × ω.
Proof of Claim. We argue by downward induction on x. For each t ∈ ]x, u], it follows from the induction hypothesis that f (t, k) ≤ f (t, k +1), thus, using Claim 1,

f (x, k) ≤ µ(x, t) ∨ f (t, k) ≤ µ(x, t) ∨ f (t, k + 1). Since f (x, k) ≤ f (x, k) ∨ a ε(k)
, the result follows immediately from (11.2). Claim 3.

By Claim 3 and as L and S ↓ u are both finite, there exists m ∈ ω \ {0} such that

(∀x ∈ S ↓ u)(∀k ≥ m in ω) f (x, k) = f (x, m) .
For the rest of the proof of Lemma 11.5 we shall fix that integer m. Set g(x) = f (x, m), for each x ∈ S ↓ u.

Claim 4. The equality g(x) = µ(x, v) holds, for each x ∈ S ↓ u.

Proof of Claim. We argue by (downward) induction on x. For each t ∈ ]x, u], it follows from the induction hypothesis that g(t) = µ(t, v), thus µ(x, t) ∨ g(t) ≥ µ(x, v). Therefore, by applying (11.2) to k ∈ {m + 1, m + 2}, we obtain that

g(x) = µ(x, t) ∨ g(t) | t ∈ ]x, u] ∧ g(x) ∨ a ε(k) ∧ µ(x, v) = g(x) ∨ a ε(k) ∧ µ(x, v) .
Therefore, by using the meet-semidistributivity of L, we obtain

g(x) = (g(x) ∨ a 0 ∨ a 1 ) ∧ µ(x, v) . (11.3)
Now, by using Claim 2, g(x)∨a 0 ∨a 1 ≥ µ(x, u)∨µ(u, v) ≥ µ(x, v), thus, using (11.3), g(x) = µ(x, v). Claim 4.

Now we fix new symbols t 1 , . . . , t m-1 and we set T = S ∪ {t 1 , . . . , t m-1 }, with u < t 1 < • • • < t m-1 < v. Furthermore, we extend the ordering of S to T by letting (s ≤ t i ⇔ s ≤ u) and (t i ≤ s ⇔ v ≤ s), whenever s ∈ S.

We extend the map µ to a map ν : δ T → L by setting

ν(x, t k ) = f (x, k) , for each (x, k) ∈ (S ↓ u) × [1, m[ , (11.4
)

ν(t k , t l ) = (a ε(i) | k ≤ i < l) , whenever 1 ≤ k < l < m , (11.5)
ν(t k , y) = (a ε(i) | k ≤ i < m) ∨ µ(v, y) , for each (k, y) ∈ [1, m[ × (S ↑ v) . (11.6)
Verifying that ν is a polarized measure amounts to verifying the following statements.

• µ(x, y) ≤ f (x, k) ≤ µ(x, y)∨f (y, k), for all x < y in S ↓u and all k ∈ [1, m[. This follows trivially from Claims 1 and 2.

• f (x, k) ≤ f (x, l) ≤ f (x, k) ∨ ν(t k , t l ),
= k + 1. • f (x, k) ≤ µ(x, y) ≤ f (x, k) ∨ ν(t k , y), for all (x, y) ∈ (S ↓ u) × (S ↑ v) and all k ∈ [1, m[.
The first inequality follows from Claim 2 together with µ(x, v) ≤ µ(x, y). In order to prove the second inequality, we separate cases

. If k ≤ m -2, then, as µ(u, v) ≤ a 0 ∨ a 1 , f (x, k) ∨ ν(t k , y) = f (x, k) ∨ a 0 ∨ a 1 ∨ µ(v, y) ≥ µ(x, u) ∨ µ(u, v) ∨ µ(v, y) (by Claim 2) ≥ µ(x, y)
and we are done.

If k = m -1, then f (x, k) ∨ ν(t k , y) = f (x, k) ∨ a ε(k) ∨ µ(v, y) ≥ f (x, k + 1) ∨ µ(v, y) (use (11.2)) = g(x) ∨ µ(v, y) = µ(x, v) ∨ µ(v, y) (by Claim 4) ≥ µ(x, y)
and we are done again.

• ν(t k , t l ) ≤ ν(t k , y) ≤ ν(t k , t l ) ∨ ν(t l , y), for all k < l in [1, m[ and all y ∈ S ↑ v. This follows immediately from (11.5) and (11.6). • ν(t k , x) ≤ ν(t k , y) ≤ ν(t k , x) ∨ µ(x, y), for all k ∈ [1, m[ and all x < y in S ↑ v. This follows immediately from (11.6). Hence we have proved that ν is a polarized measure. By construction, the refinement problem ν(u, v) ≤ a 0 ∨ a 1 can be solved in T . Now suppose that the range of µ does not contain the zero of L (provided the latter exists). In order to prove that ν satisfies the same statement and recalling that a i = 0 for i < 2, it will be enough to prove that f (x, k) is nonzero for every x ∈ S ↓u and every positive integer k. By Claim 2, if f (x, k) = 0, then µ(x, u) = 0 (remember the convention µ(u, u) = 0), thus x = u, and thus, by Claim 3, f (u, 1) = 0, that is, using 11.2, a 0 ∧ µ(u, v) = 0, which we have ruled out from the beginning. This concludes the proof. This brings us to the main result of this section, involving the extended permutohedron R(E) and its meet-subsemilattice A(E) (cf. Section 3). From now on, by "countable" we will always mean "at most countable". Theorem 11.6. Let L be a finite meet-semidistributive lattice. There are a countable, locally dismantlable lattice E together with a zero-preserving lattice embedding ϕ : L → R(E) with range contained into A(E). In particular, ϕ is also a zero-preserving lattice embedding from L into A(E).

Proof. Endowing the finite set E 0 = L \ {0} with any strict well-ordering, the map µ 0 : δ E0 → L, (x, y) → x is a polarized measure with nonzero values. Having defined a polarized measure µ n : δ En → L with nonzero values, and with E n a dismantlable lattice, a straightforward iteration of Lemma 11.5, invoking Lemma 11.3 for the preservation of dismantlability, yields a dismantlable extension E n+1 of E n and a polarized measure µ n+1 : δ En+1 → L with nonzero values, extending µ n , such that every refinement problem for µ n is solved by µ n+1 .

The union µ of all µ n is an L-valued polarized measure on the countable, locally dismantlable lattice E = n∈ω E n . It has nonzero values, and every refinement problem for µ has a solution. The map ϕ defined on L by the rule ϕ(a) = {(x, y) ∈ δ E | µ(x, y) ≤ a} , for all a ∈ L , takes its values in A(E). As the meet in A(E) is intersection, ϕ is a meet-homomorphism to A(E); as A(E) is a meet-subsemilattice of R(E), ϕ is also a meet-homomorphism to R(E). Since µ takes nonzero values, ϕ is zero-preserving. Moreover, since µ solves all its own refinement problems and since the join in R(E) is the transitive closure of the union, the definition of ϕ yields immediately that ϕ is a join-homomorphism to R(E). Finally, let us notice that ϕ is also a join-homomorphism to A(E); indeed, while the join in A(E) is, in general, not the transitive closure of the union, the fact that ϕ(a 0 ∨ a 1 ) belongs to A(E) forces it to be the join ϕ(a 0 ) ∨ ϕ(a 1 ) within A(E).

Finally, since µ extends µ 0 , its range is L \ {0}; whence ϕ is one-to-one.

Corollary 11.7. Every free lattice embeds, as a sublattice, into R(E) for some locally dismantlable lattice E, via a map with range contained in A(E).

Proof. A well known result by Day (cf. Freese, Ježek, and Nation [11, Theorem 2.84]) states that every free lattice embeds into a direct product of members of B fin . Since every member of B fin is meet-semidistributive, it follows from Theorem 11.6 that every free lattice embeds into a product i∈I R(E i ), for a collection (E i | i ∈ I) of locally dismantlable lattices E i . Fixing a strict well-ordering on I, the disjoint union E = i∈I ({i} × E i ), endowed with the lexicographical ordering (i.e., (i, x) ≤ (j, y) if either i j or (i = j and x ≤ y)), is locally dismantlable, and i∈I R(E i ) embeds into R(E) via (x i | i ∈ I) → ∈I x i . The latter assignment maps i∈I A(E i ) into A(E).

In particular, we get the following more precise form of Theorem C.

Corollary 11.8. There is no nontrivial lattice-theoretical identity satisfied by all R(E) (resp., A(E)), for E a countable, locally dismantlable lattice. Remark 11.9. Every sub-poset E of a poset F induces a (∧, 1)-homomorphism π F E : A(F ) → A(E), x → x ∩ δ E . This map preserves all directed joins. Now let E = n∈ω E n be an increasing union of finite dismantlable lattices E n . It is obvious that A(E), together with the maps π E En , is the inverse limit, in the category of all (∧, 1)-semilattices, of the A(E n ). Now it can be proved that this implies that A(E) belongs to the lattice variety generated by all A(E n ). Hence we can strengthen part of the statement of Corollary 11.8 as follows: The lattices A(E), for E ranging over all finite dismantlable lattices, do not satisfy any nontrivial lattice identity.

However, for a sub-poset E of a poset F , the assignment x → x ∩ δ E does not necessarily map R(F ) to R(E), so the argument above does not extend to R(E).

Remark 11.10. The locally dismantlable lattice E in Theorem 11.6 is obtained by means of successive segment extensions. Such extensions usually create squares. It can therefore be asked whether a better construction would lead to an embedding of every lattice from B fin into some P(E), with E square-free. This is actually not possible, as if E is square-free, then P(E) is a subdirect product of permutohedra, see Santocanale and Wehrung [51, Exercices 2.4-2.6].

Discussion

Our results raise a whole array of new questions.

12.1. How far can we go? Extending a result by Sekanina [START_REF] Sekanina | On a characterisation of the system of all regularly closed sets in general closure spaces[END_REF], the three papers Iturrioz [START_REF] Iturrioz | A simple proof of a characterization of complete orthocomplemented lattices[END_REF], Katrnoška [START_REF] Katrnoška | On the representation of orthocomplemented posets[END_REF], and Mayet [START_REF] Mayet | Une dualité pour les ensembles ordonnés orthocomplémentés[END_REF] established simultaneously that every orthoposet can be obtained as the poset of all clopen (i.e., closed and open) subsets in some closure space; hence the ortholattices of clopen sets satisfy no nontrivial identity. Nevertheless, setting restrictions on the closure space (P, ϕ) brings restrictions to the corresponding lattice Reg(P, ϕ) of regular closed subsets (i.e., the closures of open sets). For example, we prove in our paper [START_REF]Lattices of regular closed subsets of closure spaces[END_REF] that if (P, ϕ) is a finite convex geometry, then Reg(P, ϕ) is pseudocomplemented. We do not know whether there is a nontrivial lattice identity satisfied by Reg(P, ϕ) for every finite convex geometry (P, ϕ). In view of Theorem C (cf. Corollary 11.8), this certainly sounds unplausible. Then the possibility arises that every class of closure spaces (P, ϕ) would yield an identity for all the corresponding Reg(P, ϕ). Particular instances of that question, along with natural variants, would be the following:

(1) Is it the case that for every positive integer d there exists a nontrivial lattice identity satisfied by the extended permutohedron R(E) for every finite poset E of order-dimension at most d? Note that there are finite dismantlable posets of arbitrarily large order-dimension, see Kelly [START_REF] Kelly | On the dimension of partially ordered sets[END_REF].

(2) Can every finite Coxeter lattice be embedded into some P(n)? (We know that this holds for Coxeter lattices of type B.) Does it at least belong to the variety generated by all P(n)? (3) Similar questions can be asked for the various classes of "permutohedra" considered in our papers [START_REF]The extended permutohedron on a transitive binary relation[END_REF][START_REF]Lattices of regular closed subsets of closure spaces[END_REF]: most notably, lattices of regular closed subsets constructed from semilattices, graphs, hyperplane arrangements.

12.2. Finitely based subvarieties of the variety generated by all permutohedra. Denote by P the variety generated by all permutohedra. Is it decidable whether the class of all lattices satisfying a given lattice identity is contained in P? Since the variety generated by a given finite lattice can be defined by a single identity (McKenzie [START_REF] Mckenzie | Equational bases for lattice theories[END_REF]), this would solve the other question whether a given finite lattice belongs to P. Those questions arise, for instance, for the lattices B(m, n) (cf. Section 2.5, also Appendix A where we give a combinatorial equivalent of the corresponding question), or for Nation's identity β 1 from [41, page 537] (since N 5 B(3, 2) satisfies β 2 we do not need to try other β n ). In particular, we know since [START_REF] Santocanale | Sublattices of associahedra and permutohedra[END_REF] that B(3, 3) and all B(n, 2) belong to P, but we do not know whether B(4, 3) belongs to P (cf. Appendix A). A related question is the one whether the variety P can be defined by finitely many lattice identities (equivalently, by a single lattice identity).

12.3. Varieties and quasivarieties of ortholattices. Recall that a quasi-identity is a formula of the form (∀ x) p 1 ( x) = q 1 ( x) and • • • and p n ( x) = q n ( x) ⇒ p( x) = q( x) , where all p, q, p i , q i are terms. It is known since Bruns [5, § (4.

2)] that the set of all quasi-identities satisfied by all ortholattices is decidable. Can Theorem A be extended to permutohedra viewed as ortholattices, that is, lattices with an additional unary operation symbol for complementation? Can Theorem A be extended to quasi-identities? Of course, the questions asked in Subsections 12.2-12.3 can be extended similarly.

12.4. Tractability of the algorithm. While the equational theory of all permutohedra, respectively Tamari lattices, is decidable (cf. Corollaries 7.9 and 7.10), the implied algorithms are totally intractable, even for very simple identities. We do not know whether there is any tractable algorithm for those problems. The algorithms rely on Büchi's Theorem [START_REF] Büchi | On a decision method in restricted second order arithmetic[END_REF] for S1S; the complexity of deciding MSO statements is determined by the automata theoretical constructions corresponding to logical operations, thus by the logical complexity of formulas, see Thomas However, in some cases it is possible to express a negated lattice inclusion in a way which, if it falls short of yielding any practical implementation, produces nonetheless a rather transparent combinatorial description. We choose to illustrate this here for the splitting identity of the lattice B(m, n) described in Section 2.5.

(A 1 ) 1 b 1 - → 2 a 1 ← - 5 b 2 - → 8

5 Figure 2 . 1 .

 521 Figure 2.1. The lattices M 3 and N 5 1To the great puzzlement of many people, bounded homomorphic images of free lattices are

2 qFigure 2 . 2 .

 222 Figure 2.2. The join-irreducible elements of N 5 (left) and B(3, 2) (right)

Definition 7 . 7 .

 77 An orientation is a triple (u, v, U ), where u, v ∈ ω, u < v, and U ⊆ [u, v].

Definition 8 . 1 .

 81 Let A and B be (∨, 0)-semilattices. A bi-ideal of A × B is a lower subset I of A × B (endowed with the componentwise ordering), containing the subset 0 A,B = (A × {0 B }) ∪ ({0 A } × B) , such that whenever (a, b 0 ) ∈ I and (a, b 1 ) ∈ I, then (a, b 0 ∨ b 1 ) ∈ I, and similarly with the roles of A and B reversed. The (∨, 0)-semilattice A ⊗ B of all compact elements of A ⊗ B is called the tensor product of the (∨, 0)-semilattices A and B. The following elements of A ⊗ B deserve a special attention: -The pure tensors a ⊗ b = 0 A,B ∪ {(x, y) ∈ A × B | x ≤ a and y ≤ b}, whenever (a, b) ∈ A × B. In particular, 0 A,B = 0 A ⊗ 0 B . -The mixed tensors (a ⊗ b ) ∪ (a ⊗ b), whenever a ≤ a in A and b ≤ b in B. -The boxes, a b = {(x, y) ∈ A × B | x ≤ a or y ≤ b}. Clearly, the inequalities a ⊗ b ≤ a b and a ⊗ b ≤ a b hold whenever a, a ∈ A and b, b ∈ B. In fact, a ⊗ b = (a 0 B ) ∩ (0 A b). Notice also that if a and b are both nonzero, then a ⊗ b ≤ a ⊗ b iff a ≤ a and b ≤ b . While pure tensors and mixed tensors always belong to A ⊗ B (in particular, (a ⊗ b ) ∪ (a ⊗ b) is really the join of a ⊗ b and a ⊗ b), the box a b may not belong to A ⊗ B. However, if A and B both have a unit element, then a b = (a ⊗ 1 B ) ∪ (1 A ⊗ b) is a mixed tensor, thus it belongs to A ⊗ B.

Proposition 8 . 4 .

 84 Let A and B be bounded lattices. The set A B of all intersections of the form n i=1 (a i b i ), for n a non-negative integer, a 1 , . . . , a n ∈ A, and b 1 , . . . , b n ∈ B, is a lattice under set-theoretical inclusion, called the box product of A and B. Furthermore, A B is a capped sub-tensor product of A and B. Let A = N 5 and B = B(3, 2). By combining Lemma 8.3, Proposition 8.4, and the equations (2.3)-(2.5), we obtain immediately the following equations, valid in the lattice N 5 B(3, 2) whenever {i, j} = {1, 2} and k, l ∈ {1, 2, 3}:

Proposition 8 . 5 . 5 ) 8 . 6 .

 85586 Let A and B be lattices with zero and let C be a capped subtensor product of A and B. Then there exists a unique lattice isomorphism ε from(Con c A) ⊗ (Con c B) onto Con c C such that ε con A (a, a ) ⊗ con B (b, b ) = con C (a ⊗ b ) ∪ (a ⊗ b), a ⊗ b whenever a ≤ a in A and b ≤ b in B . (8.4)From now on we shall abuse notation and write α ⊗ β instead of ε(α ⊗ β), whenever (α, β) ∈ (Con c A) × (Con c B). With this abuse of notation, the formula (8.4) becomescon A (a, a ) ⊗ con B (b, b ) = con C (a ⊗ b ) ∪ (a ⊗ b), a ⊗ b whenever a ≤ a in A and b ≤ b in B . (8.Lemma The following statements hold, for any sub-tensor product C of finite lattices A and B:

Figure 10 . 1 .

 101 Figure 10.1. Cases 1.a (up-left), 1.b (up-right), and 2 (down) in the proof of (u, v) ∈ f (c ⊗ a k ) ∪ ∆ in Claim 3

Figure 10 . 2 .

 102 Figure 10.2. Cases 1 (left) and 2 (right) in the proof of v = x j in Claim 3

Figure 10 . 3 .

 103 Figure 10.3. Final cases in the proof of Lemma 10.3: Case 1 (left) and Case 2 (right)

Definition 11 . 2 .

 112 A poset T is a segment extension of a sub-poset S if there is a nonempty finite chain C of T , with extremities x = min C and y = max C, such that (i) C ∩ S = {x, y} and C ∪ S = T ; (ii) (s ≤ z ⇔ s ≤ x) and (s ≥ z ⇔ s ≥ y), whenever s ∈ S and z ∈ C.

  for all x ∈ S ↓ u and all k < l in [1, m[. The first inequality follows from Claim 3. For l = k + 1, the second inequality follows trivially from (11.2) and (11.5), while for l ≥ k + 2, it follows from (11.5) together with the case where l

[ 58 ,

 58 Section 3] or Perrin and Pin [42, Chapter 1]. Appendix A. An example: (m, n)-scores on a finite chain It is interesting to see what becomes of the decidability results established in Section 7 for concrete lattice identities. A blunt application of Theorem 7.1 to the translation obtained in Section 6, via scores, of negated lattice inclusions, looks quite hopeless from a practical viewpoint.

Figure A. 1 . 2 )Figure B. 1 .

 121 Figure A.1. A (3, 3)-score on [12] with respect to U = {5, 6, 9, 10, 11}

  Origin of the problems and statement of the results. It was proved in Iwasawa

	5. Half-scores and alternating words	11
	6. Scores and lattice inclusions	13
	7. Expressing scores within monadic second-order logic: proving
	Theorem A	15
	8. Tensor products and box products	19
	9. Tight EA-duets of maps	22
	10. An identity for all permutohedra: proving Theorem B	25
	11. Permutohedra on locally dismantlable lattices: proving Theorem C	30
	12. Discussion	34
	12.1. How far can we go?	34
	12.2. Finitely based subvarieties of the variety generated by all
	permutohedra	35
	12.3. Varieties and quasivarieties of ortholattices	35
	12.4. Tractability of the algorithm 1. Introduction
	1.1.
	1. Introduction	2
	1.1. Origin of the problems and statement of the results	2
	1.2. Hidden identities in classes of structures	3
	1.3. Organization of the paper	4
	2. Notation and terminology	6
	2.1. Basic concepts	6
	2.2. Semidistributivity	6
	2.3. Join-dependency and congruences	7
	2.4. Bounded homomorphic images of free lattices	7
	2.5. The lattices B(m, n)	8
	3. Permutohedra and Cambrian lattices of type A	8
	4. Dualities between Cambrian lattices of type A	9

Our next lemma involves the relation of weak projectivity ⇒. Let us first recall some basic definitions (cf. Grätzer [START_REF] Grätzer | Lattice Theory: Foundation[END_REF]§ III.1]). We define binary relations

The following lemma gives a convenient characterization of EA-duets defined on a subdirectly irreducible lattice with a prime critical pair. Lemma 9.6. Let K and L be lattices, with K subdirectly irreducible, and let u, v ∈ K with u v. Let f : K → L be a join-homomorphism and let g : K → L be a meet-homomorphism with f ≤ g. If (f, g) is an EA-duet, then f (u) g(v). Furthermore, if (u, v) is prime critical, then the converse holds.

Proof. If (f, g) is an EA-duet, then, by Lemma 9.2, the condition (9.1) is satisfied, thus u v implies that f (u) g(v).

Suppose, conversely, that (u, v) is prime critical and f (u) g(v). If (f, g) is not an EA-duet, then there are x, y ∈ K such that f (x) ≤ g(y) and x y. Since f (x) ≤ g(x) and g is a meet-homomorphism, we obtain that f (x) ≤ g(x ∧ y). Since x ∧ y < x, the congruence con(x ∧ y, x) is nonzero, thus it contains the monolith con(u∧v, u) of K. Since u∧v is a lower cover of u and by Grätzer [START_REF] Grätzer | Lattice Theory: Foundation[END_REF]Theorem 230

From now on until the end of this section we fix lattices K and L of finite length.

Lemma 9.7. The following are equivalent:

(i) K is a homomorphic image of a sublattice of L.

(ii) There exists an EA-duet (f, g) of maps from K to L.

Proof. (i)⇒(ii). By assumption, there are a sublattice H of L and a surjective homomorphism h : H K. Since L has finite length, the lower adjoint (resp., upper adjoint) f (resp., g) of h are both well-defined. By definition, they form an EA-duet.

Definition A.1. Let E be a chain and let

-a slope of (E, U ) if it is neither a peak nor a valley.

Definition A.2. Let E be a finite chain, let U ⊆ E, and let m and n be positive integers. An (m, n)-score on E with respect to U is a triple τ = ( B, A, τ ) such that:

where each B j is a subdivision of E. We call the B j the Basso subdivisions of τ and we set cvs( B) = n j=1 cvs(B j ). • A = (A 1 , . . . , A m ), where each A i is a subdivision of E. We call the A i the Alto subdivisions of τ and we set cvs( A) = m i=1 cvs(A i ). • τ : cvs( A) ∪ cvs( B) → a ∪ b, and the following conditions hold: (ScA) Let i ∈ [m] and let (x, y) ∈ cvs(A i ). Then τ (x, y) ∈ {a i } ∪ b; moreover, if (x, y) is a valley of (E, U ), then τ (x, y) = a i ; (ScB) Let j ∈ [n] and let (x, y) ∈ cvs(B j ). Then τ (x, y) ∈ {b j }∪a; moreover, if (x, y) is a peak of (E, U ), then τ (x, y) = b j ; (Comp) Let (x, y) ∈ cvs( B) and let (x , y ) ∈ cvs( A). Then (x, y) ∼ U (x , y ) (cf. Section 4) implies that τ (x, y) = τ (x , y ).

The terminology Basso and Alto follows the commonly used notation (β, α) for the pair consisting of the lower and upper adjoints of a lattice homomorphism (cf. Freese, Ježek, and Nation [START_REF] Freese | Free Lattices[END_REF]). It is also adjusted to the notation b j , a i for the atoms of B(m, n).

The following result translates the membership problem, of the lattice B(m, n) to the lattice variety generated by A U (E), in terms of certain tiling properties of the chain E. This result is not too hard to obtain via a combination of the methods of Sections 6 and 9. We do not include a proof here.

Theorem A.3. The following statements are equivalent, for all positive integers m and n and every subset U in a finite chain E:

(i) B(m, n) belongs to the lattice variety generated by A U (E).

(ii) A U (E) does not satisfy the splitting identity of B(m, n).

(iii) There exists an EA-duet of maps from B(m, n) to A U (E).

(iv) There exists an (m, n)-score on E with respect to U .

We proved in Santocanale and Wehrung [48, § 12] that B(3, 3) belongs to the lattice variety generated by A U [START_REF] Law | Some equations related to states on orthomodular lattices[END_REF], where U = {5, 6, 9, 10, 11}. The corresponding score is represented in Figure A.1. The circled vertices correspond to the elements of the chain [START_REF] Law | Some equations related to states on orthomodular lattices[END_REF], while the labels on the edges are the corresponding values of τ . The notation -→ x means that x / ∈ U , while ←x means that x ∈ U . We do not know whether all B(m, n) belong to the lattice variety generated by all permutohedra, even in the particular case where m = 4 and n = 3. (This question is also related to Section 12.2.) Equivalently, we do not know whether there are a positive integer N , a subset U of [N ], and a (4, 3)-score on [N ] with respect to U . Although the algorithm given by Büchi's Theorem certainly makes it possible to settle that question in principle (for fixed m and n), the time and space requirements of that particular assignment (m = 4 and n = 3) are far too large.