hyper-tamari: the Lean 4 developments accompanying "Evaluation orders on bracketings in the hyperoperation hierarchy"

Abstract

The Lean 4 developments accompanying the paper Evaluation orders on bracketings in the hyperoperation hierarchy by Toshihisa Urahigashi. Let H_r be the Goodstein hyperoperation hierarchy (H_1 addition, H_2 multiplication, H_3 exponentiation, H_4 tetration). For r ≥ 3 the operation is non-associative, so the value of a bracketed expression depends on the binary tree; the paper studies how that value varies over the Tamari and Stanley orders on trees. The archive contains two independent Lake projects. HyperTamari (the root of the archive) — ranks four and above, and the equality analysis at rank three: the hyperoperation and the conventions fixed in the paper, evaluation of bracketings, the Tamari rotation relation with strict increase along it from rank four, the classification of the rank-three equalities, the generalisation to arbitrary leaf labels, the strict nested bound H_r(H_r(x,y),z) < H_r(x,y+z) for r ≥ 4, x ≥ 2, y,z ≥ 1, and the Stanley covering relation with strict increase along it at every rank r ≥ 4. 156 theorems and lemmas, all audited with #print axioms: 12 depend on no axioms at all, 5 on propext, 139 on propext and Quot.sound. ChowStanley (the directory part1/) — the rank-three material: the Dyck-word and pointed-tree machinery, the local form of the Stanley covering relation, the separating test family, and the implication from the evaluation order to the Stanley order. 292 declarations: 105 depend on no axioms at all, 187 on propext and Quot.sound. In neither development does any declaration depend on Classical.choice, and there is no sorry, no sorryAx, no native_decide and no private axiom. The raw build output recording the audit is included as logs/axiom-audit.txt and part1/logs/axiom-audit.txt; scripts/check_audit.py and part1/verify.sh check it against the declarations in the sources. Both projects build with Lean 4 v4.30.0 and Mathlib v4.30.0, pinned in lean-toolchain and in the manifests. This archive is the state of the repository turahigashi/hyper-tamari at tag v1.14.0-pre, produced with git archive; the directory paper/, which holds an earlier superseded draft of the manuscript, is marked export-ignore and is therefore not included here. It remains in the repository. Large language models were used substantially in preparing both developments. For the declarations formalised here, correctness does not rest on the reliability of any model: it rests on the Lean 4 kernel, and the audit output is included. What the paper asserts outside the formalisation rests on its printed arguments and is the author's responsibility.