Sperner Fixed-Point Certificate

Worked Example

Let's verify Sperner's Lemma for a standard 2-simplex with subdivision 3 and the Cyclic map F = (b1, b2, b0).

The main simplex is defined by barycentric coordinates b0 + b1 + b2 = 1. We evaluate the differences b_i - F_i at the vertices:

1. Consider vertex at (0.333, 0.333, 0.333) (center, although vertices for subdivision 3 are of the form i/3, j/3, k/3). Let's pick a specific vertex (1/3, 0, 2/3). Here b0 = 0.333, b1 = 0, b2 = 0.667.
2. Under the Cyclic map F = (b1, b2, b0), we have F = (0, 0.667, 0.333).
3. Calculate the differences b_i - F_i:
   • b0 - F0 = 0.333 - 0 = 0.333
   • b1 - F1 = 0 - 0.667 = -0.667
   • b2 - F2 = 0.667 - 0.333 = 0.333
4. The maximum positive difference occurs at indices 0 and 2. Under the tie-breaking and Sperner boundary condition (since b1 = 0 forbids label 1), the smallest index maximizing the positive difference is selected, assigning label 0.
5. Running this logic across all 10 vertices yields exactly 1 fully labeled small triangle with labels 0, 1, and 2.
6. The barycenter of this fully labeled triangle (the lexicographical first witness) is calculated as:
   Witness b0: 0.1111111111111111
   Witness b1: 0.4444444444444444
   Witness b2: 0.4444444444444444
7. This cell localizes the true fixed point (0.333, 0.333, 0.333), giving a maximum residual 0.3333333333333333 against the fixed point.

Experiment

To explore the relationship between the subdivision size and the localization accuracy, interact with the Sperner Fixed-Point Certificate module:

1. Set the Subdivision to 3 and Map to Cyclic. Observe that there are 10 vertices and 1 fully labeled triangle.
2. Change the Subdivision to 4. Notice the number of fully labeled triangles remains 1 (Odd parity), and the witness barycenter lands at (1/3, 1/3, 1/3) with residual 0.
3. Switch the Map to Swap first two and observe how the coloring and labels change along the edges, but Sperner's parity remains Odd.

Limitations

Sperner's Lemma guarantees a fully labeled cell that localizes a fixed point, but the barycenter of this cell need not be exactly the fixed point (unless the subdivision grid happens to place the fixed point precisely on a barycenter). The method requires computational subdivision—scaling exponentially with dimension—so while visually effective in 2D, it is generally impractical as a numerical solver for high-dimensional Brouwer fixed points. Furthermore, floating-point residuals can appear as non-zero for algebraically precise fixed points if exact arithmetic is not used.

References

For a comprehensive introduction to Sperner's Lemma, simplicial subdivisions, and its applications to Brouwer's Fixed-Point Theorem, see:

• Sperner's Lemma and Brouwer's Fixed Point Theorem - Detailed mathematical lecture notes on the combinatorial triangulation rules.