Your understanding of the point of the theorem is very different to mine, and I'm moderately sure my understanding is pretty close to correct.
It is a fact of mathematics that there are some statements which are solely about finite objects, but to prove them requires reasoning about an infinite object. For a more accessible example than TREE, I think the Ackermann function falls into this category. The Ackermann function A(n+1, m+1) = A(n, A(n+1, m)) is well-defined for all n and m (we prove this by induction over NxN), but the proof relies on considering the lexicographic order on NxN which is inherently infinite. (I'm not totally certain that all proofs of Ackermann's well-definedness rely on an infinite object, but the only proof known to me does.) Ackermann's function itself is in some sense a "finite" object, but the proof of its well-definedness is in some sense "infinite". Whatever the status of my conjecture that "you can't prove that Ackermann's function is well-defined without considering an infinite object", it is certainly a fact that Ackermann is not primitive-recursive, and "primitive-recursive functions" corresponds to the lowest level of the five "mysterious levels" the article talks about.
So the analogy is as follows. Imagine that we knew of this "infinitary" proof that Ackermann is well-defined, but we hadn't proved that no "finitary" proof exists. (So finitists are not happy to use Ackermann, because it might not actually be well-defined according to them: any known proof requires dealing with an infinite object.) Now, this paper comes along and proves that actually a finitary proof exists. Suddenly the finitists are happy to use the Ackermann function.
The actual definition of TREE is a bit too long for me to explain here, but it is an example of a function like Ackermann, which is well-defined, but in fact if you're not allowed to consider infinite objects during the proof then it is provably impossible to prove that TREE is well-defined. So the statement "TREE is well-defined" is, in some sense, "less constructive" or "more infinitary" than R_2^2.
It is a fact of mathematics that there are some statements which are solely about finite objects, but to prove them requires reasoning about an infinite object. For a more accessible example than TREE, I think the Ackermann function falls into this category. The Ackermann function A(n+1, m+1) = A(n, A(n+1, m)) is well-defined for all n and m (we prove this by induction over NxN), but the proof relies on considering the lexicographic order on NxN which is inherently infinite. (I'm not totally certain that all proofs of Ackermann's well-definedness rely on an infinite object, but the only proof known to me does.) Ackermann's function itself is in some sense a "finite" object, but the proof of its well-definedness is in some sense "infinite". Whatever the status of my conjecture that "you can't prove that Ackermann's function is well-defined without considering an infinite object", it is certainly a fact that Ackermann is not primitive-recursive, and "primitive-recursive functions" corresponds to the lowest level of the five "mysterious levels" the article talks about.
So the analogy is as follows. Imagine that we knew of this "infinitary" proof that Ackermann is well-defined, but we hadn't proved that no "finitary" proof exists. (So finitists are not happy to use Ackermann, because it might not actually be well-defined according to them: any known proof requires dealing with an infinite object.) Now, this paper comes along and proves that actually a finitary proof exists. Suddenly the finitists are happy to use the Ackermann function.
The actual definition of TREE is a bit too long for me to explain here, but it is an example of a function like Ackermann, which is well-defined, but in fact if you're not allowed to consider infinite objects during the proof then it is provably impossible to prove that TREE is well-defined. So the statement "TREE is well-defined" is, in some sense, "less constructive" or "more infinitary" than R_2^2.