Turán problems in the hypercube

DefinitionHypercube graph#✓fully proved

For a natural number \(n\), the \(n\)-dimensional hypercube \(Q_n\) is the simple graph whose vertices are the functions from \(\{0, \dots, n-1\}\) to the Booleans \(\{\mathrm{true}, \mathrm{false}\}\), with an edge between two vertices exactly when they differ in exactly one coordinate.

def hypercubeGraph (n : ℕ) : SimpleGraph (Fin n → Bool) :=
  SimpleGraph.fromRel (fun x y => ∃! i, x i ≠ y i)

Used by 10

Used byAttainment of the hypercube Turán number · Adjacency in the hypercube · An edge of the one-dimensional hypercube · Subgraphs of the hypercube have at most as many edges · The zero-dimensional hypercube has no edges · No two vertices of the zero-dimensional hypercube are adjacent · Hypercube Turán number · Upper bound for the hypercube Turán number · The hypercube Turán number in dimension zero · The hypercube Turán number bounds every free subgraph

TheoremAdjacency in the hypercube#✓fully proved

For every natural number \(n\) and all vertices \(x, y\) of the \(n\)-dimensional hypercube \(Q_n\) (functions from \(\{0, \dots, n-1\}\) to the Booleans), \(x\) and \(y\) are adjacent in \(Q_n\) if and only if there is exactly one coordinate \(i\) with \(x_i \ne y_i\).

@[simp]
theorem hypercubeGraph_adj (n : ℕ) (x y : Fin n → Bool) :
    (hypercubeGraph n).Adj x y ↔ ∃! i, x i ≠ y i

Uses 1 · Used by 2

Statement usesHypercube graph

Used byAn edge of the one-dimensional hypercube · No two vertices of the zero-dimensional hypercube are adjacent

TheoremNo two vertices of the zero-dimensional hypercube are adjacent#✓fully proved

For all vertices \(x, y\) of the \(0\)-dimensional hypercube \(Q_0\), \(x\) and \(y\) are not adjacent in \(Q_0\).

Any two vertices agree on all (zero) coordinates.

theorem hypercubeGraph_zero_not_adj (x y : Fin 0 → Bool) :
    ¬ (hypercubeGraph 0).Adj x y

Uses 2 · Used by 1

Statement usesHypercube graph

Proof usesAdjacency in the hypercube

Used byThe zero-dimensional hypercube has no edges

TheoremAn edge of the one-dimensional hypercube#✓fully proved

In the \(1\)-dimensional hypercube \(Q_1\), the constant vertex \(\mathrm{true}\) and the constant vertex \(\mathrm{false}\) are adjacent.

theorem hypercubeGraph_one_adj :
    (hypercubeGraph 1).Adj (fun _ => true) (fun _ => false)

Uses 2

Statement usesHypercube graph

Proof usesAdjacency in the hypercube

TheoremThe zero-dimensional hypercube has no edges#✓fully proved

The edge set of the \(0\)-dimensional hypercube \(Q_0\) is empty.

theorem hypercubeGraph_zero_edgeSet : (hypercubeGraph 0).edgeSet = ∅

Uses 2 · Used by 1

Statement usesHypercube graph

Proof usesNo two vertices of the zero-dimensional hypercube are adjacent

Used byThe hypercube Turán number in dimension zero

TheoremSubgraphs of the hypercube have at most as many edges#✓fully proved

For every natural number \(n\), every subgraph of the \(n\)-dimensional hypercube \(Q_n\) has at most as many edges as \(Q_n\).

theorem hypercubeGraph_subgraph_edgeSet_ncard_le (n : ℕ)
    (S : Subgraph (hypercubeGraph n)) :
    S.edgeSet.ncard ≤ (hypercubeGraph n).edgeSet.ncard

Uses 1 · Used by 3

Statement usesHypercube graph

Used byAttainment of the hypercube Turán number · Upper bound for the hypercube Turán number · The hypercube Turán number bounds every free subgraph

DefinitionHypercube Turán number#✓fully proved

For a natural number \(n\) and a simple graph \(H\), let \(Q_n\) be the \(n\)-dimensional hypercube. The hypercube Turán number \(\mathrm{ex}(Q_n, H)\) is the largest number of edges of a subgraph (not necessarily spanning) of \(Q_n\) that contains no copy of \(H\), that is, no subgraph isomorphic to \(H\); it is \(0\) when no such subgraph exists.

noncomputable def hypercubeTuranNumber (n : ℕ) {W : Type*} (H : SimpleGraph W) : ℕ := by
  classical
  exact Finset.sup
    ((Finset.range ((hypercubeGraph n).edgeSet.ncard + 1)).filter
      (fun m => ∃ S : Subgraph (hypercubeGraph n), H.Free S.coe ∧ S.edgeSet.ncard = m))
    id

Uses 1 · Used by 8

Statement usesHypercube graph

Used byAttainment of the hypercube Turán number · Four-cycle-free subgraphs of the hypercubes of dimensions one to six · Upper bound for the hypercube Turán number · Upper bound for four-cycle-free subgraphs of the seven-dimensional hypercube · The hypercube Turán number in dimension zero · The hypercube Turán number bounds every free subgraph · Lower bound for four-cycle-free subgraphs of the eight-dimensional hypercube · Lower bound for four-cycle-free subgraphs of the seven-dimensional hypercube

TheoremThe hypercube Turán number bounds every free subgraph#✓fully proved

For every natural number \(n\) and every simple graph \(H\), let \(Q_n\) be the \(n\)-dimensional hypercube and let \(\mathrm{ex}(Q_n, H)\) be the hypercube Turán number of \(H\) in \(Q_n\). If \(S\) is a subgraph of \(Q_n\) that contains no copy of \(H\), then \(S\) has at most \(\mathrm{ex}(Q_n, H)\) edges.

theorem le_hypercubeTuranNumber (n : ℕ) {W : Type*} {H : SimpleGraph W}
    (S : Subgraph (hypercubeGraph n)) (hfree : H.Free S.coe) :
    S.edgeSet.ncard ≤ hypercubeTuranNumber n H

Uses 3

Statement usesHypercube graph · Hypercube Turán number

Proof usesSubgraphs of the hypercube have at most as many edges

TheoremUpper bound for the hypercube Turán number#✓fully proved

For every natural number \(n\) and every simple graph \(H\), writing \(Q_n\) for the \(n\)-dimensional hypercube, the hypercube Turán number \(\mathrm{ex}(Q_n, H)\) is at most the number of edges of \(Q_n\).

theorem hypercubeTuranNumber_le_edgeSet_ncard (n : ℕ) {W : Type*} (H : SimpleGraph W) :
    hypercubeTuranNumber n H ≤ (hypercubeGraph n).edgeSet.ncard

Uses 3 · Used by 1

Statement usesHypercube graph · Hypercube Turán number

Proof usesSubgraphs of the hypercube have at most as many edges

Used byThe hypercube Turán number in dimension zero

TheoremAttainment of the hypercube Turán number#✓fully proved

Let \(n\) be a natural number, \(H\) a simple graph, \(Q_n\) the \(n\)-dimensional hypercube, and \(\mathrm{ex}(Q_n, H)\) the hypercube Turán number. If \(Q_n\) has at least one subgraph (not necessarily spanning) that contains no copy of \(H\), then some subgraph \(S\) of \(Q_n\) contains no copy of \(H\) and has exactly \(\mathrm{ex}(Q_n, H)\) edges.

theorem exists_attains_hypercubeTuranNumber (n : ℕ) {W : Type*} {H : SimpleGraph W}
    (hne : ∃ S : Subgraph (hypercubeGraph n), H.Free S.coe) :
    ∃ S : Subgraph (hypercubeGraph n),
      H.Free S.coe ∧ S.edgeSet.ncard = hypercubeTuranNumber n H

Uses 3

Statement usesHypercube graph · Hypercube Turán number

Proof usesSubgraphs of the hypercube have at most as many edges

TheoremThe hypercube Turán number in dimension zero#✓fully proved

For every simple graph \(H\), writing \(Q_0\) for the \(0\)-dimensional hypercube, the hypercube Turán number \(\mathrm{ex}(Q_0, H)\) is \(0\).

theorem hypercubeTuranNumber_zero {W : Type*} (H : SimpleGraph W) :
    hypercubeTuranNumber 0 H = 0

Uses 4

Statement usesHypercube Turán number

Proof usesHypercube graph · The zero-dimensional hypercube has no edges · Upper bound for the hypercube Turán number

TheoremFour-cycle-free subgraphs of the hypercubes of dimensions one to six#●ready to prove

For a natural number \(n\), let \(Q_n\) be the \(n\)-dimensional hypercube, let \(C_4\) be the cycle on four vertices, and let \(\mathrm{ex}(Q_n, C_4)\) be the largest number of edges of a subgraph of \(Q_n\) that contains no copy of \(C_4\). Then for \(n = 1, 2, 3, 4, 5, 6\) the value of \(\mathrm{ex}(Q_n, C_4)\) is \(1\), \(3\), \(9\), \(24\), \(56\) and \(132\) respectively.

public theorem_wanted hypercubeTuranNumber_cycleGraph_four_one_to_six :
    (List.range 6).map (fun i => hypercubeTuranNumber (i + 1) (cycleGraph 4)) =
      [1, 3, 9, 24, 56, 132]

Sources

• OEIS A245762; ex(Q₆, C₄) = 132 is H. Harborth and H. Nienborg, Maximum number of edges in squarefree subgraphs of the n-cube, Bull. Inst. Combin. Appl. 12 (1994), 55–60; listed in leansolving/SqueezeBench SqueezeBench/Problems/HypercubeC4/README.md.

Uses 1

Statement usesHypercube Turán number

TheoremLower bound for four-cycle-free subgraphs of the seven-dimensional hypercube#●ready to prove

Let \(Q_7\) be the \(7\)-dimensional hypercube and \(C_4\) the cycle on four vertices. The largest number \(\mathrm{ex}(Q_7, C_4)\) of edges of a subgraph of \(Q_7\) that contains no copy of \(C_4\) is at least \(304\).

The bound is witnessed by an explicit construction.

public theorem_wanted le_hypercubeTuranNumber_seven_cycleGraph_four :
    304 ≤ hypercubeTuranNumber 7 (cycleGraph 4)

Sources

• M. Minamoto, C₄-free subgraphs of the hypercubes Q₆, Q₇, and Q₈, arXiv:2603.29127 (2026); listed in SqueezeBench SqueezeBench/Problems/HypercubeC4/README.md.

Uses 1

Statement usesHypercube Turán number

TheoremUpper bound for four-cycle-free subgraphs of the seven-dimensional hypercube#●ready to prove

Let \(Q_7\) be the \(7\)-dimensional hypercube and \(C_4\) the cycle on four vertices. The largest number \(\mathrm{ex}(Q_7, C_4)\) of edges of a subgraph of \(Q_7\) that contains no copy of \(C_4\) is at most \(308\).

The bound comes from averaging over the fourteen facets of \(Q_7\): each is a copy of \(Q_6\) and each edge lies in six of them, so \(\mathrm{ex}(Q_7, C_4) \le 14 \cdot \mathrm{ex}(Q_6, C_4) / 6 = 14 \cdot 132 / 6 = 308\).

public theorem_wanted hypercubeTuranNumber_seven_cycleGraph_four_le :
    hypercubeTuranNumber 7 (cycleGraph 4) ≤ 308

Sources

• the averaging bound applied to ex(Q₆, C₄) = 132 (Harborth and Nienborg 1994), as stated in SqueezeBench SqueezeBench/Problems/HypercubeC4/README.md.

Uses 1

Statement usesHypercube Turán number

TheoremLower bound for four-cycle-free subgraphs of the eight-dimensional hypercube#●ready to prove

Let \(Q_8\) be the \(8\)-dimensional hypercube and \(C_4\) the cycle on four vertices. The largest number \(\mathrm{ex}(Q_8, C_4)\) of edges of a subgraph of \(Q_8\) that contains no copy of \(C_4\) is at least \(682\).

The bound is witnessed by an explicit construction.

public theorem_wanted le_hypercubeTuranNumber_eight_cycleGraph_four :
    682 ≤ hypercubeTuranNumber 8 (cycleGraph 4)

Sources

• M. Minamoto, C₄-free subgraphs of the hypercubes Q₆, Q₇, and Q₈, arXiv:2603.29127v5 (2026), which improves the bound 680 of its earlier versions; SqueezeBench SqueezeBench/Problems/HypercubeC4/README.md and OEIS A245762 still list 680.

Uses 1

Statement usesHypercube Turán number

11 fully proved4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.