Is the order on repeated exponentiation the Dyck order?

EDIT: I can complete half of the proof, showing that the magma order refines the Dyck order.

---

Following Martin Rubey's comment, there is a standard bijection between association orders and Dyck paths that uses reverse Polish notation (RPN). For $n=3$, the five association orders, when written in RPN, are

a b c d ^ ^ ^
a b c ^ d ^ ^
a b ^ c d ^ ^
a b c ^ ^ d ^
a b ^ c ^ d ^

If we ignore the initial a and interpret letters as up strokes and carets as down strokes then we get Dyck paths. The Dyck order is generated by the operation "replace x ^ with ^ x" (where x is any letter). So proving your claim reduces to showing that

1. if you replace x ^ with ^ x then the value of the entire expression decreases, for all choices of values (from $\mathbb{N}_{\ge2}$) of the variables; and

2. if you have a pair of RPN expressions such that you cannot get from one to the other by a sequence of such replacements, then you can get either expression to be larger than the other by suitably choosing values (from $\mathbb{N}_{\ge2}$) for the variables.

To prove part 1, note first that in a fixed RPN expression, weakly increasing the value of any variable causes the overall value to weakly increase, by the ordered magma property.

Now consider two valid RPN expressions $\alpha$ and $\beta$ that differ only in that at one point, $\alpha$ has x ^ while $\beta$ has ^ x. Just after completing this part of the calculation, stack $\alpha$ will have $A,B^C$ on top while stack $\beta$ will have $A^B,C$ on top, for some $A$, $B$, and $C$ in $\mathbb{N}_{\ge2}$. If we continue the calculation until just before the first caret that affects $A$ in stack $\alpha$ (equivalently, until the first caret that affects $A^B$ in stack $\beta$), then the top of stack $\alpha$ will look like $A, B^{CD}$ (followed by a caret) while the top of stack $\beta$ will look like $A^B, C^D$ (followed by a caret) for some $D$ (possibly equal to 1, in the case where said caret shows up immediately). Applying the caret then yields $A^{B^{CD}}$ on stack $\alpha$ and $A^{BC^D}$ on stack $\beta$. But $B^{CD} = (B^C)^D \ge (BC)^D \ge (B^{1/D}C)^D = BC^D$ for all $B, C \in\mathbb{N}_{\ge2}$ and $D\ge1$. So the value on stack $\alpha$ at this stage is $\ge$ the value on stack $\beta$. Since the remainder of the computation is the same for both stacks, the eventual value of $\alpha$ will be $\ge$ the eventual value of $\beta$.

It seems very likely to me that we can prove part 2 by finding a place $P$ where Dyck path 1 exceeds Dyck path 2 and another place $Q$ where Dyck path 2 exceeds Dyck path 1, and inserting an extremely large number at one of these points to force whichever expression we want to be larger. But I haven't quite figured out how to say this rigorously.

(This is what I have written just before my wife killed the internet connection 12 hours ago before she went to bed. I only show that $D\leq E \Rightarrow A\leq B$ where $D$ and $E$ are Dyck paths and $A$ and $B$ the corresponding binary trees. I didn't look at Timothy's answer yet, but I am guessing it's the same.)

Indeed, the bijection between (ordered, full) binary trees (with leaves labelled $a,b,c,\dots$ from left to right) and Dyck paths (traversing the binary tree starting at the root, first traversing the right subtree, and writing an up step for a right branch and a down step for a left branch) induces an order preserving map between the Stanley lattice and the exponential evaluation order.

A path $D$ is covered by a path $E$ in the Stanley lattice, if and only if a peak in $D$ is converted to a valley in $E$, all other steps remaining the same.

In terms of binary trees, a peak in the Dyck path corresponds to a pair of siblings where the right sibling $x$ does not have further children and there is a left branch somewhere after $x$, in the order the tree is traversed.

To see what the covering relation in the Stanley lattice corresponds to, we first do an easy special case:

Suppose that, in the binary tree $B$ corresponding to the Dyck path $E$, the parent $y$ of $x$ is a right child.

Let $L_1$ be the subtree rooted at the sibling of $x$, and let $L_2$ be the subtree rooted at the sibling of $y$. The magma expression corresponding to the subtree rooted at the parent of $y$ is $L_2 (L_1 x)$.

Then the binary tree $A$ corresponding to $D$ is obtained from $B$ by replacing the subtree rooted at the parent of $y$ with the binary tree corresponding to the magma expression $(L_2 L_1) x$, which is smaller than $L_2 (L_1 x)$.

The general case is only superficially more complicated:

Suppose that, in the binary tree $B$ corresponding to the Dyck path $E$, there is a (maximal) path of $k$ left branches from a node $y$ to the parent of $x$, with (right) siblings having subtrees $D_1,D_2,\dots,D_k$. Let $L_1$ be the subtree rooted at the (left) sibling of $x$ and $L_2$ be the subtree rooted at the (left) sibling of $y$. The magma expression corresponding to the subtree rooted at the parent of $y$ is $$L_2(\cdots((L_1 x)R_1)\cdots R_k).$$

Then the binary tree $A$ corresponding to $D$ is obtained from $B$ by replacing the subtree rooted at the parent of $y$ with the binary tree corresponding to the magma expression $$(L_2 L_1)(x (R_1(\cdots R_k))).$$

Setting $R=R_1\cdots R_k$, it remains to check that $L_2^{(L_1^{xR})} \geq (L_2^{L_1})^{(x^R)}$.