The Friendship Theorem

Definitions and Statement

• A Friendship graph is one in which any two distinct vertices have exactly one neighbor in common
• A 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.

• Assume G is a finite friendship graph.
• First we show that any two nonadjacent vertices have the same degree
• Assume for contradiction that G does not have a politician.
• Conclude from the last two points that G is d-regular for some d : ℕ.
• Show that G has d ^ 2 - d + 1 vertices.
• By casework, show that if d = 0, 1, 2, then G has a politician.
• If 3 ≤ d, let p be a prime factor of d - 1.
• If A is the adjacency matrix of G with entries in ℤ/pℤ, we show that A ^ p has trace 1.
• This gives a contradiction, as A has trace 0, and thus A ^ p has trace 0.

References

• P. Erdős, A. Rényi, V. Sós, On A Problem of Graph Theory
• C. Huneke, The Friendship Theorem

def Theorems100.Friendship {V : Type u} (G : SimpleGraph V) [Fintype V] : Prop

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.

Equations

• Theorems100.Friendship G = ∀ ⦃v w : V⦄, v ≠ w → Fintype.card ↑(G.commonNeighbors v w) = 1

def Theorems100.ExistsPolitician {V : Type u} (G : SimpleGraph V) : Prop

A politician is a vertex that is adjacent to all other vertices.

Equations

• Theorems100.ExistsPolitician G = ∃ (v : V), ∀ (w : V), v ≠ w → G.Adj v w

theorem Theorems100.Friendship.adjMatrix_sq_of_ne {V : Type u} (R : Type v) [Semiring R] [Fintype V] {G : SimpleGraph V} (hG : Theorems100.Friendship G) {v w : V} (hvw : v ≠ w) : (SimpleGraph.adjMatrix R G ^ 2) v w = 1

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.

theorem Theorems100.Friendship.adjMatrix_pow_three_of_not_adj {V : Type u} (R : Type v) [Semiring R] [Fintype V] {G : SimpleGraph V} (hG : Theorems100.Friendship G) {v w : V} (non_adj : ¬G.Adj v w) : (SimpleGraph.adjMatrix R G ^ 3) v w = ↑(G.degree v)

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.

theorem Theorems100.Friendship.degree_eq_of_not_adj {V : Type u} [Fintype V] {G : SimpleGraph V} (hG : Theorems100.Friendship G) {v w : V} (hvw : ¬G.Adj v w) : G.degree v = G.degree w

As v and w not being adjacent implies degree G v = ((G.adjMatrix R) ^ 3) v w and degree G w = ((G.adjMatrix R) ^ 3) v w, the degrees are equal if ((G.adjMatrix R) ^ 3) v w = ((G.adjMatrix R) ^ 3) w v

This is true as the adjacency matrix is symmetric.

theorem Theorems100.Friendship.adjMatrix_sq_of_regular {V : Type u} {R : Type v} [Semiring R] [Fintype V] {G : SimpleGraph V} {d : ℕ} (hG : Theorems100.Friendship G) (hd : G.IsRegularOfDegree d) : SimpleGraph.adjMatrix R G ^ 2 = Matrix.of fun (v w : V) => if v = w then ↑d else 1

Let A be the adjacency matrix of a graph G. If G is a friendship graph, then all of the off-diagonal entries of A^2 are 1. If G is d-regular, then all of the diagonal entries of A^2 are d. Putting these together determines A^2 exactly for a d-regular friendship graph.

theorem Theorems100.Friendship.adjMatrix_sq_mod_p_of_regular {V : Type u} [Fintype V] {G : SimpleGraph V} {d : ℕ} (hG : Theorems100.Friendship G) {p : ℕ} (dmod : ↑d = 1) (hd : G.IsRegularOfDegree d) : SimpleGraph.adjMatrix (ZMod p) G ^ 2 = Matrix.of fun (x x : V) => 1

theorem Theorems100.Friendship.isRegularOf_not_existsPolitician {V : Type u} [Fintype V] {G : SimpleGraph V} (hG : Theorems100.Friendship G) [Nonempty V] (hG' : ¬Theorems100.ExistsPolitician G) : ∃ (d : ℕ), G.IsRegularOfDegree d

If 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.

theorem Theorems100.Friendship.card_of_regular {V : Type u} [Fintype V] {G : SimpleGraph V} {d : ℕ} (hG : Theorems100.Friendship G) [Nonempty V] (hd : G.IsRegularOfDegree d) : d + (Fintype.card V - 1) = d * d

Let A be the adjacency matrix of a d-regular friendship graph, and let v be a vector all of whose components are 1. Then 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.

theorem Theorems100.Friendship.card_mod_p_of_regular {V : Type u} [Fintype V] {G : SimpleGraph V} {d : ℕ} (hG : Theorems100.Friendship G) [Nonempty V] {p : ℕ} (dmod : ↑d = 1) (hd : G.IsRegularOfDegree d) : ↑(Fintype.card V) = 1

The size of a d-regular friendship graph is 1 mod (d-1), and thus 1 mod p for a factor p ∣ d-1.

theorem Theorems100.Friendship.adjMatrix_sq_mul_const_one_of_regular {V : Type u} {R : Type v} [Semiring R] [Fintype V] {G : SimpleGraph V} {d : ℕ} (hd : G.IsRegularOfDegree d) : (SimpleGraph.adjMatrix R G * Matrix.of fun (x x : V) => 1) = Matrix.of fun (x x : V) => ↑d

theorem Theorems100.Friendship.adjMatrix_mul_const_one_mod_p_of_regular {V : Type u} [Fintype V] {G : SimpleGraph V} {d p : ℕ} (dmod : ↑d = 1) (hd : G.IsRegularOfDegree d) : (SimpleGraph.adjMatrix (ZMod p) G * Matrix.of fun (x x : V) => 1) = Matrix.of fun (x x : V) => 1

theorem Theorems100.Friendship.adjMatrix_pow_mod_p_of_regular {V : Type u} [Fintype V] {G : SimpleGraph V} {d : ℕ} (hG : Theorems100.Friendship G) {p : ℕ} (dmod : ↑d = 1) (hd : G.IsRegularOfDegree d) {k : ℕ} (hk : 2 ≤ k) : SimpleGraph.adjMatrix (ZMod p) G ^ k = Matrix.of fun (x x : V) => 1

Modulo a factor of d-1, the square and all higher powers of the adjacency matrix of a d-regular friendship graph reduce to the matrix whose entries are all 1.

theorem Theorems100.Friendship.false_of_three_le_degree {V : Type u} [Fintype V] {G : SimpleGraph V} {d : ℕ} (hG : Theorems100.Friendship G) [Nonempty V] (hd : G.IsRegularOfDegree d) (h : 3 ≤ d) : False

This is the main proof. Assuming that 3 ≤ d, we take p to be a prime factor of d-1. Then the pth power of the adjacency matrix of a d-regular friendship graph must have trace 1 mod 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.

theorem Theorems100.Friendship.existsPolitician_of_degree_le_one {V : Type u} [Fintype V] {G : SimpleGraph V} {d : ℕ} (hG : Theorems100.Friendship G) [Nonempty V] (hd : G.IsRegularOfDegree d) (hd1 : d ≤ 1) : Theorems100.ExistsPolitician G

If d ≤ 1, a d-regular friendship graph has at most one vertex, which is trivially a politician.

theorem Theorems100.Friendship.neighborFinset_eq_of_degree_eq_two {V : Type u} [Fintype V] {G : SimpleGraph V} (hG : Theorems100.Friendship G) [Nonempty V] (hd : G.IsRegularOfDegree 2) (v : V) : G.neighborFinset v = Finset.univ.erase v

If d = 2, a d-regular friendship graph has 3 vertices, so it must be complete graph, and all the vertices are politicians.

theorem Theorems100.Friendship.existsPolitician_of_degree_eq_two {V : Type u} [Fintype V] {G : SimpleGraph V} (hG : Theorems100.Friendship G) [Nonempty V] (hd : G.IsRegularOfDegree 2) : Theorems100.ExistsPolitician G

theorem Theorems100.Friendship.existsPolitician_of_degree_le_two {V : Type u} [Fintype V] {G : SimpleGraph V} {d : ℕ} (hG : Theorems100.Friendship G) [Nonempty V] (hd : G.IsRegularOfDegree d) (h : d ≤ 2) : Theorems100.ExistsPolitician G

theorem Theorems100.friendship_theorem {V : Type u} [Fintype V] {G : SimpleGraph V} (hG : Theorems100.Friendship G) [Nonempty V] : Theorems100.ExistsPolitician G

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 d, and now we do casework on d. 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.