Monsky's theorem, again

[Timothy Y. Chow]

A few weeks ago, I asked what is needed to prove Monsky's theorem.

https://cs.nyu.edu/pipermail/fom/2022-September/023579.html

I did not receive any responses, so I tried asking on MathOverflow.

https://mathoverflow.net/questions/432265/is-monskys-theorem-provable-in-mathsfrca-0

This time, Qiaochu Yuan and Francois Dorais made some useful comments, but 
stopped short of a complete answer to the question.  Perhaps some FOM 
readers can pick up where they left off.

As a quick summary, Qiaochu Yuan gave an argument that the existence of a 
dissection of the desired type is equivalent to a first-order statement in 
the language of real-closed fields, so if there is such a thing at all, 
then it can be realized using only algebraic numbers.  However, it's not 
clear whether this argument can be carried out on the basis of RCA_0 
alone.

Francois Dorais gave a sketch of a possible argument that Monsky's theorem 
is provable in RCA_0, but there are many details in the sketch that are, 
well, sketchy.

Tim