In their article "A Borsuk-Ulam Equivalent that Directly Implies Sperner's Lemma" (American Mathematical Monthly, April 2013), Nyman and Su write "[W]e are unaware of a direct proof that Tucker's lemma implies Sperner's lemma".
Could there be a mathematical obstruction to finding a derivation of Sperner's lemma from Tucker's lemma? E.g., could there be a mathematical context (perhaps some fragment of ZF as a background theory), and in that context two propositions S and T that are recognizable as versions of Sperner's lemma and Tucker's lemma, such that T is true but S is false? Or a computational context in which finding "Sperner's maguffin" (a fully labeled n-simplex) is demonstrably harder than finding "Tucker's maguffin" (a complementary edge)?
See the related thread In what rigorous sense are Sperner's Lemma and the Brouwer Fixed Point Theorem equivalent?.
Best Answer
Are you familiar with Christos Papadimitriou's paper "On the complexity of the parity argument and other inefficient proofs of existence"? I remember that he discusses Sperner's Lemma, but I don't recall whether Tucker is there too, and the version of the paper available at http://www.cs.berkeley.edu/~christos/papers/On%20the%20Complexity.pdf seems to be an unsearchable scan of a hard copy.