TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

If $k \geq 1$ and $n \geq 3 k^{2} 2^{k}$ , an $n$ -vertex tournament with property $S_{k}$ exists

Statement

Let $k \geq 1$ and $n \geq 3 k^{2} 2^{k}$ . Then there exists a tournament on $n$ vertices with property $S_{k}$ .

Facts & Assumptions

Given: Naturals $k \geq 1$ and $n \geq 3 k^{2} 2^{k}$ .

[L1]

Property $S_{k}$ means every set of at most $k$ vertices has an outside vertex directing an arc to each of its members (Tournament property $S_{k}$ : every set of at most $k$ vertices is dominated by one vertex).

[L2]

Independent edge orientations form a product probability space (Product weights normalize, and coordinate events are mutually independent).

[L3]

Probability of a finite union is at most the sum of its event probabilities, and an event and its complement have probabilities summing to $1$ (The finite union bound, Normalization, nonnegativity, monotonicity, complements, and differences in a finite probability space).

[L4]

For every real $y$ , $1 + y \leq \exp (y)$ ; consequently $(1 - p)^{m} \leq \exp (- m p)$ for $0 \leq p \leq 1$ ( $1 + x \leq \exp (x)$ for every real $x$ , hence $(1 - p)^{m} \leq \exp (- m p)$ ).

[L5]

The number of $k$ -subsets is $(\binom{n}{k}) = n! / (k! (n - k)!)$ , and $k!$ is its usual finite product (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ , $(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$ , The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ).

[L6]

$e = \exp (1)$ is the sum of its nonnegative exponential series; $\exp (u + v) = \exp (u) \exp (v)$ ; natural powers obey their product laws; and $\log$ is the increasing inverse of $\exp$ with $\log (x y) = \log x + \log y$ (The real exponential function and the number $e$ by a power series, A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum, The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ , Integer powers $a^{m}$ , Laws of integer exponents, Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ , The natural logarithm as the inverse of the exponential function, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[L7]

A positive-probability event in a finite probability space is nonempty (An event of positive probability in a finite probability space is nonempty).

Proof

technique · cases

1.1

Orient every edge independently and fairly. For a fixed $k$ -set $S$ , each outside vertex dominates all of $S$ with probability $2^{- k}$ , independently across outside vertices; hence the failure probability is $(1 - 2^{- k})^{n - k}$ .

2.1

The union bound gives total failure probability at most $F_{k} (n) : = (\binom{n}{k}) (1 - 2^{- k})^{n - k}$ .

step 1.1L3L5

3.1

The ratio $F_{k} (n + 1) / F_{k} (n) = \frac{n + 1}{n + 1 - k} (1 - 2^{- k})$ is at most $1$ whenever $n + 1 \geq k 2^{k}$ . Thus $F_{k} (n)$ is nonincreasing throughout the stated range.

step 2.1L5algebra

3.2

Suppose $k = 1$ . At $n = 6$ , $F_{1} (6) = 6 / 2^{5} < 1$ .

assume-case onestep 2.1algebra

3.3

Suppose $k = 2$ . At $n = 48$ , $F_{2} (48) = 1128 (3 / 4)^{46}$ . Since $(3 / 4)^{8} = 6561 / 65536 < 1 / 9$ , one has $(3 / 4)^{46} < (3 / 4)^{40} < 1 / 9^{5}$ , and $1128 < 9^{5}$ ; hence $F_{2} (48) < 1$ .

assume-case twostep 2.1L5algebra

3.4

Suppose $k \geq 3$ and put $N = 3 k^{2} 2^{k}$ . The $k$ th nonnegative term of the exponential series gives $k! \geq (k / e)^{k}$ , so $(\binom{N}{k}) \leq (e N / k)^{k}$ . With [L4], $F_{k} (N) \leq \exp (k (1 + \log (N / k)) - (N - k) / 2^{k})$ .

assume-case largestep 2.1L4L5L6algebra

4.1

Since $N / k = 3 k 2^{k}$ , [L4] applied at $\log x$ gives $\log x \leq x - 1$ for $x > 0$ . Hence the exponent in step 3.4 is at most $k (1 + 2 + (k - 1) + k - 3 k) + k / 2^{k} = k (2 - k) + k / 2^{k} < 0$ , using $\log 3 \leq 2$ , $\log k \leq k - 1$ , and $\log 2 \leq 1$ . Thus $F_{k} (N) < 1$ .

step 3.4L4L6algebra

5.1

Monotonicity from step 3.1, together with the initial bounds in steps 3.2, 3.3, and 4.1, shows $F_{k} (n) < 1$ in every case. Since step 2.1 bounds the failure union by $F_{k} (n)$ , [L3] makes its complement positive; that event is nonempty by [L7].

step 2.1step 3.1step 3.2step 3.3step 4.1L3L7cases-exhaustive

6.1

In the resulting tournament every set of size exactly $k$ has a dominator. Any smaller set extends to a $k$ -set because $n \geq k$ , and the same dominator works; hence [L1] gives property $S_{k}$ .

step 5.1L1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

86 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

M. Bucic, Probabilistic Method, Theorem 1.5 (standard reference, not scraped)

If k≥1k≥1 and n≥3k22kn≥3k22k, an nn-vertex tournament with property SkSk​ exists