Slow well-ordering below epsilon zero ($\forall k\exists N\forall ({\alpha }_i{)}_{i<N}(\Vert {\alpha }_i\Vert \le k+i\Rightarrow \exists i<j{\alpha }_i\le {\alpha }_j)$)

Use the unary Cantor normal form tree norm, counting one root and recursively counting all repeated exponent subterms. There are only finitely many notations of bounded norm. This finite principle bounds all descending sequences whose norms grow at most linearly with the position. Friedman's finite form of Kruskal's theorem implies it through the natural-sum ordinal rank of a finite rooted tree. The Friedman–Smith miniaturization theorem turns this controlled termination principle for standard epsilon-zero notations into the formal consistency statement for Peano arithmetic; the technical ordinal-analysis result is needed in addition to the tree coding. Section 2.2 of formal.hknu.ac.kr/Publi/kruskalJKMS.pdf records the general miniaturization and soundness theorem.