Corollary 44, p. 29 — no empty squares in a good complex C gives d_N(B(C, r)) ≤ 1 for every proper coloring r

Proved

MulticlassDS.NatGap.cor44_no_empty_square_natarajan_le_one

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

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

Let $C$ be a good simplicial complex of dimension $d$ over $V$ that contains no empty square. Then for every proper coloring $r$ of $C$ ,

d_N\big(B(C, r)\big) \le 1 .

This is the coloring-free version of Proposition 43: the absence of empty squares is a property of the complex alone, and it bounds the Natarajan dimension of every pseudo-cube the complex defines.

Formalization Note $B(C,r)$ is a class over Fin (d + 1); the dimension is $\mathbb N_\infty$ -valued.

Preamble

import Mathlib
import Definitions.Def_MulticlassDS_NatGap_Dimensions
import Definitions.Def_MulticlassDS_NatGap_Complexes

Formal statement

namespace MulticlassDS.NatGap

theorem cor44_no_empty_square_natarajan_le_one {V : Type*} (C : Set (Finset V)) (d : ℕ)
    (hC : IsGood C d) (hsq : NoEmptySquares C) :
    ∀ r : V → Fin (d + 1), IsProperColoring C d r →
      natarajanDim (pseudoCubeOf C d r) ≤ 1 := by sorry

end MulticlassDS.NatGap

Source

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

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