A codimension-one grid simplex lies in one or two full simplices

Proved

Plasticity.Ext.Brouwer.parent_count

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. If some coordinate is constantly $0$ or constantly $p$ along its vertices, exactly one grid $n$ -simplex has $I$ as a face; otherwise exactly two do.

This is the door-counting step of Kuhn's cubical Sperner lemma.

Preamble

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

Formal statement

namespace Plasticity.Ext.Brouwer
theorem parent_count (SC : CubicalSperner.SpernerCube) {n1 : ℕ} (hn1 : n1 + 1 = SC.n)
    (I : Fin (n1 + 1) → SC.G) (hI : CubicalSperner.simplex SC n1 I) :
    (((∃ j, ∀ k, I k j = 0) ∨ (∃ j, ∀ k, I k j = Fin.last SC.p)) →
      Nat.card {J : Fin (SC.n + 1) → SC.G // CubicalSperner.is_face SC I J} = 1) ∧
    (¬((∃ j, ∀ k, I k j = 0) ∨ (∃ j, ∀ k, I k j = Fin.last SC.p)) →
      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