# 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?.

-
Since these are results in finite combinatorics, the right context would be the theories discussed by Steve Cook and Phuong Nguyen in their book Logical Foundations of Proof Complexity. –  François G. Dorais May 22 '13 at 20:57
Please can we clarify, for this and the other question, what the statement of Sperner's Lemma is that is under discussion. Is the Wikipedia article clear enough? en.wikipedia.org/wiki/Sperner_lemma –  Paul Taylor May 22 '13 at 21:34
@Paul Taylor: See willamette.edu/~knyman/papers/Fan_Sperner.pdf for clear statements of Sperner's lemma and Tucker's lemma. –  James Propp May 23 '13 at 14:13
Have you seen this? arxiv.org/pdf/1305.6158.pdf –  domotorp Jun 7 '13 at 14:29
@domotorp: Thanks for pointing out this article! It was very relevant and interesting. –  James Propp Jun 14 '13 at 16:51

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.

-
Indeed, I don't think that Tucker has been studied in the context of PPAD complexity. It has been of some interest to me if Borsuk-Ulam is part of this class of path following proofs that Papadimitriou introduced. –  Rabee Tourky Jun 7 '13 at 8:42
Both Borsuk-Ulam and Tucker have been studied and shown to be PPAD-complete in the linked paper. I also believe that this shows that Sperner can be derived from Tucker, however, it would be nice to have a simple, straightforward reduction. –  domotorp Jun 7 '13 at 10:10