I never said the triangles in the standard proof are going to be nested, so your whole segue into reverse mathematics is, just like I said, irrelevant. The point of the argument is that you can find a sequence of triangles with differently colored vertices, the vertices of which all converge to the same point (thanks to compactness), which contradicts continuity of the retraction on the boundary. The nonstandard version of this is exactly the same argument, it just replaces the explicit limiting step that contradicts continuity with the an argument that uses the nonstandard formulation of continuity in terms of infinitesimals.
If that makes it easier for you to understand it, in the standard proof, you also color every point of the rectangle, with the color of the edge it retracts to (picking the colors of the vertices of the big triangle arbitrarily, just making sure that the color of each vertex is a color of one of the edges it belongs to, not one of the opposite edges). Then, an easy argument from continuity shows that no interior point will have points of three different colors arbitrarily close to it. Finally, applying Sperner's lemma as above proves that such point must nevertheless exist, obtaining contradiction with the existence of the retraction.
and then treated Sperner as an additional ingredient even though the coloring step in Nelson's proof is already the corresponding Sperner argument.
I don't understand what are you saying here. What I'm saying is that for the coloring proof of BFPT to work, whether clothed in standard or nonstandard language, you must perform a combinatorial argument that uses a topology of a triangle as a necessary ingredient, similar in shape to the proof of Sperner's lemma.
If that makes it easier for you to understand it, in the standard proof, you also color every point of the rectangle, with the color of the edge it retracts to (picking the colors of the vertices of the big triangle arbitrarily, just making sure that the color of each vertex is a color of one of the edges it belongs to, not one of the opposite edges). Then, an easy argument from continuity shows that no interior point will have points of three different colors arbitrarily close to it. Finally, applying Sperner's lemma as above proves that such point must nevertheless exist, obtaining contradiction with the existence of the retraction.
and then treated Sperner as an additional ingredient even though the coloring step in Nelson's proof is already the corresponding Sperner argument.
I don't understand what are you saying here. What I'm saying is that for the coloring proof of BFPT to work, whether clothed in standard or nonstandard language, you must perform a combinatorial argument that uses a topology of a triangle as a necessary ingredient, similar in shape to the proof of Sperner's lemma.