Erdős #902 — Schütte's tournament problem

Let f(n) be the minimum number of vertices in a tournament in which every n-set is dominated by some vertex outside it. Erdős #902 asks for the growth of f(n).

This repository develops the problem in Lean 4 and exact finite computation: asymptotic bounds, small cases, the window for f(4), order-49 Cayley eliminations, doubly regular tournament structure at order 23, and several structural reductions.

Classical bounds in Lean

The main formal theorem is

theorem classical_sandwich (n : ℕ) (hn : 1 ≤ n) :
    (n + 2) * 2 ^ (n - 1) - 1 ≤ f n ∧
    f n ≤ n + 3 * n ^ 2 * 2 ^ n

The lower bound is the Szekeres–Szekeres bound

[ (n+2)2^{n-1}-1\le f(n), ]

proved by multiplicity amplification and descent through in-neighbourhoods.

The upper bound

[ f(n)\le n+3n^2 2^n ]

is an explicit first-moment existence argument. The constant is not optimized.

Erdős's original 1963 lower bound

[ 2^{n+1}-1\le f(n) ]

is also formalized independently.

Exact and finite results

The repository formalizes:

• f(1)=3;

• f(2)=7;

• f(3)>=19 from the Szekeres–Szekeres theorem;

• the complete current finite window

  [ \boxed{48\le f(4)\le67}; ]

• a QR67 certificate proving the upper bound;

• exact elimination of the two order-49 Cayley families on Z/49Z and F_7^2 by SAT with checked DRAT certificates.

The two Cayley eliminations are construction-family results; the unrestricted order-49 case is a separate question.

The order-48 boundary and DRT(23)

For a hypothetical 48-vertex S_4 tournament, the formal reduction forces an in-neighbourhood of size 23 that inherits S_3 and is a doubly regular tournament with parameters (23,11,5).

The two relevant DRT(23) classes are encoded exactly. The formal development proves, among other things:

• their tournament and parameter identities;
• S_3 for both rows;
• exact counts of undominated four-sets;
• for one class, a 2-(23,4,60) design on the bad four-sets;
• rigidity of admissible 12-sets;
• exact repair-capacity bounds for the top two mask layers;
• an explicit identification of one class with the Paley tournament QR_23;
• the affine automorphisms generated by translation and multiplication by 2.

These results live in Erdos902DRT23*.lean, Erdos902Capacity.lean, and Erdos902QR23.lean.

Structural reductions

Several general tournament lemmas are formalized beyond the finite f(4) program.

Dominator cubes

For a k-set P in an S_k tournament, let

[ D_R=\operatorname{dom}(P\setminus R). ]

The Boolean faces satisfy

[ D_R\cap D_S=D_{R\cap S}, ]

and each face carries the corresponding smaller domination property. Failure-set encoding converts face membership into subset containment.

Minimality and private witnesses

Order-minimal extremizers are kings: every vertex is the unique dominator of some n-set and reaches every other vertex in at most two steps.

Private ownership is equivalent to irredundancy of finite covers, giving a Bollobás-style cross-intersecting set-pair structure for private tournament witnesses.

Factorization falsifier

A cyclic tournament family on 2k+1 vertices satisfies the relaxed private-witness Boolean factorization. Therefore that relaxation alone permits linear-size examples and cannot imply an exponential lower bound without using the full global S_k covering condition.

Verification

All headline Lean theorems have axiom footprint

{propext, Classical.choice, Quot.sound}

with no sorry and no native_decide in the counted results.

Build the complete project with

elan toolchain install $(cat lean-toolchain)
lake exe cache get
lake build

Erdos902All.lean imports the full formal development.

Reading map

file	content
Erdos902Szekeres.lean	Szekeres–Szekeres lower bound and classical_sandwich
Erdos902Existence.lean	explicit probabilistic upper bound
Erdos902ClosedForm.lean	Erdős 1963 lower bound and formulation equivalence
Erdos902Control.lean	exact f(1)=3, f(2)=7
Erdos902Reid.lean	f(4)>=48
Erdos902QR67.lean	QR67 certificate and f(4)<=67
ORDER49_MONOLITHIC_ASSAULT.md	checked order-49 Cayley eliminations
Erdos902F4Step.lean	reduction of a hypothetical 48-vertex S_4 tournament
Erdos902DRT23*.lean	exact order-23 doubly regular tournament structure
Erdos902QR23.lean	QR23 identification and affine symmetry
Erdos902Capacity.lean	repair capacities
Erdos902DominatorCube.lean	Boolean dominator-cube structure
Erdos902PrivateCoverBarrier.lean	private-cover and set-pair reductions
Erdos902FactorizationFalsifier.lean	cyclic counterfamily to the relaxed factorization route
Erdos902DropAudit.lean	formal audit of an insufficient switching argument

Status

The general factor-n gap between the lower and upper asymptotic bounds remains open. The exact finite and structural theorems above are independent results within that larger problem.

References

• P. Erdős, On a problem in graph theory, Math. Gaz. 47 (1963), 220–223.
• G. Szekeres and E. Szekeres, On a problem of Schütte and Erdős, Math. Gaz. 49 (1965), 290–293.
• K. B. Reid, A. A. McRae, S. M. Hedetniemi, S. T. Hedetniemi, Domination and irredundance in tournaments, Australas. J. Combin. 29 (2004), 157–172.
• N. Y. Javier, B. Llano, R. Zuazua, 2- and 3-existentially closed tournaments, Contrib. Discrete Math. 21(1) (2026).

License

Apache-2.0.

Author: Jared Wilder.