${\mathrm{\Pi }}_4^0$ conservation of the Ordered Variable Word theorem

A left-variable word over an alphabet~$A$ is a word over~$A\cup \{\star \}$ whose first letter is the distinguished symbol~$\star$ standing for a placeholder. The Ordered Variable Word theorem ($\mathsf{O}\mathsf{V}\mathsf{W}$), also known as Carlson-Simpson’s theorem, is a tree partition theorem, stating that for every finite alphabet~$A$ and every finite coloring of the words over~$A$, there exists a word $c_0$ and an infinite sequence of left-variable words $w_1,w_2,\dots$ such that $\{c_0\cdot w_1[a_1]\cdot \cdots \cdot w_k[a_k]:k\in \mathbb{N},a_1,\dots ,a_k\in A\}$ is monochromatic. In this article, we prove that $\mathsf{O}\mathsf{V}\mathsf{W}$ is ${\mathrm{\Pi }}_4^0$-conservative over~${\mathsf{R}\mathsf{C}\mathsf{A}}_0+\mathsf{B}{\mathrm{\Sigma }}_2^0$. This implies in particular that $\mathsf{O}\mathsf{V}\mathsf{W}$ does not imply ${\mathsf{A}\mathsf{C}\mathsf{A}}_0$ over~${\mathsf{R}\mathsf{C}\mathsf{A}}_0$. This is the first principle for which the only known separation from~${\mathsf{A}\mathsf{C}\mathsf{A}}_0$ involves non-standard models.