Largeness notions and polytime translation for $\mathrm{\forall }{\mathrm{\Sigma }}_3^0$-consequences of ${\mathsf{R}\mathsf{T}}_2^2$

Le Houérou, Patey and Yokoyama defined a parameterized version of $\alpha$-largeness to prove that ${\mathsf{W}\mathsf{K}\mathsf{L}}_0+{\mathsf{R}\mathsf{T}}_2^2$ is a $\mathrm{\forall }{\mathrm{\Sigma }}_3^0$-conservative extension of ${\mathsf{R}\mathsf{C}\mathsf{A}}_0+\mathsf{B}{\mathrm{\Sigma }}_2^0$, where $\mathrm{\forall }{\mathrm{\Sigma }}_3^0$ is the universal set-closure of the class of ${\mathrm{\Sigma }}_3^0$-formulas. We introduce a variant of this notion of largeness and obtain polynomial bounds, using a tree partition theorem based on Milliken’s tree theorem. Thanks to the framework of forcing interpretation, this yields that any proof of a $\mathrm{\forall }{\mathrm{\Sigma }}_3^0$-sentence in the theory ${\mathsf{W}\mathsf{K}\mathsf{L}}_0+{\mathsf{R}\mathsf{T}}_2^2$ can be translated into a proof in ${\mathsf{R}\mathsf{C}\mathsf{A}}_0+\mathsf{B}{\mathrm{\Sigma }}_2^0$ at the cost of a polynomial increase in size.