Line counts of linear spaces

DefinitionLinear spaces (2-designs)#✓fully proved

A family \(A_1, \dots, A_t\) of subsets of \(\{1, \dots, v\}\) is a \(2\)-design (also called a pairwise balanced design or a linear space) when every block \(A_i\) has at least two points and every pair of distinct points of \(\{1, \dots, v\}\) lies in exactly one block.

def IsTwoDesign {v t : ℕ} (A : Fin t → Finset (Fin v)) : Prop :=
  (∀ i, 2 ≤ (A i).card) ∧ ∀ x y : Fin v, x ≠ y → ∃! i, x ∈ A i ∧ y ∈ A i

Used by 1

Used byErdős Problem 903: line counts just above a projective plane

DefinitionErdős Problem 903: line counts just above a projective plane#✓fully proved

This is the statement that for every prime power \(p\), with \(n = p^2 + p + 1\), every \(2\)-design \(A_1, \dots, A_t\) on \(\{1, \dots, n\}\) with more than \(n\) blocks has at least \(n + p\) blocks. Here a \(2\)-design is a family of subsets in which every block has at least two points and every pair of distinct points lies in exactly one block.

def lineCountGapAboveProjectivePlane : Prop :=
  ∀ p : ℕ, IsPrimePow p → ∀ (t : ℕ) (A : Fin t → Finset (Fin (p ^ 2 + p + 1))),
    IsTwoDesign A → p ^ 2 + p + 1 < t → p ^ 2 + p + 1 + p ≤ t

def IsTwoDesign {v t : ℕ} (A : Fin t → Finset (Fin v)) : Prop :=
  (∀ i, 2 ≤ (A i).card) ∧ ∀ x y : Fin v, x ≠ y → ∃! i, x ∈ A i ∧ y ∈ A i

WantedExt/Combinatorics/LinearSpaceLineCountGapErdosProblem903Wanted.lean:43

Uses 1 · Used by 1

Statement usesLinear spaces (2-designs)

Used byErdős–Fowler–Sós–Wilson gap above a projective plane (Erdős Problem 903)

TheoremErdős–Fowler–Sós–Wilson gap above a projective plane (Erdős Problem 903)#●ready to prove

Let \(p\) be a prime power and \(n = p^2 + p + 1\). Let \(A_1, \dots, A_t\) be a \(2\)-design on \(\{1, \dots, n\}\): every block \(A_i\) has at least two points and every pair of distinct points lies in exactly one block. If \(t > n\), then \(t \ge n + p\).

Erdős, Fowler, Sós and Wilson prove this for every natural number \(p\), not only prime powers.

public theorem_wanted lineCountGapAboveProjectivePlane_holds : lineCountGapAboveProjectivePlane

def lineCountGapAboveProjectivePlane : Prop :=
  ∀ p : ℕ, IsPrimePow p → ∀ (t : ℕ) (A : Fin t → Finset (Fin (p ^ 2 + p + 1))),
    IsTwoDesign A → p ^ 2 + p + 1 < t → p ^ 2 + p + 1 + p ≤ t

WantedExt/Combinatorics/LinearSpaceLineCountGapErdosProblem903Wanted.lean:48

Sources

T. F. Bloom, Erdős Problems, Problem #903, https://www.erdosproblems.com/903 (status PROVED); resolution: P. Erdős, J. C. Fowler, V. T. Sós and R. M. Wilson, On 2-designs, J. Combin. Theory Ser. A 38 (1985), 131-142, Theorem 2: for v = p² + p + 1 (p not necessarily a prime power) there is no 2-design with v points and b lines when p² + p + 1 < b < p² + 2p + 1, where a 2-design has every pair of points in exactly one block and every block of size > 1, https://users.renyi.hu/~p_erdos/1985-22.pdf.

Uses 1

Statement usesErdős Problem 903: line counts just above a projective plane

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.