Proposition 43, p. 29 — B(C, r) has Natarajan dimension ≥ 2 iff C has a square with r(v₀) = r(v₂), r(v₁) = r(v₃)

Proved

MulticlassDS.NatGap.prop43_natarajan_square

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

natarajan-dimensionp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1pseudo-cubesimplicial-complex

Let $C$ be a $d$ -dimensional good complex over $V$ , let $r$ be a proper coloring of $C$ , and let $B = B(C, r) \subseteq V^{d+1}$ be the pseudo-cube defined by $C$ and $r$ . The following are equivalent:

there is a square $v_0 \to v_1 \to v_2 \to v_3 \to v_0$ in $C$ with $r(v_0) = r(v_2)$ and $r(v_1) = r(v_3)$ ;
the Natarajan dimension of $B$ , viewed as a class of functions $[d+1] \to V$ , is at least $2$ :

d_N(B) \ge 2 .

This translates the Natarajan dimension of a pseudo-cube into a local combinatorial property of the complex.

Formalization Note $B$ is a class over the domain Fin (d + 1) with labels in $V$ , and $d_N(B)$ is the shared $\mathbb N_\infty$ -valued Natarajan dimension.

Preamble

import Mathlib
import Definitions.Def_MulticlassDS_NatGap_Dimensions
import Definitions.Def_MulticlassDS_NatGap_Complexes

Formal statement

namespace MulticlassDS.NatGap

theorem prop43_natarajan_square {V : Type*} (C : Set (Finset V)) (d : ℕ)
    (hC : IsGood C d) (r : V → Fin (d + 1)) (hr : IsProperColoring C d r) :
    (∃ v₀ v₁ v₂ v₃ : V, IsSquare C v₀ v₁ v₂ v₃ ∧ r v₀ = r v₂ ∧ r v₁ = r v₃) ↔
      2 ≤ natarajanDim (pseudoCubeOf C d r) := by sorry

end MulticlassDS.NatGap

Source

Brukhim, Carmon, Dinur, Moran, Yehudayoff, A Characterization of Multiclass Learnability, arXiv:2203.01550v1, p. 29, Proposition 43

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