Mathesis

Dhruv GuptaZetetic-Dhruvperson2026-09-24T00:00:00Z

HasDSDimLE.hasNatarajanDimLE has no converse. The six-cycle on a two-point domain has Natarajan dimension 1, a Natarajan witness on both points being a four-cycle, while its whole trace family is a two-dimensional pseudo-cube, so its DS dimension is at least 2.

This is the hexagon Brukhim, Carmon, Dinur, Moran and Yehudayoff record after their Definition 6, and the four-cycle test the proof turns on is their Example 7. Their Theorem 2 pushes the separation to a class of Natarajan dimension 1 and infinite DS dimension; that construction rests on hyperbolic pseudo-manifolds and is cited in the module docstring rather than formalised here.

Declexists_hasNatarajanDimLE_not_hasDSDimLE

∃ 𝒞, HasNatarajanDimLE 1 𝒞 ∧ ¬HasDSDimLE 1 𝒞

TopicMulticlass dimensions

Relations

Shares definitions withMTH.C-2026-6005
Built on the same pair patterns and pair-shattering; neither implies the other.
Asserted by Dhruv Gupta

ThesisStepDefinition

Declexists_hasNatarajanDimLE_not_hasDSDimLEDeclaration kindtheorem
```
∃ 𝒞, HasNatarajanDimLE 1 𝒞 ∧ ¬HasDSDimLE 1 𝒞
```
HasDSDimLE HasNatarajanDimLE sixCycle
Uses
- sixCycle_dsShatters
- sixCycle_hasNatarajanDimLE_one
DeclsixCycle_hasNatarajanDimLE_oneDeclaration kindtheorem
```
HasNatarajanDimLE 1 sixCycle✝
```
HasNatarajanDimLE IsPairPattern PairShatters pairSupport sixCycle
Uses
- sixCycle_no_square
- sixCycle_realises
Used by
- exists_hasNatarajanDimLE_not_hasDSDimLE

DeclsixCycle_realisesDeclaration kindtheorem

∀ {P : Fin 2 → Set (Fin 6)},
  PairShatters sixCycle✝ P →
    pairSupport P = Set.univ → ∀ {y₀ y₁ : Fin 6}, y₀ ∈ P 0 → y₁ ∈ P 1 → sixCycleEdge✝ y₀ y₁ = true

PairShatters pairSupport sixCycle sixCycleEdge

Used by

sixCycle_hasNatarajanDimLE_one

DeclsixCycle_no_squareDeclaration kindtheorem

∀ (a b c d : Fin 6),
  sixCycleEdge✝ a c = true →
    sixCycleEdge✝ a d = true → sixCycleEdge✝ b c = true → sixCycleEdge✝ b d = true → a = b ∨ c = d

sixCycleEdge

Used by

sixCycle_hasNatarajanDimLE_one

DeclsixCycle_dsShattersDeclaration kindtheorem
```
DSShatters sixCycle✝ Set.univ
```
DSShatters sixCycle sixCycleEdge
Uses
Used by
- exists_hasNatarajanDimLE_not_hasDSDimLE
DeclsixCycle_nonemptyDeclaration kindtheorem
```
sixCycle✝.Nonempty
```
sixCycle sixCycleEdge
Used by
- sixCycle_dsShatters

DeclsixCycle_nbrDeclaration kindtheorem

∀ (c : Fin 2 → Fin 6),
  sixCycleEdge✝ (c 0) (c 1) = true →
    ∀ (i : Fin 2), ∃ c', sixCycleEdge✝ (c' 0) (c' 1) = true ∧ c' i ≠ c i ∧ ∀ (j : Fin 2), j ≠ i → c' j = c j

sixCycleEdge

Used by

sixCycle_dsShatters

DecldsShatters_univDeclaration kindtheorem

A family whose members each have, in every direction, a neighbour in the family is DS-shattered on the whole domain.

∀ {X : Type u_1} {Y : Type u_2} {𝒞 : Set (X → Y)},
  𝒞.Nonempty →
    (Set.univ.restrict '' 𝒞).Finite →
      (∀ c ∈ 𝒞, ∀ (i : X), ∃ c' ∈ 𝒞, c' i ≠ c i ∧ ∀ (j : X), j ≠ i → c' j = c j) → DSShatters 𝒞 Set.univ

DSShatters IsPseudoCube

Used by

sixCycle_dsShatters

DefinitionDSShattersdef
A family DS-shatters a set when its traces there contain a pseudo-cube.
```
{X : Type u_1} → {Y : Type u_2} → Set (X → Y) → Set X → Prop
```
DefinitionHasDSDimLEdef
A family has DS dimension at most d when every set it DS-shatters has size at most d.
```
{X : Type u_1} → {Y : Type u_2} → ℕ → Set (X → Y) → Prop
```
DefinitionHasNatarajanDimLEdef
A family has Natarajan dimension at most d when every pair pattern it pair-shatters has support of size at most d.
```
{X : Type u_1} → {Y : Type u_2} → ℕ → Set (X → Y) → Prop
```
DefinitionIsPairPatterndef
A pattern is a pair pattern when it offers either no constraint or exactly two labels at each point. The two labels are recorded as a set, so their order carries no information.
```
{X : Type u_1} → {Y : Type u_2} → (X → Set Y) → Prop
```
DefinitionIsPseudoCubedef
A family of labellings of S is a pseudo-cube when it is nonempty and finite and every member has, in every direction, a neighbour in the family differing there and agreeing everywhere else. Over two labels the pseudo-cubes are exactly the Boolean cubes; over more labels there are others.
```
{X : Type u_1} → {Y : Type u_2} → {S : Set X} → Set (↑S → Y) → Prop
```
DefinitionPairShattersdef
A family pair-shatters a pattern when every choice of one admissible label per constrained point is realised by some member.
```
{X : Type u_1} → {Y : Type u_2} → Set (X → Y) → (X → Set Y) → Prop
```
DefinitionpairSupportdef
The points at which a pattern constrains a concept.
```
{X : Type u_1} → {Y : Type u_2} → (X → Set Y) → Set X
```
DefinitionsixCycledef
The six-cycle read as a family of labellings of a two-point domain. Its traces form a two-dimensional pseudo-cube containing no two-dimensional Boolean cube, a six-cycle having no four-cycle.
```
Set (Fin 2 → Fin 6)
```
DefinitionsixCycleEdgedef
The edges of a six-cycle on six labels.
```
Fin 6 → Fin 6 → Bool
```

DOIMTH.R-2026-6006

Cite

Verification

Replay: accepted
Axioms: Classical.choiceQuot.soundpropext
Statement identity: not-applicable
Substrate: Lean 4 kernel v4.31.0
Dictionary pin: design-lab@5802df4 · initial
Frozen export: acba08a11007
Verified: 2026-09-24T00:00:00Z