Let me just add a note about the choice if the identity 2[s]4=2[s+1]3. It's interesting to understand if other similar identities of the Goodstein h.os can be used to study other aspects of what you are doing. That identity is just one of the many arising once one fixes the base and the exponent to fixed integer values and let the rank be the variable.
Just one example: let \(h_s(n):=3+_s n\) then using the funny fact that for ranks above multiplication \(h_{s+2}(2)=h_{s+1}(3)=h_{s}h_{s+1}(2)\) holds and defining \(T(s):=h_s(2)\) we obtain \[T(s+n)=\prod_{i=-1}^{n-2}h_{s+i}\bullet T(s)\]
where the product is meant to be omega notation for outer composition. Probably this needs some fine tuning for the domain of variables and some index. It is remarkable that in this identity the ranks increase from right to left, while in most of the Goodstein iterative identities one can easily deduce the ranks increase going from left to right.
addendum 1: in the same way, by induction, one might be able to derive some iterated composition for the case\(h_s(n):=2+_s n\). Maybe using the equation \(h_{s+2}(3)=h_{s+1}(4)=h_{s}h_{s+1}(3)\). I wonder if it is possible to describe completely the class of all the equation of this kind.
addendum 2: the general case fixing the exponent to 2 is: let\(h_{b,s}(n):=b+_s n\) and define \(T_b(s):=h_{b,s}(2)\). Use this notation to rewrite and use the identity \(h_{b,s+2}(2)=h_{b,s+1}(b)=h_{b,s}^{b-2}h_{b,s+1}(2)\) as \[T_b(s+2)=h_{b,s}^{b-2}T_b(s+1)\] and obtain
\[T_b(s+n)=\prod_{i=-1}^{n-2}h^{b-2}_{b,s+i}\bullet T_b(s)\]
Obviously, If I'm able to follow your methods a lil bit, you could use these kind of eqs. for ranks near the integers, something like \(s\in \bigcup_{n\in\mathbb N} [n-\epsilon,n+\epsilon]\).
addendum 3: we can look the previous recursion also in the other direction: define \({\bf A}_b(s):=h_{b,s}(b)\) and rewrite the previous recursion as \({\bf A}_b(s+1)=h_{b,s}^{b-2}h_{b,s+1}(2)=h_{b,s}^{b-2}{\bf A}_b(s)\) obtaining
\[{\bf A}_b(s+n)=\prod_{i=0}^{n-1}h^{b-2}_{b,s+i}\bullet {\bf A}_b(s)\]
addendum 4: the case \(h_{b,s+1}(3)=h_{b,s}(4)\) works only for \(b=2\) and seems much more difficult to generalize. First of all it doesn't belong to the previous family of iterated composition even if it is very similar in its form. Define \(E(s):=h_{s}(3)=2+_s3\) then \(E(s+2)=h_{s+1}(4)=h_s(E(s+1))\) and \[E(s+n)=\prod_{i=-1}^{n-2}h_{s+i}\bullet E(s)\]
Just one example: let \(h_s(n):=3+_s n\) then using the funny fact that for ranks above multiplication \(h_{s+2}(2)=h_{s+1}(3)=h_{s}h_{s+1}(2)\) holds and defining \(T(s):=h_s(2)\) we obtain \[T(s+n)=\prod_{i=-1}^{n-2}h_{s+i}\bullet T(s)\]
where the product is meant to be omega notation for outer composition. Probably this needs some fine tuning for the domain of variables and some index. It is remarkable that in this identity the ranks increase from right to left, while in most of the Goodstein iterative identities one can easily deduce the ranks increase going from left to right.
addendum 1: in the same way, by induction, one might be able to derive some iterated composition for the case\(h_s(n):=2+_s n\). Maybe using the equation \(h_{s+2}(3)=h_{s+1}(4)=h_{s}h_{s+1}(3)\). I wonder if it is possible to describe completely the class of all the equation of this kind.
addendum 2: the general case fixing the exponent to 2 is: let\(h_{b,s}(n):=b+_s n\) and define \(T_b(s):=h_{b,s}(2)\). Use this notation to rewrite and use the identity \(h_{b,s+2}(2)=h_{b,s+1}(b)=h_{b,s}^{b-2}h_{b,s+1}(2)\) as \[T_b(s+2)=h_{b,s}^{b-2}T_b(s+1)\] and obtain
\[T_b(s+n)=\prod_{i=-1}^{n-2}h^{b-2}_{b,s+i}\bullet T_b(s)\]
Obviously, If I'm able to follow your methods a lil bit, you could use these kind of eqs. for ranks near the integers, something like \(s\in \bigcup_{n\in\mathbb N} [n-\epsilon,n+\epsilon]\).
addendum 3: we can look the previous recursion also in the other direction: define \({\bf A}_b(s):=h_{b,s}(b)\) and rewrite the previous recursion as \({\bf A}_b(s+1)=h_{b,s}^{b-2}h_{b,s+1}(2)=h_{b,s}^{b-2}{\bf A}_b(s)\) obtaining
\[{\bf A}_b(s+n)=\prod_{i=0}^{n-1}h^{b-2}_{b,s+i}\bullet {\bf A}_b(s)\]
addendum 4: the case \(h_{b,s+1}(3)=h_{b,s}(4)\) works only for \(b=2\) and seems much more difficult to generalize. First of all it doesn't belong to the previous family of iterated composition even if it is very similar in its form. Define \(E(s):=h_{s}(3)=2+_s3\) then \(E(s+2)=h_{s+1}(4)=h_s(E(s+1))\) and \[E(s+n)=\prod_{i=-1}^{n-2}h_{s+i}\bullet E(s)\]
Mother Law \(\sigma^+\circ 0=\sigma \circ \sigma^+ \)
\({\rm Grp}_{\rm pt} ({\rm RK}J,G)\cong \mathbb N{\rm Set}_{\rm pt} (J, \Sigma^G)\)