Finite bottom-up tree-automaton acceptance has one uniform implementation on the Lax word RAM. The program is chosen before the automaton, tree, and word width. Its actual machine instruction count is bounded by a fixed constant times a quadratic function of the automaton workload and a linear function of the number of tree nodes. The workload is the certified constructor size plus the largest symbol rank; the latter is relevant because a node may have that many ordered children even though a rank is one primitive natural payload.

The only physical input admitted by the theorem is the distinguished constructor-certified $lax-58$ arena input. Lax560851's reusable complexity predicate supplies the program quantifier and requires correctness at every word width satisfying payload, arena-address, and implementation-capacity bounds. The natural output is one word: zero for rejection and one for acceptance.