The Friendship Theorem #
Definitions and Statement #
friendshipgraph is one in which any two distinct vertices have exactly one neighbor in common
politician, at least in the context of this problem, is a vertex in a graph which is adjacent to every other vertex.
- The friendship theorem (Erdős, Rényi, Sós 1966) states that every finite friendship graph has a politician.
Proof outline #
The proof revolves around the theory of adjacency matrices, although some steps could equivalently be phrased in terms of counting walks.
Gis a finite friendship graph.
- First we show that any two nonadjacent vertices have the same degree
- Assume for contradiction that
Gdoes not have a politician.
- Conclude from the last two points that
d-regular for some
d : ℕ.
- Show that
d ^ 2 - d + 1vertices.
- By casework, show that if
d = 0, 1, 2, then
Ghas a politician.
3 ≤ d, let
pbe a prime factor of
d - 1.
Ais the adjacency matrix of
Gwith entries in
ℤ/pℤ, we show that
A ^ phas trace
- This gives a contradiction, as
0, and thus
A ^ phas trace
This property of a graph is the hypothesis of the friendship theorem: every pair of nonadjacent vertices has exactly one common friend, a vertex to which both are adjacent.
- theorems_100.friendship G = ∀ ⦃v w : V⦄, v ≠ w → fintype.card ↥(G.common_neighbors v w) = 1
A politician is a vertex that is adjacent to all other vertices.
One characterization of a friendship graph is that there is exactly one walk of length 2 between distinct vertices. These walks are counted in off-diagonal entries of the square of the adjacency matrix, so for a friendship graph, those entries are all 1.
This calculation amounts to counting the number of length 3 walks between nonadjacent vertices. We use it to show that nonadjacent vertices have equal degrees.
w not being adjacent implies
degree G v = ((G.adj_matrix R) ^ 3) v w and
degree G w = ((G.adj_matrix R) ^ 3) v w,
the degrees are equal if
((G.adj_matrix R) ^ 3) v w = ((G.adj_matrix R) ^ 3) w v
This is true as the adjacency matrix is symmetric.
A be the adjacency matrix of a graph
G is a friendship graph, then all of the off-diagonal entries of
A^2 are 1.
d-regular, then all of the diagonal entries of
Putting these together determines
A^2 exactly for a
d-regular friendship graph.
G is a friendship graph without a politician (a vertex adjacent to all others), then
it is regular. We have shown that nonadjacent vertices of a friendship graph have the same degree,
and if there isn't a politician, we can show this for adjacent vertices by finding a vertex
neither is adjacent to, and then using transitivity.
A be the adjacency matrix of a
d-regular friendship graph, and let
v be a vector
all of whose components are
v is an eigenvector of
A ^ 2, and we can compute
the eigenvalue to be
d * d, or as
d + (fintype.card V - 1), so those quantities must be equal.
This essentially means that the graph has
d ^ 2 - d + 1 vertices.
The size of a
d-regular friendship graph is
1 mod (d-1), and thus
1 mod p for a
p ∣ d-1.
Modulo a factor of
d-1, the square and all higher powers of the adjacency matrix
d-regular friendship graph reduce to the matrix whose entries are all 1.
This is the main proof. Assuming that
3 ≤ d, we take
p to be a prime factor of
pth power of the adjacency matrix of a
d-regular friendship graph must have trace 1
p, but we can also show that the trace must be the
pth power of the trace of the original
adjacency matrix, which is 0, a contradiction.
d ≤ 1, a
d-regular friendship graph has at most one vertex, which is
trivially a politician.
d = 2, a
d-regular friendship graph has 3 vertices, so it must be complete graph,
and all the vertices are politicians.
Friendship theorem: We wish to show that a friendship graph has a politician (a vertex
adjacent to all others). We proceed by contradiction, and assume the graph has no politician.
We have already proven that a friendship graph with no politician is
d-regular for some
and now we do casework on
If the degree is at most 2, we observe by casework that it has a politician anyway.
If the degree is at least 3, the graph cannot exist.