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

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.

Graham–Pollak: a complete bipartite decomposition of $K_{n}$ has at least $n - 1$ parts

Statement

Let

$((X_{1}, Y_{1}), \dots, (X_{m}, Y_{m}))$

be a complete bipartite decomposition of the complete graph $K_{n}$ . Then

$m \geq n - 1.$

Facts & Assumptions

Given: a complete bipartite decomposition $((X_{1}, Y_{1}), \dots, (X_{m}, Y_{m}))$ of $K_{n}$ .

[F1]

In such a decomposition every edge of $K_{n}$ lies in exactly one of the complete bipartite graphs $K_{X_{k}, Y_{k}}$ (A decomposition of a graph's edge set into complete bipartite subgraphs).

[F2]

A homogeneous linear system with fewer equations than unknowns has a nonzero solution (The system $A x = b$ is consistent if and only if $rank (A) = rank ([A ∣ b])$ , Reduced row echelon form detects consistency and parametrises every solution by the nonpivot variables).

Proof

technique · contradiction

1.1assume-contraF2

Suppose, for contradiction, that $m \leq n - 2$ . Then the homogeneous real system $\sum_{i < n} x_{i} = 0, \sum_{i \in X_{k}} x_{i} = 0 for 1 \leq k \leq m$ has $m + 1 \leq n - 1 < n$ equations in the $n$ unknowns $x_{0}, \dots, x_{n - 1}$ , so [F2] gives a nonzero real solution $a = (a_{0}, \dots, a_{n - 1})$ .

1.2F1

Because each edge ${i, j}$ of $K_{n}$ lies in exactly one part by [F1], one has $\sum_{i < j} x_{i} x_{j} = \sum_{k = 1}^{m} (\sum_{i \in X_{k}} x_{i}) (\sum_{j \in Y_{k}} x_{j}) .$

2.1step 1.1step 1.2algebradischarge-contradiction∎

Substituting the solution $a$ into step 1.2 gives $0$ on the right, because every displayed sum over an $X_{k}$ is $0$ by step 1.1. On the left, $\sum_{i < j} a_{i} a_{j} = \frac{1}{2} [(\sum_{i < n} a_{i})^{2} - \sum_{i < n} a_{i}^{2}] = - \frac{1}{2} \sum_{i < n} a_{i}^{2} < 0,$ since $\sum_{i < n} a_{i} = 0$ by step 1.1 and not all $a_{i}$ are $0$ . This contradiction shows that $m \geq n - 1$ .

Remarks

The lower bound is sharp: the star decomposition of $K_{n}$ into the graphs $K_{{0}, {1, \dots, n - 1}}$ , $K_{{1}, {2, \dots, n - 1}}$ , and so on uses exactly $n - 1$ parts.

Depends on

Used by

Dependency tree · two levels

31 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

L. Babai and P. Frankl, Linear Algebra Methods in Combinatorics, §1.4 (standard reference, not scraped)
J. Matousek, Thirty-three Miniatures, Miniature 8 (standard reference, not scraped)
O. Pikhurko, An Introduction to Combinatorics, §3.3 (standard reference, not scraped)

Graham–Pollak: a complete bipartite decomposition of KnKn​ has at least n−1n−1 parts