Π⁰₄ conservation of the Ordered Variable Word theorem

A left-variable word over an alphabet~A is a word over~A ∪ \\ whose first letter is the distinguished symbol~ standing for a placeholder. The Ordered Variable Word theorem (OVW), 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₀ and an infinite sequence of left-variable words w₁, w₂, such that \ c₀ · w₁[a₁] · · wₖ[aₖ] : k ∈ N, a₁, , aₖ ∈ A \ is monochromatic. In this article, we prove that OVW is Π⁰₄-conservative over~RCA₀ + BΣ⁰₂. This implies in particular that OVW does not imply ACA₀ over~RCA₀. This is the first principle for which the only known separation from~ACA₀ involves non-standard models.