Shannon capacity of a graph

AbbreviationPositive block lengths#✓fully proved

The type of positive integers, that is, of natural numbers \(n\) with \(1 \le n\), used as the block lengths of codes.

abbrev PositiveNat := {n : ℕ // 1 ≤ n}

Used by 3

Used byRate of a cycle code · Code rates are at most the cycle capacity · Shannon capacity of the modular cycle

DefinitionIndependent codes for the modular cycle#✓fully proved

Let \(q\) and \(n\) be natural numbers. A finite set \(A\) of words of length \(n\) over \(\mathbb{Z}/q\mathbb{Z}\) is an independent code for the \(q\)-cycle when every difference \(x = a_1 - a_2\) with \(a_1, a_2 \in A\) whose coordinates all lie in \(\{-1, 0, 1\}\) is the zero word. For \(q \ge 3\) this says exactly that \(A\) is an independent set in the \(n\)-th strong power of the cycle graph \(C_q\).

The source uses odd \(q \ge 7\); the definition is stated for every \(q\).

def IsCycleCode (q : ℕ) {n : ℕ} (A : Finset (Fin n → ZMod q)) : Prop :=
  ∀ (x : Fin n → ZMod q),
    (∃ a₁ ∈ A, ∃ a₂ ∈ A, a₁ - a₂ = x) →
    (∀ i : Fin n, x i = -1 ∨ x i = 0 ∨ x i = 1) →
    x = 0

Used by 15

Used byBuys–Polak–Zuiddam code for the eleven-cycle in dimension 174 · Buys–Polak–Zuiddam code for the fifteen-cycle in dimension 4096 · Buys–Polak–Zuiddam code for the nineteen-cycle in dimension 16384 · Buys–Polak–Zuiddam code for the 7-cycle in length 200 · Buys–Polak–Zuiddam code for the 13-cycle in length 432 · Buys–Polak–Zuiddam code for the 21-cycle in length 4096 · Buys–Polak–Zuiddam code for the 23-cycle in length 2048 · Cycle codes · Finitely many cycle codes of each length · Rate of a cycle code · Codes give lower bounds on the cycle capacity · Gao's code of dimension 200 for the 7-cycle · Itty–Rosin–Carstensen–Reichman code of dimension 10 for the 7-cycle · Polak–Schrijver code of size 367 for the 7-cycle · Tandon's dimension-500 code for the 7-cycle

AbbreviationCycle codes#✓fully proved

For natural numbers \(q\) and \(n\), a cycle code of length \(n\) modulo \(q\) is a finite set of words of length \(n\) over \(\mathbb{Z}/q\mathbb{Z}\) that is an independent code for the \(q\)-cycle.

abbrev CycleCode (q n : ℕ) := {A : Finset (Fin n → ZMod q) // IsCycleCode q A}

Uses 1 · Used by 4

Statement usesIndependent codes for the modular cycle

Used byFinitely many cycle codes of each length · Rate of a cycle code · Code rates are at most the cycle capacity · Shannon capacity of the modular cycle

TheoremFinitely many cycle codes of each length#✓fully proved

For every nonzero natural number \(q\) and every natural number \(n\), there are only finitely many cycle codes of length \(n\) modulo \(q\).

theorem cycleCode_finite (q n : ℕ) [NeZero q] : Finite (CycleCode q n)

Uses 2

Statement usesCycle codes

Proof usesIndependent codes for the modular cycle

DefinitionRate of a cycle code#✓fully proved

For a natural number \(q\), a positive integer \(n\) and a cycle code \(A\) of length \(n\) modulo \(q\), the rate of \(A\) is \(|A|^{1/n}\), the \(n\)-th root of the number of codewords of \(A\), taken in the extended nonnegative reals \([0, \infty]\).

noncomputable def cycleCodeRate (q : ℕ) (n : PositiveNat) (A : CycleCode q n.1) : ENNReal :=
  ENNReal.rpow (A.1.card : ENNReal) ((n.1 : ℝ)⁻¹)

Uses 3 · Used by 2

Statement usesCycle codes · Independent codes for the modular cycle · Positive block lengths

Used byCode rates are at most the cycle capacity · Shannon capacity of the modular cycle

DefinitionShannon capacity of the modular cycle#✓fully proved

For a natural number \(q\), the Shannon capacity of the \(q\)-cycle is the supremum, in \([0, \infty]\), of the rates \(|A|^{1/n}\) over all positive integers \(n\) and all cycle codes \(A\) of length \(n\) modulo \(q\).

noncomputable def shannonCapacityCycle (q : ℕ) : ENNReal :=
  ⨆ (n : PositiveNat) (A : CycleCode q n.1), cycleCodeRate q n A

Uses 3 · Used by 18

Statement usesCycle codes · Positive block lengths · Rate of a cycle code

Used byBaumert et al. lower bound for the capacity of the 7-cycle · Buys–Polak–Zuiddam lower bound for the capacity of the eleven-cycle · Buys–Polak–Zuiddam lower bound for the capacity of the fifteen-cycle · Buys–Polak–Zuiddam lower bound for the capacity of the 19-cycle · Buys–Polak–Zuiddam lower bound for the capacity of the 7-cycle · Buys–Polak–Zuiddam lower bound for the capacity of the 13-cycle · Buys–Polak–Zuiddam lower bound for the capacity of the 21-cycle · Buys–Polak–Zuiddam lower bound for the capacity of the 23-cycle · Code rates are at most the cycle capacity · Codes give lower bounds on the cycle capacity · Gao's lower bound for the capacity of the 7-cycle · Itty–Rosin–Carstensen–Reichman lower bound for the capacity of the 7-cycle · Lovász's upper bound for the capacity of the 7-cycle · Mathew–Östergård lower bound for the capacity of the 7-cycle · Polak–Schrijver lower bound for the capacity of the 7-cycle · Shannon's upper bound for the capacity of the 7-cycle · Tandon's lower bound for the capacity of the 7-cycle · Vesel–Žerovnik lower bound for the capacity of the 7-cycle

TheoremCode rates are at most the cycle capacity#✓fully proved

For every natural number \(q\), every positive integer \(n\) and every cycle code \(A\) of length \(n\) modulo \(q\), the rate of \(A\) is at most the Shannon capacity of the \(q\)-cycle.

theorem cycleCodeRate_le_shannonCapacity (q : ℕ) (n : PositiveNat)
    (A : CycleCode q n.1) :
    cycleCodeRate q n A ≤ shannonCapacityCycle q

Uses 4 · Used by 1

Statement usesCycle codes · Positive block lengths · Rate of a cycle code · Shannon capacity of the modular cycle

Used byCodes give lower bounds on the cycle capacity

TheoremCodes give lower bounds on the cycle capacity#✓fully proved

Let \(q\), \(n\) and \(M\) be natural numbers with \(n \ge 1\). If some finite set of words of length \(n\) over \(\mathbb{Z}/q\mathbb{Z}\) is an independent code for the \(q\)-cycle and has exactly \(M\) elements, then \(M^{1/n}\) is at most the Shannon capacity of the \(q\)-cycle, as an inequality in \([0, \infty]\).

theorem cycleConstruction_implies_lowerBound (q n M : ℕ) (hn : 1 ≤ n) :
    (∃ A : Finset (Fin n → ZMod q), IsCycleCode q A ∧ A.card = M) →
      ENNReal.rpow (M : ENNReal) ((n : ℝ)⁻¹) ≤ shannonCapacityCycle q

Uses 3

Statement usesIndependent codes for the modular cycle · Shannon capacity of the modular cycle

Proof usesCode rates are at most the cycle capacity

TheoremPolak–Schrijver code of size 367 for the 7-cycle#●ready to prove

There is a finite set \(A\) of words of length \(5\) over \(\mathbb{Z}/7\mathbb{Z}\) that is an independent code for the \(7\)-cycle and has exactly \(367\) elements.

theorem_wanted polakSchrijverLowerBound :
  ∃ A : Finset (Fin 5 → ZMod 7), IsCycleCode 7 A ∧ A.card = 367

Sources

• Polak--Schrijver, arXiv:1808.07438, the fifth-power 367-word construction.

Uses 1

Statement usesIndependent codes for the modular cycle

TheoremShannon's upper bound for the capacity of the 7-cycle#●ready to prove

The Shannon capacity of the \(7\)-cycle is at most \(7/2\).

theorem_wanted shannon1956UpperBound :
  shannonCapacityCycle 7 ≤ (7 : ENNReal) / 2

Sources

• Shannon (1956), the fractional-clique-cover upper bound.

Uses 1

Statement usesShannon capacity of the modular cycle

DefinitionLovász's theta value for the 7-cycle#✓fully proved

This is the real number \(\frac{7 \cos(\pi/7)}{1 + \cos(\pi/7)}\), Lovász's closed form for the theta number of the \(7\)-cycle, viewed as an element of \([0, \infty]\).

Approximate decimal displays of this number in the source are not asserted as equalities.

noncomputable def lovaszThetaCycleSeven : ENNReal :=
  ENNReal.ofReal (7 * Real.cos (Real.pi / 7) / (1 + Real.cos (Real.pi / 7)))

Sources

• Lovász (1979), as printed in BPZ, arXiv:2607.29681.

Used by 1

Used byLovász's upper bound for the capacity of the 7-cycle

TheoremLovász's upper bound for the capacity of the 7-cycle#●ready to prove

The Shannon capacity of the \(7\)-cycle is at most \(\frac{7 \cos(\pi/7)}{1 + \cos(\pi/7)}\), as an inequality in \([0, \infty]\).

theorem_wanted lovasz1979UpperBound :
  shannonCapacityCycle 7 ≤ lovaszThetaCycleSeven

Sources

• Lovász (1979); the closed form is also printed in the retained BPZ primary.

Uses 2

Statement usesShannon capacity of the modular cycle · Lovász's theta value for the 7-cycle

TheoremBaumert et al. lower bound for the capacity of the 7-cycle#●ready to prove

The Shannon capacity of the \(7\)-cycle is at least \(343^{1/5}\), as an inequality in \([0, \infty]\).

theorem_wanted bmrrst1971LowerBound :
  ENNReal.rpow 343 ((5 : ℝ)⁻¹) ≤ shannonCapacityCycle 7

Sources

• Baumert--McEliece--Rodemich--Rumsey--Stanley--Taylor (1971), exact rate row.

Uses 1

Statement usesShannon capacity of the modular cycle

TheoremVesel–Žerovnik lower bound for the capacity of the 7-cycle#●ready to prove

The Shannon capacity of the \(7\)-cycle is at least \(108^{1/4}\).

theorem_wanted veselZerovnik2002LowerBound :
  ENNReal.rpow 108 ((4 : ℝ)⁻¹) ≤ shannonCapacityCycle 7

Sources

• Vesel--Žerovnik (2002), exact rate row; no unprinted code is supplied.

Uses 1

Statement usesShannon capacity of the modular cycle

TheoremMathew–Östergård lower bound for the capacity of the 7-cycle#●ready to prove

The Shannon capacity of the \(7\)-cycle is at least \(350^{1/5}\), as an inequality in \([0, \infty]\).

theorem_wanted mathewOstergard2017LowerBound :
  ENNReal.rpow 350 ((5 : ℝ)⁻¹) ≤ shannonCapacityCycle 7

Sources

• Mathew--Östergård (2017), exact rate row; no unprinted code is supplied.

Uses 1

Statement usesShannon capacity of the modular cycle

TheoremPolak–Schrijver lower bound for the capacity of the 7-cycle#●ready to prove

The Shannon capacity of the \(7\)-cycle is at least \(367^{1/5}\), as an inequality in \([0, \infty]\).

theorem_wanted polakSchrijverRateLowerBound :
  ENNReal.rpow 367 ((5 : ℝ)⁻¹) ≤ shannonCapacityCycle 7

Sources

• Polak--Schrijver, arXiv:1808.07438, exact fifth-root rate.

Uses 1

Statement usesShannon capacity of the modular cycle

TheoremItty–Rosin–Carstensen–Reichman lower bound for the capacity of the 7-cycle#●ready to prove

The Shannon capacity of the \(7\)-cycle is at least \(134753^{1/10}\), as an inequality in \([0, \infty]\).

theorem_wanted ittyRosinCarstensenReichman2026LowerBound :
  ENNReal.rpow 134753 ((10 : ℝ)⁻¹) ≤ shannonCapacityCycle 7

Sources

• Itty--Rosin--Carstensen--Reichman, arXiv:2607.21517, exact tenth-root rate.

Uses 1

Statement usesShannon capacity of the modular cycle

TheoremItty–Rosin–Carstensen–Reichman code of dimension 10 for the 7-cycle#●ready to prove

There is a finite set \(A\) of words of length \(10\) over \(\mathbb{Z}/7\mathbb{Z}\) that is an independent code for the \(7\)-cycle and has exactly \(134753\) elements.

theorem_wanted ittyRosinCarstensenReichman2026Construction :
  ∃ A : Finset (Fin 10 → ZMod 7), IsCycleCode 7 A ∧ A.card = 134753

Sources

• Itty--Rosin--Carstensen--Reichman, arXiv:2607.21517, tenth-power construction.

Uses 1

Statement usesIndependent codes for the modular cycle

StructureBPZ profiles#✓fully proved

A BPZ profile is an arbitrary quadruple of integers, called its code, pairs, auxiliary and neutral coordinates: the four integer coordinates propagated by the valid-tuple product of Buys, Polak and Zuiddam. No validity condition is imposed on the quadruple.

structure BPZProfile where
  code : ℤ
  pairs : ℤ
  auxiliary : ℤ
  neutral : ℤ
  deriving DecidableEq, Repr

Sources

• BPZ, arXiv:2607.29681, valid-tuple profiles.

Used by 49

Used byOne-block BPZ profile for the 11-cycle · Fourteen-block BPZ profile for the 11-cycle · Fifteen-block BPZ profile for the 11-cycle · Two-block BPZ profile for the 11-cycle · Twenty-nine-block BPZ profile for the 11-cycle · Three-block BPZ profile for the 11-cycle · Four-block BPZ profile for the 11-cycle · Fifty-eight-block BPZ profile for the 11-cycle · Seven-block BPZ profile for the 11-cycle · Eight-block BPZ profile of the eleven-cycle · One-block BPZ profile of the thirteen-cycle · Two-block BPZ profile of the thirteen-cycle · Three-block BPZ profile of the thirteen-cycle · Four-block BPZ profile of the thirteen-cycle · Five-block BPZ profile of the thirteen-cycle · Seventy-two-block BPZ profile of the thirteen-cycle · Nine-block BPZ profile of the thirteen-cycle · One-block BPZ profile of the fifteen-cycle · BPZ profile of the fifteen-cycle after ten squarings · Buys–Polak–Zuiddam one-block profile for the 19-cycle · Buys–Polak–Zuiddam 4096-block profile for the 19-cycle · Buys–Polak–Zuiddam one-block profile for the 21-cycle · Buys–Polak–Zuiddam 1024-block profile for the 21-cycle · Buys–Polak–Zuiddam one-block profile for the 23-cycle · Buys–Polak–Zuiddam 512-block profile for the 23-cycle · Buys–Polak–Zuiddam one-block profile for the 7-cycle · Buys–Polak–Zuiddam ten-block profile for the 7-cycle · Buys–Polak–Zuiddam two-block profile for the 7-cycle · Buys–Polak–Zuiddam twenty-block profile for the 7-cycle · Three-block BPZ seven-cycle profile · Forty-block BPZ seven-cycle profile · Code coordinate of the forty-block BPZ seven-cycle profile · Five-block BPZ seven-cycle profile · Iterated squaring of BPZ profiles · Buys–Polak–Zuiddam code for the eleven-cycle in dimension 174 · Buys–Polak–Zuiddam lower bound for the capacity of the eleven-cycle · Buys–Polak–Zuiddam code for the fifteen-cycle in dimension 4096 · Buys–Polak–Zuiddam lower bound for the capacity of the fifteen-cycle · Buys–Polak–Zuiddam code for the nineteen-cycle in dimension 16384 · Buys–Polak–Zuiddam lower bound for the capacity of the 19-cycle · Buys–Polak–Zuiddam code for the 7-cycle in length 200 · Buys–Polak–Zuiddam lower bound for the capacity of the 7-cycle · Buys–Polak–Zuiddam code for the 13-cycle in length 432 · Buys–Polak–Zuiddam lower bound for the capacity of the 13-cycle · Buys–Polak–Zuiddam code for the 21-cycle in length 4096 · Buys–Polak–Zuiddam lower bound for the capacity of the 21-cycle · Buys–Polak–Zuiddam code for the 23-cycle in length 2048 · Buys–Polak–Zuiddam lower bound for the capacity of the 23-cycle · Product of BPZ profiles

DefinitionProduct of BPZ profiles#✓fully proved

For \(i = 1, 2\) let \(p_i = (c_i, \pi_i, a_i, z_i)\) be a BPZ profile, with integer code, pairs, auxiliary and neutral coordinates. The product \(p_1 \star p_2\) is the BPZ profile with code coordinate \((c_1 - \pi_1)(c_2 - \pi_2) + a_1 \pi_2 + \pi_1 a_2\), pairs coordinate \(z_1 \pi_2 + \pi_1 z_2\), auxiliary coordinate \(a_1 a_2\) and neutral coordinate \(z_1 z_2 + (a_1 - z_1)(a_2 - z_2)\).

The product is arithmetic on the four coordinates only; it does not supply an independent set.

def BPZProfile.star (p₁ p₂ : BPZProfile) : BPZProfile where
  code :=
    (p₁.code - p₁.pairs) * (p₂.code - p₂.pairs) +
      p₁.auxiliary * p₂.pairs + p₁.pairs * p₂.auxiliary
  pairs := p₁.neutral * p₂.pairs + p₁.pairs * p₂.neutral
  auxiliary := p₁.auxiliary * p₂.auxiliary
  neutral :=
    p₁.neutral * p₂.neutral +
      (p₁.auxiliary - p₁.neutral) * (p₂.auxiliary - p₂.neutral)

Sources

• BPZ, arXiv:2607.29681, the profile product.

Uses 1 · Used by 21

Statement usesBPZ profiles

Used byFourteen-block BPZ profile for the 11-cycle · Fifteen-block BPZ profile for the 11-cycle · Two-block BPZ profile for the 11-cycle · Twenty-nine-block BPZ profile for the 11-cycle · Three-block BPZ profile for the 11-cycle · Four-block BPZ profile for the 11-cycle · Fifty-eight-block BPZ profile for the 11-cycle · Seven-block BPZ profile for the 11-cycle · Eight-block BPZ profile of the eleven-cycle · Two-block BPZ profile of the thirteen-cycle · Three-block BPZ profile of the thirteen-cycle · Four-block BPZ profile of the thirteen-cycle · Five-block BPZ profile of the thirteen-cycle · Nine-block BPZ profile of the thirteen-cycle · Buys–Polak–Zuiddam ten-block profile for the 7-cycle · Buys–Polak–Zuiddam two-block profile for the 7-cycle · Buys–Polak–Zuiddam twenty-block profile for the 7-cycle · Three-block BPZ seven-cycle profile · Forty-block BPZ seven-cycle profile · Five-block BPZ seven-cycle profile · Iterated squaring of BPZ profiles

DefinitionIterated squaring of BPZ profiles#✓fully proved

Write \(\star\) for the BPZ profile product. For a natural number \(k\) and a BPZ profile \(p\), the \(k\)-fold iterated square \(S_k(p)\) is defined by \(S_0(p) = p\) and \(S_{k+1}(p) = S_k(p \star p)\); that is, \(S_k(p)\) is obtained from \(p\) by squaring \(k\) times under \(\star\).

def bpzProfileSquareIter : ℕ → BPZProfile → BPZProfile
  | 0, p => p
  | k + 1, p => bpzProfileSquareIter k (p.star p)

Sources

• BPZ, arXiv:2607.29681, iterated profile products.

Uses 2 · Used by 5

Statement usesBPZ profiles · Product of BPZ profiles

Used bySeventy-two-block BPZ profile of the thirteen-cycle · BPZ profile of the fifteen-cycle after ten squarings · Buys–Polak–Zuiddam 4096-block profile for the 19-cycle · Buys–Polak–Zuiddam 1024-block profile for the 21-cycle · Buys–Polak–Zuiddam 512-block profile for the 23-cycle

DefinitionGao's code size in dimension 200#✓fully proved

\(M_{40}\) is the natural number \(4085567963379990282748597333793399773399910167372462 112610203714626938509773125898252337545387866277249\), the cardinality Gao prints for a code of length \(200\) for the \(7\)-cycle.

def gao2026M40 : ℕ :=
  4085567963379990282748597333793399773399910167372462112610203714626938509773125898252337545387866277249

Sources

• Gao, arXiv:2607.27869, the printed M40 value.

Used by 2

Used byGao's code of dimension 200 for the 7-cycle · Gao's lower bound for the capacity of the 7-cycle

TheoremGao's code of dimension 200 for the 7-cycle#●ready to prove

Let \(M_{40}\) be Gao's printed dimension-200 cardinality, a natural number with 103 decimal digits. There is a finite set \(A\) of words of length \(200\) over \(\mathbb{Z}/7\mathbb{Z}\) that is an independent code for the \(7\)-cycle and has exactly \(M_{40}\) elements.

theorem_wanted gao2026Construction :
  ∃ A : Finset (Fin 200 → ZMod 7), IsCycleCode 7 A ∧ A.card = gao2026M40

Sources

• Gao, arXiv:2607.27869, exact dimension-200 construction.

Uses 2

Statement usesIndependent codes for the modular cycle · Gao's code size in dimension 200

TheoremGao's lower bound for the capacity of the 7-cycle#●ready to prove

Let \(M_{40}\) be Gao's printed dimension-200 cardinality, a natural number with 103 decimal digits. The Shannon capacity of the \(7\)-cycle is at least \(M_{40}^{1/200}\), as an inequality in \([0, \infty]\).

theorem_wanted gao2026LowerBound :
  ENNReal.rpow (gao2026M40 : ENNReal) ((200 : ℝ)⁻¹) ≤ shannonCapacityCycle 7

Sources

• Gao, arXiv:2607.27869, exact dimension-200 root rate.

Uses 2

Statement usesShannon capacity of the modular cycle · Gao's code size in dimension 200

DefinitionBuys–Polak–Zuiddam one-block profile for the 7-cycle#✓fully proved

This is the Buys–Polak–Zuiddam (BPZ) profile whose code, pairs, auxiliary and neutral coordinates are \(367\), \(8\), \(367\) and \(322\).

Only these four integers are recorded, not BPZ's five-dimensional construction behind them.

def bpzC7Pi1 : BPZProfile := ⟨367, 8, 367, 322⟩

Sources

• BPZ, arXiv:2607.29681, seven-cycle construction.

Uses 1 · Used by 2

Statement usesBPZ profiles

Used byBuys–Polak–Zuiddam two-block profile for the 7-cycle · Three-block BPZ seven-cycle profile

DefinitionBuys–Polak–Zuiddam two-block profile for the 7-cycle#✓fully proved

This is \(p_1 \star p_1\), where \(p_1\) is the one-block 7-cycle profile, whose code, pairs, auxiliary and neutral coordinates are \(367\), \(8\), \(367\) and \(322\), and \(\star\) is the Buys–Polak–Zuiddam (BPZ) profile product.

def bpzC7Pi2 : BPZProfile := bpzC7Pi1.star bpzC7Pi1

Sources

• BPZ, arXiv:2607.29681, seven-cycle construction.

Uses 3 · Used by 2

Statement usesBPZ profiles · Product of BPZ profiles · Buys–Polak–Zuiddam one-block profile for the 7-cycle

Used byThree-block BPZ seven-cycle profile · Five-block BPZ seven-cycle profile

DefinitionThree-block BPZ seven-cycle profile#✓fully proved

A BPZ profile is a quadruple of integers (code, pairs, auxiliary, neutral), and \(\star\) denotes the BPZ profile product. The three-block seven-cycle profile of Buys–Polak–Zuiddam is \(\pi_3 = \pi_1 \star \pi_2\), where \(\pi_1 = (367, 8, 367, 322)\) is the one-block profile and \(\pi_2 = \pi_1 \star \pi_1\) is the two-block profile.

def bpzC7Pi3 : BPZProfile := bpzC7Pi1.star bpzC7Pi2

Sources

• BPZ, arXiv:2607.29681, seven-cycle construction.

Uses 4 · Used by 1

Statement usesBPZ profiles · Product of BPZ profiles · Buys–Polak–Zuiddam one-block profile for the 7-cycle · Buys–Polak–Zuiddam two-block profile for the 7-cycle

Used byFive-block BPZ seven-cycle profile

DefinitionFive-block BPZ seven-cycle profile#✓fully proved

A BPZ profile is a quadruple of integers (code, pairs, auxiliary, neutral), and \(\star\) denotes the BPZ profile product. The five-block seven-cycle profile of Buys–Polak–Zuiddam is \(\pi_5 = \pi_2 \star \pi_3\), where \(\pi_1 = (367, 8, 367, 322)\), \(\pi_2 = \pi_1 \star \pi_1\) and \(\pi_3 = \pi_1 \star \pi_2\) are the one-, two- and three-block profiles.

def bpzC7Pi5 : BPZProfile := bpzC7Pi2.star bpzC7Pi3

Sources

• BPZ, arXiv:2607.29681, seven-cycle construction.

Uses 4 · Used by 1

Statement usesBPZ profiles · Product of BPZ profiles · Buys–Polak–Zuiddam two-block profile for the 7-cycle · Three-block BPZ seven-cycle profile

Used byBuys–Polak–Zuiddam ten-block profile for the 7-cycle

DefinitionBuys–Polak–Zuiddam ten-block profile for the 7-cycle#✓fully proved

This is \(p_5 \star p_5\), where \(p_5\) is the five-block 7-cycle profile and \(\star\) is the Buys–Polak–Zuiddam (BPZ) profile product.

def bpzC7Pi10 : BPZProfile := bpzC7Pi5.star bpzC7Pi5

Sources

• BPZ, arXiv:2607.29681, seven-cycle construction.

Uses 3 · Used by 1

Statement usesBPZ profiles · Product of BPZ profiles · Five-block BPZ seven-cycle profile

Used byBuys–Polak–Zuiddam twenty-block profile for the 7-cycle

DefinitionBuys–Polak–Zuiddam twenty-block profile for the 7-cycle#✓fully proved

This is \(p_{10} \star p_{10}\), where \(p_{10}\) is the ten-block 7-cycle profile and \(\star\) is the Buys–Polak–Zuiddam (BPZ) profile product.

def bpzC7Pi20 : BPZProfile := bpzC7Pi10.star bpzC7Pi10

Sources

• BPZ, arXiv:2607.29681, seven-cycle construction.

Uses 3 · Used by 1

Statement usesBPZ profiles · Product of BPZ profiles · Buys–Polak–Zuiddam ten-block profile for the 7-cycle

Used byForty-block BPZ seven-cycle profile

DefinitionForty-block BPZ seven-cycle profile#✓fully proved

A BPZ profile is a quadruple of integers (code, pairs, auxiliary, neutral), and \(\star\) denotes the BPZ profile product. The final forty-block seven-cycle profile of Buys–Polak–Zuiddam is \(\pi_{40} = \pi_{20} \star \pi_{20}\), where \(\pi_1 = (367, 8, 367, 322)\), \(\pi_2 = \pi_1 \star \pi_1\), \(\pi_3 = \pi_1 \star \pi_2\), \(\pi_5 = \pi_2 \star \pi_3\), \(\pi_{10} = \pi_5 \star \pi_5\) and \(\pi_{20} = \pi_{10} \star \pi_{10}\).

def bpzC7Pi40 : BPZProfile := bpzC7Pi20.star bpzC7Pi20

Sources

• BPZ, arXiv:2607.29681, seven-cycle construction.

Uses 3 · Used by 3

Statement usesBPZ profiles · Product of BPZ profiles · Buys–Polak–Zuiddam twenty-block profile for the 7-cycle

Used byCode coordinate of the forty-block BPZ seven-cycle profile · Buys–Polak–Zuiddam code for the 7-cycle in length 200 · Buys–Polak–Zuiddam lower bound for the capacity of the 7-cycle

TheoremCode coordinate of the forty-block BPZ seven-cycle profile#✓fully proved

The code coordinate (the first of the four integer coordinates) of the forty-block seven-cycle profile \(\pi_{40}\) of Buys–Polak–Zuiddam equals \(4089635995108338053456272492117641008738901835089431264388780413340766441486608 118807897325023935704961\).

theorem bpzC7Pi40_code :
    bpzC7Pi40.code =
      4089635995108338053456272492117641008738901835089431264388780413340766441486608118807897325023935704961

Sources

• BPZ, arXiv:2607.29681, forty-block seven-cycle recursion.

Uses 2

Statement usesBPZ profiles · Forty-block BPZ seven-cycle profile

TheoremBuys–Polak–Zuiddam code for the 7-cycle in length 200#●ready to prove

Let \(c\) be the code coordinate of BPZ's final forty-block seven-cycle profile, and let \(M = \max(c, 0)\). There is a finite set of words of length \(200\) over \(\mathbb{Z}/7\mathbb{Z}\) that is an independent code for the \(7\)-cycle and has exactly \(M\) elements.

theorem_wanted bpz2026CycleSevenConstruction :
  ∃ A : Finset (Fin 200 → ZMod 7), IsCycleCode 7 A ∧ A.card = bpzC7Pi40.code.toNat

Sources

• BPZ, arXiv:2607.29681, the exact forty-block dimension-200 construction.

Uses 3

Statement usesIndependent codes for the modular cycle · BPZ profiles · Forty-block BPZ seven-cycle profile

TheoremBuys–Polak–Zuiddam lower bound for the capacity of the 7-cycle#●ready to prove

Let \(c\) be the code coordinate of BPZ's final forty-block seven-cycle profile, and let \(M = \max(c, 0)\). Then \(M^{1/200}\) is at most the Shannon capacity of the \(7\)-cycle, as an inequality in \([0, \infty]\).

theorem_wanted bpz2026CycleSevenLowerBound :
  ENNReal.rpow (bpzC7Pi40.code.toNat : ENNReal) ((200 : ℝ)⁻¹) ≤ shannonCapacityCycle 7

Sources

• BPZ, arXiv:2607.29681, the exact dimension-200 root rate.

Uses 3

Statement usesShannon capacity of the modular cycle · BPZ profiles · Forty-block BPZ seven-cycle profile

DefinitionTandon's dimension-500 code size#✓fully proved

Tandon's dimension-500 code size is the natural number \(M^*\) with \(257\) decimal digits given by

\[ M^* = 33964672918117456943408517573718333225317390754651100605971152590324909277046876400440 35395842835926298962152039473727668119665577675838633047083277330855915999031707610213 1413374061066595834823529274560988950698158729501949866486079791784996498585401881281 \]

def tandon2026Mstar : ℕ :=
  33964672918117456943408517573718333225317390754651100605971152590324909277046876400440353958428359262989621520394737276681196655776758386330470832773308559159990317076102131413374061066595834823529274560988950698158729501949866486079791784996498585401881281

Sources

• Tandon, arXiv:2608.30273, the printed Mstar value.

Used by 2

Used byTandon's dimension-500 code for the 7-cycle · Tandon's lower bound for the capacity of the 7-cycle

TheoremTandon's dimension-500 code for the 7-cycle#●ready to prove

Let \(M^*\) be Tandon's dimension-500 code size. There is an independent code for the \(7\)-cycle consisting of words of length \(500\) over \(\mathbb{Z}/7\mathbb{Z}\) with exactly \(M^*\) codewords.

theorem_wanted tandon2026Construction :
  ∃ A : Finset (Fin 500 → ZMod 7), IsCycleCode 7 A ∧ A.card = tandon2026Mstar

Sources

• Tandon, arXiv:2608.30273, exact dimension-500 construction.

Uses 2

Statement usesIndependent codes for the modular cycle · Tandon's dimension-500 code size

TheoremTandon's lower bound for the capacity of the 7-cycle#●ready to prove

Let \(M^*\) be Tandon's dimension-500 code size. The Shannon capacity of the \(7\)-cycle is at least \((M^*)^{1/500}\).

theorem_wanted tandon2026LowerBound :
  ENNReal.rpow (tandon2026Mstar : ENNReal) ((500 : ℝ)⁻¹) ≤ shannonCapacityCycle 7

Sources

• Tandon, arXiv:2608.30273, exact dimension-500 root rate.

Uses 2

Statement usesShannon capacity of the modular cycle · Tandon's dimension-500 code size

DefinitionOne-block BPZ profile for the 11-cycle#✓fully proved

The one-block eleven-cycle profile of Buys, Polak and Zuiddam is the profile with code coordinate \(148\), pairs coordinate \(3\), auxiliary coordinate \(148\) and neutral coordinate \(142\).

In the source this profile comes from a construction in dimension \(3\); that origin is not checked here.

def bpzC11Pi1 : BPZProfile := ⟨148, 3, 148, 142⟩

Sources

• BPZ, arXiv:2607.29681, eleven-cycle construction.

Uses 1 · Used by 2

Statement usesBPZ profiles

Used byTwo-block BPZ profile for the 11-cycle · Three-block BPZ profile for the 11-cycle

DefinitionTwo-block BPZ profile for the 11-cycle#✓fully proved

The two-block eleven-cycle profile of Buys, Polak and Zuiddam is the profile product \(\pi_1 \star \pi_1\), where \(\pi_1\) is their one-block eleven-cycle profile.

def bpzC11Pi2 : BPZProfile := bpzC11Pi1.star bpzC11Pi1

Sources

• BPZ, arXiv:2607.29681, eleven-cycle construction.

Uses 3 · Used by 2

Statement usesBPZ profiles · Product of BPZ profiles · One-block BPZ profile for the 11-cycle

Used byThree-block BPZ profile for the 11-cycle · Four-block BPZ profile for the 11-cycle

DefinitionThree-block BPZ profile for the 11-cycle#✓fully proved

The three-block eleven-cycle profile of Buys, Polak and Zuiddam is the profile product \(\pi_1 \star \pi_2\), where \(\pi_1\) and \(\pi_2\) are their one-block and two-block eleven-cycle profiles.

def bpzC11Pi3 : BPZProfile := bpzC11Pi1.star bpzC11Pi2

Sources

• BPZ, arXiv:2607.29681, eleven-cycle construction.

Uses 4 · Used by 1

Statement usesBPZ profiles · Product of BPZ profiles · One-block BPZ profile for the 11-cycle · Two-block BPZ profile for the 11-cycle

Used bySeven-block BPZ profile for the 11-cycle

DefinitionFour-block BPZ profile for the 11-cycle#✓fully proved

The four-block eleven-cycle profile of Buys, Polak and Zuiddam is the profile product \(\pi_2 \star \pi_2\), where \(\pi_2\) is their two-block eleven-cycle profile.

def bpzC11Pi4 : BPZProfile := bpzC11Pi2.star bpzC11Pi2

Sources

• BPZ, arXiv:2607.29681, eleven-cycle construction.

Uses 3 · Used by 2

Statement usesBPZ profiles · Product of BPZ profiles · Two-block BPZ profile for the 11-cycle

Used bySeven-block BPZ profile for the 11-cycle · Eight-block BPZ profile of the eleven-cycle

DefinitionSeven-block BPZ profile for the 11-cycle#✓fully proved

The seven-block eleven-cycle profile of Buys, Polak and Zuiddam is the profile product \(\pi_3 \star \pi_4\), where \(\pi_3\) and \(\pi_4\) are their three-block and four-block eleven-cycle profiles.

def bpzC11Pi7 : BPZProfile := bpzC11Pi3.star bpzC11Pi4

Sources

• BPZ, arXiv:2607.29681, eleven-cycle construction.

Uses 4 · Used by 2

Statement usesBPZ profiles · Product of BPZ profiles · Three-block BPZ profile for the 11-cycle · Four-block BPZ profile for the 11-cycle

Used byFourteen-block BPZ profile for the 11-cycle · Fifteen-block BPZ profile for the 11-cycle

DefinitionEight-block BPZ profile of the eleven-cycle#✓fully proved

The eight-block BPZ profile of the eleven-cycle is \(\pi_4 \star \pi_4\), where \(\pi_4\) is the four-block BPZ profile of the eleven-cycle and \(\star\) is the BPZ profile product.

def bpzC11Pi8 : BPZProfile := bpzC11Pi4.star bpzC11Pi4

Sources

• BPZ, arXiv:2607.29681, eleven-cycle construction.

Uses 3 · Used by 1

Statement usesBPZ profiles · Product of BPZ profiles · Four-block BPZ profile for the 11-cycle

Used byFifteen-block BPZ profile for the 11-cycle

DefinitionFourteen-block BPZ profile for the 11-cycle#✓fully proved

The fourteen-block eleven-cycle profile of Buys, Polak and Zuiddam is the profile product \(\pi_7 \star \pi_7\), where \(\pi_7\) is their seven-block eleven-cycle profile.

def bpzC11Pi14 : BPZProfile := bpzC11Pi7.star bpzC11Pi7

Sources

• BPZ, arXiv:2607.29681, eleven-cycle construction.

Uses 3 · Used by 1

Statement usesBPZ profiles · Product of BPZ profiles · Seven-block BPZ profile for the 11-cycle

Used byTwenty-nine-block BPZ profile for the 11-cycle

DefinitionFifteen-block BPZ profile for the 11-cycle#✓fully proved

The fifteen-block eleven-cycle profile of Buys, Polak and Zuiddam is the profile product \(\pi_7 \star \pi_8\), where \(\pi_7\) and \(\pi_8\) are their seven-block and eight-block eleven-cycle profiles.

def bpzC11Pi15 : BPZProfile := bpzC11Pi7.star bpzC11Pi8

Sources

• BPZ, arXiv:2607.29681, eleven-cycle construction.

Uses 4 · Used by 1

Statement usesBPZ profiles · Product of BPZ profiles · Seven-block BPZ profile for the 11-cycle · Eight-block BPZ profile of the eleven-cycle

Used byTwenty-nine-block BPZ profile for the 11-cycle

DefinitionTwenty-nine-block BPZ profile for the 11-cycle#✓fully proved

The twenty-nine-block eleven-cycle profile of Buys, Polak and Zuiddam is the profile product \(\pi_{14} \star \pi_{15}\), where \(\pi_{14}\) and \(\pi_{15}\) are their fourteen-block and fifteen-block eleven-cycle profiles.

def bpzC11Pi29 : BPZProfile := bpzC11Pi14.star bpzC11Pi15

Sources

• BPZ, arXiv:2607.29681, eleven-cycle construction.

Uses 4 · Used by 1

Statement usesBPZ profiles · Product of BPZ profiles · Fourteen-block BPZ profile for the 11-cycle · Fifteen-block BPZ profile for the 11-cycle

Used byFifty-eight-block BPZ profile for the 11-cycle

DefinitionFifty-eight-block BPZ profile for the 11-cycle#✓fully proved

The final fifty-eight-block eleven-cycle profile of Buys, Polak and Zuiddam is the profile product \(\pi_{29} \star \pi_{29}\), where \(\pi_{29}\) is their twenty-nine-block eleven-cycle profile.

def bpzC11Pi58 : BPZProfile := bpzC11Pi29.star bpzC11Pi29

Sources

• BPZ, arXiv:2607.29681, eleven-cycle construction.

Uses 3 · Used by 2

Statement usesBPZ profiles · Product of BPZ profiles · Twenty-nine-block BPZ profile for the 11-cycle

Used byBuys–Polak–Zuiddam code for the eleven-cycle in dimension 174 · Buys–Polak–Zuiddam lower bound for the capacity of the eleven-cycle

DefinitionOne-block BPZ profile of the thirteen-cycle#✓fully proved

The one-block BPZ profile of the thirteen-cycle is the BPZ profile with code coordinate \(62530\), pairs coordinate \(1014\), auxiliary coordinate \(62530\) and neutral coordinate \(60502\).

BPZ describe it as their one-block six-dimensional thirteen-cycle profile.

def bpzC13Pi1 : BPZProfile := ⟨62530, 1014, 62530, 60502⟩

Sources

• BPZ, arXiv:2607.29681, thirteen-cycle construction.

Uses 1 · Used by 2

Statement usesBPZ profiles

Used byTwo-block BPZ profile of the thirteen-cycle · Three-block BPZ profile of the thirteen-cycle

DefinitionTwo-block BPZ profile of the thirteen-cycle#✓fully proved

The two-block BPZ profile of the thirteen-cycle is \(\pi_1 \star \pi_1\), where \(\pi_1\) is the one-block BPZ profile of the thirteen-cycle and \(\star\) is the BPZ profile product.

def bpzC13Pi2 : BPZProfile := bpzC13Pi1.star bpzC13Pi1

Sources

• BPZ, arXiv:2607.29681, thirteen-cycle construction.

Uses 3 · Used by 3

Statement usesBPZ profiles · Product of BPZ profiles · One-block BPZ profile of the thirteen-cycle

Used byThree-block BPZ profile of the thirteen-cycle · Four-block BPZ profile of the thirteen-cycle · Five-block BPZ profile of the thirteen-cycle

DefinitionThree-block BPZ profile of the thirteen-cycle#✓fully proved

The three-block BPZ profile of the thirteen-cycle is \(\pi_1 \star \pi_2\), where \(\pi_1\) and \(\pi_2\) are the one-block and two-block BPZ profiles of the thirteen-cycle and \(\star\) is the BPZ profile product.

def bpzC13Pi3 : BPZProfile := bpzC13Pi1.star bpzC13Pi2

Sources

• BPZ, arXiv:2607.29681, thirteen-cycle construction.

Uses 4 · Used by 1

Statement usesBPZ profiles · Product of BPZ profiles · One-block BPZ profile of the thirteen-cycle · Two-block BPZ profile of the thirteen-cycle

Used byFive-block BPZ profile of the thirteen-cycle

DefinitionFour-block BPZ profile of the thirteen-cycle#✓fully proved

The four-block BPZ profile of the thirteen-cycle is \(\pi_2 \star \pi_2\), where \(\pi_2\) is the two-block BPZ profile of the thirteen-cycle and \(\star\) is the BPZ profile product.

def bpzC13Pi4 : BPZProfile := bpzC13Pi2.star bpzC13Pi2

Sources

• BPZ, arXiv:2607.29681, thirteen-cycle construction.

Uses 3 · Used by 1

Statement usesBPZ profiles · Product of BPZ profiles · Two-block BPZ profile of the thirteen-cycle

Used byNine-block BPZ profile of the thirteen-cycle

DefinitionFive-block BPZ profile of the thirteen-cycle#✓fully proved

The five-block BPZ profile of the thirteen-cycle is \(\pi_2 \star \pi_3\), where \(\pi_2\) and \(\pi_3\) are the two-block and three-block BPZ profiles of the thirteen-cycle and \(\star\) is the BPZ profile product.

def bpzC13Pi5 : BPZProfile := bpzC13Pi2.star bpzC13Pi3

Sources

• BPZ, arXiv:2607.29681, thirteen-cycle construction.

Uses 4 · Used by 1

Statement usesBPZ profiles · Product of BPZ profiles · Two-block BPZ profile of the thirteen-cycle · Three-block BPZ profile of the thirteen-cycle

Used byNine-block BPZ profile of the thirteen-cycle

DefinitionNine-block BPZ profile of the thirteen-cycle#✓fully proved

The nine-block BPZ profile of the thirteen-cycle is \(\pi_4 \star \pi_5\), where \(\pi_4\) and \(\pi_5\) are the four-block and five-block BPZ profiles of the thirteen-cycle and \(\star\) is the BPZ profile product.

def bpzC13Pi9 : BPZProfile := bpzC13Pi4.star bpzC13Pi5

Sources

• BPZ, arXiv:2607.29681, thirteen-cycle construction.

Uses 4 · Used by 1

Statement usesBPZ profiles · Product of BPZ profiles · Four-block BPZ profile of the thirteen-cycle · Five-block BPZ profile of the thirteen-cycle

Used bySeventy-two-block BPZ profile of the thirteen-cycle

DefinitionSeventy-two-block BPZ profile of the thirteen-cycle#✓fully proved

Let \(\pi_9\) be the nine-block BPZ profile of the thirteen-cycle, and let \(\star\) be the BPZ profile product. Set \(\sigma_0 = \pi_9\) and \(\sigma_{k+1} = \sigma_k \star \sigma_k\). The seventy-two-block BPZ profile of the thirteen-cycle is \(\sigma_3\), the result of squaring \(\pi_9\) three times.

This is the final profile of BPZ's thirteen-cycle construction.

def bpzC13Pi72 : BPZProfile := bpzProfileSquareIter 3 bpzC13Pi9

Sources

• BPZ, arXiv:2607.29681, thirteen-cycle construction.

Uses 3 · Used by 2

Statement usesBPZ profiles · Nine-block BPZ profile of the thirteen-cycle · Iterated squaring of BPZ profiles

Used byBuys–Polak–Zuiddam code for the 13-cycle in length 432 · Buys–Polak–Zuiddam lower bound for the capacity of the 13-cycle

DefinitionOne-block BPZ profile of the fifteen-cycle#✓fully proved

The one-block BPZ profile of the fifteen-cycle is the BPZ profile with code coordinate \(2842\), pairs coordinate \(3\), auxiliary coordinate \(2842\) and neutral coordinate \(2833\).

BPZ describe it as their one-block four-dimensional fifteen-cycle profile.

def bpzC15Pi1 : BPZProfile := ⟨2842, 3, 2842, 2833⟩

Sources

• BPZ, arXiv:2607.29681, fifteen-cycle construction.

Uses 1 · Used by 1

Statement usesBPZ profiles

Used byBPZ profile of the fifteen-cycle after ten squarings

DefinitionBPZ profile of the fifteen-cycle after ten squarings#✓fully proved

Let \(\pi_1\) be the one-block BPZ profile of the fifteen-cycle, and let \(\star\) be the BPZ profile product. Set \(\sigma_0 = \pi_1\) and \(\sigma_{k+1} = \sigma_k \star \sigma_k\). This profile is \(\sigma_{10}\), the result of squaring \(\pi_1\) ten times.

This is the final profile of BPZ's fifteen-cycle construction.

def bpzC15Pi1024 : BPZProfile := bpzProfileSquareIter 10 bpzC15Pi1

Sources

• BPZ, arXiv:2607.29681, fifteen-cycle construction.

Uses 3 · Used by 2

Statement usesBPZ profiles · One-block BPZ profile of the fifteen-cycle · Iterated squaring of BPZ profiles

Used byBuys–Polak–Zuiddam code for the fifteen-cycle in dimension 4096 · Buys–Polak–Zuiddam lower bound for the capacity of the fifteen-cycle

DefinitionBuys–Polak–Zuiddam one-block profile for the 19-cycle#✓fully proved

This is the Buys–Polak–Zuiddam (BPZ) profile whose code, pairs, auxiliary and neutral coordinates are \(7666\), \(2\), \(7666\) and \(7661\).

Only these four integers are recorded, not BPZ's four-dimensional construction behind them.

def bpzC19Pi1 : BPZProfile := ⟨7666, 2, 7666, 7661⟩

Sources

• BPZ, arXiv:2607.29681, nineteen-cycle construction.

Uses 1 · Used by 1

Statement usesBPZ profiles

Used byBuys–Polak–Zuiddam 4096-block profile for the 19-cycle

DefinitionBuys–Polak–Zuiddam 4096-block profile for the 19-cycle#✓fully proved

Let \(p_0\) be the one-block 19-cycle profile, whose code, pairs, auxiliary and neutral coordinates are \(7666\), \(2\), \(7666\) and \(7661\), and let \(p_{j+1} = p_j \star p_j\), where \(\star\) is the Buys–Polak–Zuiddam (BPZ) profile product. This profile is \(p_{12}\), the result of squaring \(p_0\) twelve times.

def bpzC19Pi4096 : BPZProfile := bpzProfileSquareIter 12 bpzC19Pi1

Sources

• BPZ, arXiv:2607.29681, nineteen-cycle construction.

Uses 3 · Used by 2

Statement usesBPZ profiles · Buys–Polak–Zuiddam one-block profile for the 19-cycle · Iterated squaring of BPZ profiles

Used byBuys–Polak–Zuiddam code for the nineteen-cycle in dimension 16384 · Buys–Polak–Zuiddam lower bound for the capacity of the 19-cycle

DefinitionBuys–Polak–Zuiddam one-block profile for the 21-cycle#✓fully proved

This is the Buys–Polak–Zuiddam (BPZ) profile whose code, pairs, auxiliary and neutral coordinates are \(11441\), \(10\), \(11441\) and \(11398\).

Only these four integers are recorded, not BPZ's four-dimensional construction behind them.

def bpzC21Pi1 : BPZProfile := ⟨11441, 10, 11441, 11398⟩

Sources

• BPZ, arXiv:2607.29681, twenty-one-cycle construction.

Uses 1 · Used by 1

Statement usesBPZ profiles

Used byBuys–Polak–Zuiddam 1024-block profile for the 21-cycle

DefinitionBuys–Polak–Zuiddam 1024-block profile for the 21-cycle#✓fully proved

Let \(p_0\) be the one-block 21-cycle profile, whose code, pairs, auxiliary and neutral coordinates are \(11441\), \(10\), \(11441\) and \(11398\), and let \(p_{j+1} = p_j \star p_j\), where \(\star\) is the Buys–Polak–Zuiddam (BPZ) profile product. This profile is \(p_{10}\), the result of squaring \(p_0\) ten times.

def bpzC21Pi1024 : BPZProfile := bpzProfileSquareIter 10 bpzC21Pi1

Sources

• BPZ, arXiv:2607.29681, twenty-one-cycle construction.

Uses 3 · Used by 2

Statement usesBPZ profiles · Buys–Polak–Zuiddam one-block profile for the 21-cycle · Iterated squaring of BPZ profiles

Used byBuys–Polak–Zuiddam code for the 21-cycle in length 4096 · Buys–Polak–Zuiddam lower bound for the capacity of the 21-cycle

DefinitionBuys–Polak–Zuiddam one-block profile for the 23-cycle#✓fully proved

This is the Buys–Polak–Zuiddam (BPZ) profile whose code, pairs, auxiliary and neutral coordinates are \(16466\), \(30\), \(16466\) and \(16323\).

Only these four integers are recorded, not BPZ's four-dimensional construction behind them.

def bpzC23Pi1 : BPZProfile := ⟨16466, 30, 16466, 16323⟩

Sources

• BPZ, arXiv:2607.29681, twenty-three-cycle construction.

Uses 1 · Used by 1

Statement usesBPZ profiles

Used byBuys–Polak–Zuiddam 512-block profile for the 23-cycle

DefinitionBuys–Polak–Zuiddam 512-block profile for the 23-cycle#✓fully proved

Let \(p_0\) be the one-block 23-cycle profile, whose code, pairs, auxiliary and neutral coordinates are \(16466\), \(30\), \(16466\) and \(16323\), and let \(p_{j+1} = p_j \star p_j\), where \(\star\) is the Buys–Polak–Zuiddam (BPZ) profile product. This profile is \(p_9\), the result of squaring \(p_0\) nine times.

def bpzC23Pi512 : BPZProfile := bpzProfileSquareIter 9 bpzC23Pi1

Sources

• BPZ, arXiv:2607.29681, twenty-three-cycle construction.

Uses 3 · Used by 2

Statement usesBPZ profiles · Buys–Polak–Zuiddam one-block profile for the 23-cycle · Iterated squaring of BPZ profiles

Used byBuys–Polak–Zuiddam code for the 23-cycle in length 2048 · Buys–Polak–Zuiddam lower bound for the capacity of the 23-cycle

TheoremBuys–Polak–Zuiddam code for the eleven-cycle in dimension 174#●ready to prove

Let \(c\) be the code coordinate of the fifty-eight-block eleven-cycle profile \(\pi_{58}\) of Buys–Polak–Zuiddam. There is a finite set of words of length \(174\) over \(\mathbb{Z}/11\mathbb{Z}\) that is an independent code for the \(11\)-cycle and has exactly \(\max(c, 0)\) elements.

theorem_wanted bpz2026CycleElevenConstruction :
  ∃ A : Finset (Fin 174 → ZMod 11), IsCycleCode 11 A ∧ A.card = bpzC11Pi58.code.toNat

Sources

• BPZ, arXiv:2607.29681, eleven-cycle construction in dimension 174.

Uses 3

Statement usesIndependent codes for the modular cycle · BPZ profiles · Fifty-eight-block BPZ profile for the 11-cycle

TheoremBuys–Polak–Zuiddam code for the 13-cycle in length 432#●ready to prove

Let \(c\) be the code coordinate of BPZ's final seventy-two-block thirteen-cycle profile, and let \(M = \max(c, 0)\). There is a finite set of words of length \(432\) over \(\mathbb{Z}/13\mathbb{Z}\) that is an independent code for the \(13\)-cycle and has exactly \(M\) elements.

theorem_wanted bpz2026CycleThirteenConstruction :
  ∃ A : Finset (Fin 432 → ZMod 13), IsCycleCode 13 A ∧ A.card = bpzC13Pi72.code.toNat

Sources

• BPZ, arXiv:2607.29681, thirteen-cycle construction in dimension 432.

Uses 3

Statement usesIndependent codes for the modular cycle · BPZ profiles · Seventy-two-block BPZ profile of the thirteen-cycle

TheoremBuys–Polak–Zuiddam code for the fifteen-cycle in dimension 4096#●ready to prove

Let \(c\) be the code coordinate of the \(1024\)-block fifteen-cycle profile \(\pi_{1024}\) of Buys–Polak–Zuiddam. There is a finite set of words of length \(4096\) over \(\mathbb{Z}/15\mathbb{Z}\) that is an independent code for the \(15\)-cycle and has exactly \(\max(c, 0)\) elements.

theorem_wanted bpz2026CycleFifteenConstruction :
  ∃ A : Finset (Fin 4096 → ZMod 15), IsCycleCode 15 A ∧ A.card = bpzC15Pi1024.code.toNat

Sources

• BPZ, arXiv:2607.29681, fifteen-cycle construction in dimension 4096.

Uses 3

Statement usesIndependent codes for the modular cycle · BPZ profiles · BPZ profile of the fifteen-cycle after ten squarings

TheoremBuys–Polak–Zuiddam code for the nineteen-cycle in dimension 16384#●ready to prove

Let \(c\) be the code coordinate of the \(4096\)-block nineteen-cycle profile \(\pi_{4096}\) of Buys–Polak–Zuiddam. There is a finite set of words of length \(16384\) over \(\mathbb{Z}/19\mathbb{Z}\) that is an independent code for the \(19\)-cycle and has exactly \(\max(c, 0)\) elements.

theorem_wanted bpz2026CycleNineteenConstruction :
  ∃ A : Finset (Fin 16384 → ZMod 19), IsCycleCode 19 A ∧ A.card = bpzC19Pi4096.code.toNat

Sources

• BPZ, arXiv:2607.29681, nineteen-cycle construction in dimension 16384.

Uses 3

Statement usesIndependent codes for the modular cycle · BPZ profiles · Buys–Polak–Zuiddam 4096-block profile for the 19-cycle

TheoremBuys–Polak–Zuiddam code for the 21-cycle in length 4096#●ready to prove

Let \(c\) be the code coordinate of BPZ's final twenty-one-cycle profile after ten squarings, and let \(M = \max(c, 0)\). There is a finite set of words of length \(4096\) over \(\mathbb{Z}/21\mathbb{Z}\) that is an independent code for the \(21\)-cycle and has exactly \(M\) elements.

theorem_wanted bpz2026CycleTwentyOneConstruction :
  ∃ A : Finset (Fin 4096 → ZMod 21), IsCycleCode 21 A ∧ A.card = bpzC21Pi1024.code.toNat

Sources

• BPZ, arXiv:2607.29681, twenty-one-cycle construction in dimension 4096.

Uses 3

Statement usesIndependent codes for the modular cycle · BPZ profiles · Buys–Polak–Zuiddam 1024-block profile for the 21-cycle

TheoremBuys–Polak–Zuiddam code for the 23-cycle in length 2048#●ready to prove

Let \(c\) be the code coordinate of BPZ's final twenty-three-cycle profile after nine squarings, and let \(M = \max(c, 0)\). There is a finite set of words of length \(2048\) over \(\mathbb{Z}/23\mathbb{Z}\) that is an independent code for the \(23\)-cycle and has exactly \(M\) elements.

theorem_wanted bpz2026CycleTwentyThreeConstruction :
  ∃ A : Finset (Fin 2048 → ZMod 23), IsCycleCode 23 A ∧ A.card = bpzC23Pi512.code.toNat

Sources

• BPZ, arXiv:2607.29681, twenty-three-cycle construction in dimension 2048.

Uses 3

Statement usesIndependent codes for the modular cycle · BPZ profiles · Buys–Polak–Zuiddam 512-block profile for the 23-cycle

TheoremBuys–Polak–Zuiddam lower bound for the capacity of the eleven-cycle#●ready to prove

Let \(c\) be the code coordinate of the fifty-eight-block eleven-cycle profile \(\pi_{58}\) of Buys–Polak–Zuiddam. Then \(\max(c, 0)^{1/174}\) is at most the Shannon capacity of the \(11\)-cycle, as an inequality in \([0, \infty]\).

theorem_wanted bpz2026CycleElevenLowerBound :
  ENNReal.rpow (bpzC11Pi58.code.toNat : ENNReal) ((174 : ℝ)⁻¹) ≤ shannonCapacityCycle 11

Sources

• BPZ, arXiv:2607.29681, exact eleven-cycle root rate.

Uses 3

Statement usesShannon capacity of the modular cycle · BPZ profiles · Fifty-eight-block BPZ profile for the 11-cycle

TheoremBuys–Polak–Zuiddam lower bound for the capacity of the 13-cycle#●ready to prove

Let \(c\) be the code coordinate of BPZ's final seventy-two-block thirteen-cycle profile, and let \(M = \max(c, 0)\). Then \(M^{1/432}\) is at most the Shannon capacity of the \(13\)-cycle, as an inequality in \([0, \infty]\).

theorem_wanted bpz2026CycleThirteenLowerBound :
  ENNReal.rpow (bpzC13Pi72.code.toNat : ENNReal) ((432 : ℝ)⁻¹) ≤ shannonCapacityCycle 13

Sources

• BPZ, arXiv:2607.29681, exact thirteen-cycle root rate.

Uses 3

Statement usesShannon capacity of the modular cycle · BPZ profiles · Seventy-two-block BPZ profile of the thirteen-cycle

TheoremBuys–Polak–Zuiddam lower bound for the capacity of the fifteen-cycle#●ready to prove

Let \(c\) be the code coordinate of the \(1024\)-block fifteen-cycle profile \(\pi_{1024}\) of Buys–Polak–Zuiddam. Then \(\max(c, 0)^{1/4096}\) is at most the Shannon capacity of the \(15\)-cycle, as an inequality in \([0, \infty]\).

theorem_wanted bpz2026CycleFifteenLowerBound :
  ENNReal.rpow (bpzC15Pi1024.code.toNat : ENNReal) ((4096 : ℝ)⁻¹) ≤ shannonCapacityCycle 15

Sources

• BPZ, arXiv:2607.29681, exact fifteen-cycle root rate.

Uses 3

Statement usesShannon capacity of the modular cycle · BPZ profiles · BPZ profile of the fifteen-cycle after ten squarings

TheoremBuys–Polak–Zuiddam lower bound for the capacity of the 19-cycle#●ready to prove

Let \(c\) be the code coordinate of BPZ's final nineteen-cycle profile after twelve squarings, and let \(M = \max(c, 0)\). Then \(M^{1/16384}\) is at most the Shannon capacity of the \(19\)-cycle, as an inequality in \([0, \infty]\).

theorem_wanted bpz2026CycleNineteenLowerBound :
  ENNReal.rpow (bpzC19Pi4096.code.toNat : ENNReal) ((16384 : ℝ)⁻¹) ≤ shannonCapacityCycle 19

Sources

• BPZ, arXiv:2607.29681, exact nineteen-cycle root rate.

Uses 3

Statement usesShannon capacity of the modular cycle · BPZ profiles · Buys–Polak–Zuiddam 4096-block profile for the 19-cycle

TheoremBuys–Polak–Zuiddam lower bound for the capacity of the 21-cycle#●ready to prove

Let \(c\) be the code coordinate of BPZ's final twenty-one-cycle profile after ten squarings, and let \(M = \max(c, 0)\). Then \(M^{1/4096}\) is at most the Shannon capacity of the \(21\)-cycle, as an inequality in \([0, \infty]\).

theorem_wanted bpz2026CycleTwentyOneLowerBound :
  ENNReal.rpow (bpzC21Pi1024.code.toNat : ENNReal) ((4096 : ℝ)⁻¹) ≤ shannonCapacityCycle 21

Sources

• BPZ, arXiv:2607.29681, exact twenty-one-cycle root rate.

Uses 3

Statement usesShannon capacity of the modular cycle · BPZ profiles · Buys–Polak–Zuiddam 1024-block profile for the 21-cycle

TheoremBuys–Polak–Zuiddam lower bound for the capacity of the 23-cycle#●ready to prove

Let \(c\) be the code coordinate of BPZ's final twenty-three-cycle profile after nine squarings, and let \(M = \max(c, 0)\). Then \(M^{1/2048}\) is at most the Shannon capacity of the \(23\)-cycle, as an inequality in \([0, \infty]\).

theorem_wanted bpz2026CycleTwentyThreeLowerBound :
  ENNReal.rpow (bpzC23Pi512.code.toNat : ENNReal) ((2048 : ℝ)⁻¹) ≤ shannonCapacityCycle 23

Sources

• BPZ, arXiv:2607.29681, exact twenty-three-cycle root rate.

Uses 3

Statement usesShannon capacity of the modular cycle · BPZ profiles · Buys–Polak–Zuiddam 512-block profile for the 23-cycle

DefinitionStrong power of a graph#✓fully proved

Let \(G\) be a simple graph with vertex set \(V\) and let \(k\) be a natural number. The \(k\)-th strong power \(G^{\boxtimes k}\) is the simple graph whose vertices are the words \(x = (x_1, \dots, x_k) \in V^k\) of length \(k\), in which two words \(x\) and \(y\) are adjacent (confusable) when \(x \neq y\) and for every \(i\) either \(x_i = y_i\) or \(x_i\) and \(y_i\) are adjacent in \(G\).

def strongPower {V : Type*} (G : SimpleGraph V) (k : ℕ) : SimpleGraph (Fin k → V) where
  Adj x y := x ≠ y ∧ ∀ i, x i = y i ∨ G.Adj (x i) (y i)
  symm.symm x y := by
    rintro ⟨hxy, hcoord⟩
    exact ⟨hxy.symm, fun i => (hcoord i).imp Eq.symm SimpleGraph.Adj.symm⟩
  loopless := ⟨fun x h => h.1 rfl⟩

Used by 1

Used byShannon capacity of a graph

DefinitionShannon capacity of a graph#✓fully proved

Let \(G\) be a simple graph on a finite vertex set and let \(\theta\) be a real number. For \(k \ge 1\) let \(G^{\boxtimes k}\) be the \(k\)-th strong power of \(G\) and \(\alpha(G^{\boxtimes k})\) its independence number. The graph \(G\) has Shannon capacity \(\theta\) when \(\alpha(G^{\boxtimes k})^{1/k} \to \theta\) as \(k \to \infty\).

noncomputable def HasShannonCapacity {V : Type*} [Fintype V] (G : SimpleGraph V) (θ : ℝ) :
    Prop :=
  Tendsto
    (fun k : ℕ =>
      Real.rpow
        ((strongPower G (k + 1)).indepNum : ℝ)
        ((k + 1 : ℝ)⁻¹))
    atTop (𝓝 θ)

Uses 1 · Used by 1

Statement usesStrong power of a graph

Used byLovász's theorem: the Shannon capacity of the pentagon

TheoremLovász's theorem: the Shannon capacity of the pentagon#●ready to prove

The cycle graph \(C_5\) on five vertices has Shannon capacity \(\sqrt{5}\): writing \(\alpha(C_5^{\boxtimes k})\) for the independence number of the \(k\)-th strong power of \(C_5\), we have \(\alpha(C_5^{\boxtimes k})^{1/k} \to \sqrt{5}\) as \(k \to \infty\).

public theorem_wanted shannon_capacity_pentagon :
    HasShannonCapacity (SimpleGraph.cycleGraph 5) (Real.sqrt 5)

Sources

• Knill, Some fundamental theorems in mathematics, §238. Problem shannon_capacity_pentagon of the lean-eval benchmark.

Uses 1

Statement usesShannon capacity of a graph

49 fully proved28 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.