Block-compatible sequences of pairwise balanced designs
DefinitionPairwise balanced design#✓fully proved
For a natural number \(n\), a finite list of blocks \(B_1, \ldots, B_m \subseteq \{0, \ldots, n - 1\}\) is a pairwise balanced design on these \(n\) points when the blocks are pairwise distinct, every block has at least two points, and every two distinct points lie in exactly one common block.
def IsPBD (n : ℕ) (blocks : List (Finset (Fin n))) : Prop :=
blocks.Nodup ∧
(∀ B ∈ blocks, 2 ≤ B.card) ∧
∀ x y : Fin n, x ≠ y →
∃! B : Finset (Fin n), B ∈ blocks ∧ x ∈ B ∧ y ∈ BUsed by 1
DefinitionBlock-compatible sequences#✓fully proved
For a natural number \(n\), a finite sequence \((x_1, \ldots, x_m)\) of natural numbers is block-compatible for \(n\) when \(x_1 \ge x_2 \ge \cdots \ge x_m\), every \(x_k\) satisfies \(2 \le x_k \le n\), and there is a pairwise balanced design on the point set \(\{0, \ldots, n - 1\}\) whose blocks, listed in order as \(B_1, \ldots, B_m\), have sizes \(|B_k| = x_k\) for every \(k\).
def BlockCompatible (n : ℕ) (l : List ℕ) : Prop :=
List.Pairwise (· ≥ ·) l ∧ (∀ x ∈ l, 2 ≤ x ∧ x ≤ n) ∧
∃ blocks : List (Finset (Fin n)),
blocks.map Finset.card = l ∧ IsPBD n blocksdef IsPBD (n : ℕ) (blocks : List (Finset (Fin n))) : Prop :=
blocks.Nodup ∧
(∀ B ∈ blocks, 2 ≤ B.card) ∧
∀ x y : Fin n, x ≠ y →
∃! B : Finset (Fin n), B ∈ blocks ∧ x ∈ B ∧ y ∈ BWantedExt/Combinatorics/BlockCompatibleSequenceCountWanted.lean:38
Uses 1 · Used by 1
DefinitionMany block-compatible sequences#✓fully proved
The statement that there are a real number \(c > 0\) and a natural number \(N\) such that for every \(n \ge N\) there is a finite set of at least \(\exp(c \sqrt{n} \log n)\) distinct finite sequences of natural numbers, each of which is block-compatible for \(n\). Here \(\log\) is the natural logarithm.
def conjecture : Prop :=
∃ c : ℝ, 0 < c ∧ ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
∃ S : Finset (List ℕ), (∀ l ∈ S, BlockCompatible n l) ∧
Real.exp (c * Real.sqrt n * Real.log n) ≤ (S.card : ℝ)def BlockCompatible (n : ℕ) (l : List ℕ) : Prop :=
List.Pairwise (· ≥ ·) l ∧ (∀ x ∈ l, 2 ≤ x ∧ x ≤ n) ∧
∃ blocks : List (Finset (Fin n)),
blocks.map Finset.card = l ∧ IsPBD n blocksWantedExt/Combinatorics/BlockCompatibleSequenceCountWanted.lean:46
Sources
- OWR-14299518-002, question (2).
Uses 1 · Used by 1
TheoremMany block-compatible sequences (Erdős Problem 732)#●ready to prove
There are a real number \(c > 0\) and a natural number \(N\) such that for every \(n \ge N\) there is a finite set of at least \(\exp(c \sqrt{n} \log n)\) distinct finite sequences of natural numbers, each of which is block-compatible for \(n\). Here \(\log\) is the natural logarithm.
Alon proved the stronger bound that at least \(2^{(1/2 + o(1)) \sqrt{n} \log n}\) sequences are block-compatible for \(n\) (Oberwolfach Report 42/2025, Theorem 4; also Theorem 2.3 of his note 'Blocking partial designs and block-compatible sequences').
public theorem_wanted conjecture_holds : conjecturedef conjecture : Prop :=
∃ c : ℝ, 0 < c ∧ ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
∃ S : Finset (List ℕ), (∀ l ∈ S, BlockCompatible n l) ∧
Real.exp (c * Real.sqrt n * Real.log n) ≤ (S.card : ℝ)WantedExt/Combinatorics/BlockCompatibleSequenceCountWanted.lean:53
Sources
- N. Alon, On designs and partial designs, extended abstract in Oberwolfach Report 42/2025 (Combinatorics, Probability and Computing), pp. 2249-2250, Theorem 4, https://doi.org/10.4171/owr/2025/42; N. Alon, Blocking partial designs and block-compatible sequences, note, Theorem 2.3, https://web.math.princeton.edu/~nalon/PDFS/remark191.pdf; T. F. Bloom, Erdős Problem #732, erdosproblems.com (status PROVED), https://www.erdosproblems.com/732.
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.