Sperner's lemma and Tucker's lemma 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?.
 A: Hello, I'm one of the authors of this paper: arXiv:1305.6158 (PDF)
The way I see it, "Sperner's Lemma", as usually stated, is actually the "wrong" version of the theorem.  The versions in my paper, which use cubic and octahedral labels, are in some sense, the more "natural" statements, at least as far as analogy with Tucker goes.  As we show, they are implied by Tucker's lemma quite naturally via geometric embeddings.
Topologically, the various Sperner-like theorems are obviously the same.  But it seems that you need a topological theorem (e.g. Brouwer) to establish their equivalence.  For the same reason, it seems like you need a topological theorem to prove Sperner from Tucker.  At the very least, the geometric approach doesn't make any sense, because the antipodality condition doesn't have a good analogy.
As for your question about mathematical contexts where T is True and S is false, I can't think of any context where that would really make sense.  Maybe T can be provable and S can be unprovable, e.g. if you restricted yourself to a context where Brouwer, etc. can't be proven (maybe by accepting only axioms that yield constructive proofs).
A: 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.
