Is Monsky's theorem provable in $\mathsf{RCA}_0$?

Question

Monsky's theorem states that it is not possible to dissect a square into an odd number of triangles of equal area. Monsky's proof attracted attention in part because it unexpectedly made use of the fact that the 2-adic valuation on $\mathbb{Q}$ can be extended to $\mathbb{R}$. There is no canonical way to extend the 2-adic valuation to transcendental extensions of $\mathbb{Q}$, so this step of the proof has a highly arbitrary and nonconstructive feel to it. Most people would not expect that such non-canonical choices would be necessary to prove something as concrete as Monsky's theorem. (Occasionally someone will even ask whether Monsky's proof makes essential use of the axiom of choice, but the answer is no.)

The aforementioned "nonconstructive feel" leads me to ask the following question. In the language of Subsystems of Second-Order Arithmetic, can Monsky's theorem be proved in $\mathsf{RCA}_0$? A potential sticking point might be the existence of transcendence bases, which is something that doesn't kick in until the $\mathsf{ACA}_0$ level. So for example, if we're handed some candidate vertices with coordinates that involve (say) the numbers $e$ and $\pi$, then we have no effective way to determine whether $e$ and $\pi$ are algebraically independent. But maybe we don't really need transcendence bases per se. Since we're using classical logic, perhaps we can split into two cases, according to whether $e$ and $\pi$ are algebraically dependent or not, and argue that the desired conclusion follows in either case?

Answer 1

This isn't an answer to your question because I have no idea whether this argument can be carried out in $RCA_0$, but this fact doesn't appear to be mentioned anywhere easily accessible through googling about Monsky's theorem so it seems good to document it somewhere (assuming I didn't make a mistake!). We can say the following (unless I am horribly mistaken about something!):

Claim 1: A system of polynomial equations $P_1(x_1, \dots x_n) = \dots = P_k(x_1, \dots x_n)$ over $\mathbb{Q}$ has a solution over $\mathbb{R}$ iff it has a solution over the real algebraic numbers $\mathbb{R} \cap \overline{\mathbb{Q}}$.

Claim 2: For a fixed positive integer $k$, Monsky's theorem for subdivisions into $2k+1$ triangles is equivalent to the statement that no member of a specific finite set of systems of polynomial equations has a solution over $\mathbb{R}$.

The upshot is that Monsky's theorem is true over $\mathbb{R}$ iff it's true over $\mathbb{R} \cap \overline{\mathbb{Q}}$, and hence that we only need to extend the $2$-adic valuation to the finite extension of $\mathbb{Q}$ generated by the coordinates of a potential algebraic counterexample, which is just a number field $K$. And this can be done with no shenanigans whatsoever, since it suffices to choose a prime ideal of $\mathcal{O}_K$ lying over $(2)$. So there is no need, as far as I can tell, to consider even a single transcendental number in the argument.

Claim 1 follows from the fact that $\mathbb{R}$ is elementary equivalent to any real closed field but I believe it should also have a more elementary proof using elimination theory; hopefully someone else can fill in the details and say what exactly is needed in the proof.

Claim 2 is the usual reduction of Euclidean geometry to the theory of real closed fields: an equal-area dissection of the unit square into $2k+1$ triangles consists of the coordinates of a finite collection of points together with one of a finite set of finitely many assertions that these points 1) lie inside the unit square, and 2) define triangles with area $\frac{1}{2k+1}$ (we may want to draw different lines between the points to define different sets of triangles but for $k$ fixed there are only finitely many possible configurations). A real number $x$ lies in $[0, 1]$ iff $\exists y_1 : x = y_1^2$ and $\exists y_2 : 1 - x = y_2^2$, and the area of a triangle is a quadratic polynomial in the coordinates of its vertices, so the conclusion is that for fixed $k$ the existence of an equal-area dissection into $2k+1$ triangles is equivalent to the existence of a solution to one of a finite set of systems of quadratic polynomials.