Proposition 42 (⇒), p. 28 — a d-dimensional good complex C with a proper coloring r gives a (d+1)-dimensional pseudo-cube B(C, r)

Proved

MulticlassDS.NatGap.prop42_good_complex_pseudo_cube

by mikedeng1 · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

good-complexp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1pseudo-cubesimplicial-complex

Let $C$ be a $d$ -dimensional good simplicial complex over a vertex set $V$ and let $r : V \to [d+1]$ be a proper coloring of $C$ . Then the class

B(C, r) = \big\{(v_1, \dots, v_{d+1}) \in V^{d+1} : \{v_1,\dots,v_{d+1}\} \in C,\ r(v_i) = i \text{ for all } i\big\}

is a $(d+1)$ -dimensional pseudo-cube.

This is the first half of the equivalence between pseudo-cubes and good complexes: properties of complexes (finiteness, replacement) become the defining properties of a pseudo-cube (finiteness, neighbours in every direction).

Formalization Note The statement is about the explicit class $B(C,r)$ the proof constructs (the paper's Remark after Proposition 42). Replacement is the version with a new vertex $u \notin f$ ; see the definitions item.

Preamble

import Mathlib
import Definitions.Def_MulticlassDS_NatGap_Dimensions
import Definitions.Def_MulticlassDS_NatGap_Complexes

Formal statement

namespace MulticlassDS.NatGap

theorem prop42_good_complex_pseudo_cube {V : Type*} (C : Set (Finset V)) (d : ℕ)
    (hC : IsGood C d) (r : V → Fin (d + 1)) (hr : IsProperColoring C d r) :
    IsPseudoCube (pseudoCubeOf C d r) := by sorry

end MulticlassDS.NatGap

Source

Brukhim, Carmon, Dinur, Moran, Yehudayoff, A Characterization of Multiclass Learnability, arXiv:2203.01550v1, p. 28, Proposition 42, first sentence (good complex ⟹ pseudo-cube)

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph