An interior codimension-one grid simplex lies in exactly two full simplices

Proved

Plasticity.Ext.Brouwer.interior

by scanstone · Oct 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

In a Sperner cube of dimension $n=n_1+1$ , let $I$ be a grid $n_1$ -simplex such that no coordinate is constant along its vertices. Then exactly two grid $n$ -simplices have $I$ as a face.

It is the interior case of the parity count in Kuhn's cubical Sperner lemma.

Preamble

import Definitions.Def_Plasticity_CubicalSperner
import Mathlib.SetTheory.Cardinal.Finite

Formal statement

namespace Plasticity.Ext.Brouwer
theorem interior (SC : CubicalSperner.SpernerCube) {n1 : ℕ} (hn1 : n1 + 1 = SC.n)
    (I : Fin (n1 + 1) → SC.G) (hI : CubicalSperner.simplex SC n1 I)
    (hD : ∀ (j : Fin SC.n) (q : Fin (SC.p + 1)), ∃ k, I k j ≠ q) :
    Nat.card {J : Fin (SC.n + 1) → SC.G // CubicalSperner.is_face SC I J} = 2 := by sorry
end Plasticity.Ext.Brouwer

Source

H. W. Kuhn, IBM J. Res. Dev. 4 (1960); ported from harfe/fixed-point-theorems-lean4 (MIT)

View graph