Evaluation orders on bracketings in the hyperoperation hierarchy

Let Hr be the Goodstein hyperoperation hierarchy, so that H3 is exponentiation and H4 tetration. For r ≥ 3 the operation is not associative, so the value of Hr(a1, …, an) depends on the bracketing, that is on a binary tree with n leaves. Write T ≤ev U when evr(T) ≤ evr(U) for every assignment of leaf values ≥ 2, and let ≤St be the Stanley order on those trees, which extends the Tamari order. At rank 3 we determine ≤ev completely: it is the Stanley order. The inclusion ≤St ⊆ ≤ev is due to Chow; we prove its converse, which he left open, constructively and with a bound. If T ≰St U then a single leaf separates them, and the value to put there is written down in advance as M = 2K2, where K is a product of subtree values read off from U. One family of n − 2 assignments, given in closed form, therefore decides the entire order. For every r ≥ 4 we prove that ≤St ⊆ ≤ev, the value increasing strictly along every Stanley cover; the semi-associative law that underlies this is not new, and we say where it is already stated. Equality in that law is settled by one statement covering every rank and every boundary case. The device throughout is the vector of right depths of the leaves. Much of the paper is machine-checked in Lean 4, and it is explicit about what is not. This is a preprint (33 pages; LaTeX source included). It has not been refereed. Use of AI-assisted tools. Generative AI tools (large language models) were used to find the proofs, and also for the computations, the formalisation and the writing. The author directed the work, reviewed and verified the resulting mathematical arguments, and takes full responsibility for the manuscript. The Lean 4 developments that accompany the paper are archived separately: version DOI 10.5281/zenodo.22789946 (tag v1.15.0-pre, the version the paper describes), concept DOI 10.5281/zenodo.22779441. The two files of this deposit are paper/hyper-tamari.tex and paper/hyper-tamari.pdf at commit 77989d1 of github.com/turahigashi/hyper-tamari, and are licensed under CC BY 4.0.