Pigeon-hole and double counting

TODO

• statement (pigeon_hole_principle)
• 1. Numbers
  • Claim 1 (coprime pair)
  • Claim 2 (divisibility)
• 2. Sequences
  • Claim 3 (Erdős–Szekeres) — via ErdosSzekeres (merged)
• 3. Sums
  • Claim 4 (contiguous sum divisible by n)
• Double Counting
• 4. Numbers again
  • sum_divisor_count (proved)
• 5. Graphs
  • sum_choose_deg_le_choose_card (proved)
  • c4_free_edge_bound (proved)
• 6. Sperner's Lemma
  • sperner_lemma (proved — abstract parity version)
  • sperner_lemma_exists (proved — corollary)
  • brouwer_fixed_point_2d (proved — via covering space / no-retraction argument)

Erdős–Szekeres theorem

Uses the proof by Bhavik Mehta from Mathlib's Archive: Archive.Wiedijk100Theorems.AscendingDescendingSequences.

Faithfulness note: The book assigns each element a single label tᵢ (length of the longest increasing subsequence starting at aᵢ) and applies pigeonhole to get n+1 elements with the same label, then argues they must be decreasing. The Mathlib Archive proof uses a dual-label strategy (maxInc, maxDec) and applies pigeonhole to the product {1,…,m} × {1,…,n}. The two strategies are mathematically equivalent — the dual-label approach is a natural generalization that avoids the separate "same-label implies decreasing" argument.

theorem ErdosSzekeres.erdos_szekeres_fin (m n : ℕ) (f : Fin (m * n + 1) → ℝ) (hf : Function.Injective f) : (∃ (t : Finset (Fin (m * n + 1))), m < t.card ∧ StrictMonoOn f ↑t) ∨ ∃ (t : Finset (Fin (m * n + 1))), n < t.card ∧ StrictAntiOn f ↑t

Corollary: Any injective sequence of m*n+1 elements has an increasing subsequence of length m+1 or a decreasing subsequence of length n+1.

Brouwer Fixed Point Theorem (merged from Brouwer.lean)

theorem chapter28.pigeon_hole_principle (n r : ℕ) (h : r < n) (object_to_boxes : Fin n → Fin r) : ∃ (box : Fin r) (object₁ : Fin n) (object₂ : Fin n), object₁ ≠ object₂ ∧ object_to_boxes object₁ = box ∧ object_to_boxes object₂ = box

theorem chapter28.handshaking {α : Type u_1} [Fintype α] [DecidableEq α] {G : SimpleGraph α} [DecidableRel G.Adj] : ∑ v : α, G.degree v = 2 * G.edgeFinset.card

Handshaking lemma: The sum of vertex degrees equals twice the number of edges.

This is also available in Mathlib as SimpleGraph.sum_degrees_eq_twice_card_edges, which uses darts (oriented edges) as the intermediate counting object. Our proof follows the book's double-counting argument more faithfully: we count incidence pairs (v, e) with v ∈ e, swap the summation order via Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow, then observe each edge contributes exactly 2.

theorem chapter28.claim1_coprime (n : ℕ) (S : Finset (Fin (2 * n))) (hS : n < S.card) : ∃ a ∈ S, ∃ b ∈ S, a ≠ b ∧ (↑a + 1).Coprime (↑b + 1)

Claim 1 (Coprime pair): From any n+1 numbers in {0,...,2n-1} (representing {1,...,2n}), two must be coprime (as values +1).

theorem chapter28.claim2_divisible (n : ℕ) (hn : 0 < n) (S : Finset ℕ) (hS_sub : ∀ x ∈ S, 1 ≤ x ∧ x ≤ 2 * n) (hS_card : S.card = n + 1) : ∃ a ∈ S, ∃ b ∈ S, a ≠ b ∧ a ∣ b

Claim 2: From {1, 2, ..., 2n}, any n+1 chosen numbers contain two where one divides the other.

theorem chapter28.claim3_erdos_szekeres (m n : ℕ) (f : Fin (m * n + 1) → ℝ) (hf : Function.Injective f) : (∃ (t : Finset (Fin (m * n + 1))), m < t.card ∧ StrictMonoOn f ↑t) ∨ ∃ (t : Finset (Fin (m * n + 1))), n < t.card ∧ StrictAntiOn f ↑t

Claim 3 (Erdős–Szekeres): Any injective sequence of mn+1 distinct reals has an increasing subsequence of length m+1 or a decreasing subsequence of length n+1.

theorem chapter28.claim4_contiguous_sum (n : ℕ) (hn : 0 < n) (a : Fin n → ℤ) : ∃ (l : Fin n) (r : Fin n), l ≤ r ∧ ↑n ∣ ∑ i ∈ Finset.Icc l r, a i

Claim 4 (Contiguous sum divisible by n): Given n integers, there exists a nonempty contiguous subsequence whose sum is divisible by n.

Double Counting

theorem chapter28.double_counting {α : Type u_2} {β : Type u_3} (R : Finset α) (C : Finset β) (r : α → β → Prop) [(a : α) → (b : β) → Decidable (r a b)] : ∑ p ∈ R, (Finset.bipartiteAbove r C p).card = ∑ q ∈ C, (Finset.bipartiteBelow r R q).card

Double counting: the sum over rows of the number of related columns equals the sum over columns of the number of related rows. This is a direct wrapper around Mathlib's Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow.

5. Graphs — C₄-free edge bound

theorem chapter28.sum_choose_deg_le_choose_card {V : Type u_2} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hC4 : ∀ (a b c d : V), a ≠ b → a ≠ c → a ≠ d → b ≠ c → b ≠ d → c ≠ d → ¬(G.Adj a b ∧ G.Adj b c ∧ G.Adj c d ∧ G.Adj d a)) : ∑ v : V, (G.degree v).choose 2 ≤ (Fintype.card V).choose 2

In a C₄-free graph, the sum of C(d(v), 2) over all vertices is at most C(n, 2).

This is the key combinatorial inequality: each pair of vertices can have at most one common neighbor (otherwise they'd form a 4-cycle), so the number of "cherries" (paths of length 2) is at most the number of vertex pairs.

theorem chapter28.c4_free_edge_bound {V : Type u_2} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hC4 : ∀ (a b c d : V), a ≠ b → a ≠ c → a ≠ d → b ≠ c → b ≠ d → c ≠ d → ¬(G.Adj a b ∧ G.Adj b c ∧ G.Adj c d ∧ G.Adj d a)) (n : ℕ) (hn : Fintype.card V = n) : G.edgeFinset.card ≤ ⌊↑n / 4 * (1 + √(4 * ↑n - 3))⌋₊

If a simple graph on n vertices contains no 4-cycle (C₄), then |E| ≤ ⌊n/4 · (1 + √(4n − 3))⌋.

The proof uses sum_choose_deg_le_choose_card together with the handshaking lemma and Cauchy–Schwarz / Jensen.

4. Numbers again

theorem chapter28.sum_divisor_count (n : ℕ) : ∑ j ∈ Finset.Icc 1 n, j.divisors.card = ∑ i ∈ Finset.Icc 1 n, n / i

Double counting for divisor sums: Σ_{j=1}^{n} (number of divisors of j) = Σ_{i=1}^{n} ⌊n/i⌋.

Both sides count pairs (i, j) with 1 ≤ i ≤ n, 1 ≤ j ≤ n, and i ∣ j. LHS groups by j (divisors of j), RHS groups by i (multiples of i up to n).

theorem chapter28.avg_divisor_count_le_harmonic (n : ℕ) : ∑ j ∈ Finset.Icc 1 n, ↑j.divisors.card ≤ ↑n * ∑ i ∈ Finset.Icc 1 n, 1 / ↑i

The average number of divisors is bounded by the harmonic sum: ∑ j in [1,n], t(j) ≤ n * Hₙ where t(j) = #(divisors j) and Hₙ = ∑ 1/i.

theorem chapter28.avg_divisor_count_lower_bound (n : ℕ) (hn : 0 < n) : ↑n * ∑ i ∈ Finset.Icc 1 n, 1 / ↑i - ↑n < ∑ j ∈ Finset.Icc 1 n, ↑j.divisors.card

Lower bound: ∑ t(j) > n·Hₙ − n, i.e., t̄(n) > Hₙ − 1 > log n − 1.

Dimension of Kₙ via iterated Erdős-Szekeres

The dimension of the complete graph Kₙ is the minimum number of linear orders (permutations) such that no 3-element subset is simultaneously monotone in all orders.

Theorem: dim(Kₙ) ≥ ⌈log₂(⌈log₂ n⌉)⌉ for n ≥ 3.

The proof uses an iterated Erdős-Szekeres argument: given p injective functions on n elements with n > 2^(2^p), repeated extraction of monotone subsequences (one per function) yields a subset of size > 2 that is simultaneously monotone in all functions.

This means p linear orders cannot "separate" all triples, so dim(Kₙ) > p. Taking the contrapositive with p = ⌈log₂(⌈log₂ n⌉)⌉ − 1 gives the bound.

theorem chapter28.KnDimension.erdos_szekeres_finset {n m : ℕ} (f : Fin n → ℝ) (S : Finset (Fin n)) (hcard : m * m < S.card) (hf : Set.InjOn f ↑S) : ∃ T ⊆ S, m < T.card ∧ (StrictMonoOn f ↑T ∨ StrictAntiOn f ↑T)

Erdős-Szekeres on finsets: Given a finset S of size > m² and a function f injective on S, there exists a subset T ⊆ S of size > m on which f is monotone.

theorem chapter28.KnDimension.iterated_erdos_szekeres (p : ℕ) {n : ℕ} (fs : Fin p → Fin n → ℝ) (S : Finset (Fin n)) : (∀ (i : Fin p), Set.InjOn (fs i) ↑S) → 2 ^ 2 ^ p < S.card → ∃ T ⊆ S, 2 < T.card ∧ ∀ (i : Fin p), StrictMonoOn (fs i) ↑T ∨ StrictAntiOn (fs i) ↑T

Iterated Erdős-Szekeres: Given p injective functions on Fin n and a finset S with |S| > 2^(2^p), there exists a subset T ⊆ S with |T| > 2 that is simultaneously monotone (each function is either strictly increasing or strictly decreasing on T).

theorem chapter28.KnDimension.kn_dimension_bound (p n : ℕ) (hn : 2 ^ 2 ^ p < n) (fs : Fin p → Fin n → ℝ) (hfs : ∀ (i : Fin p), Function.Injective (fs i)) : ∃ (T : Finset (Fin n)), 2 < T.card ∧ ∀ (i : Fin p), StrictMonoOn (fs i) ↑T ∨ StrictAntiOn (fs i) ↑T

Simultaneous monotone triple: For n > 2^(2^p) and p injective functions Fin n → ℝ, there exists a subset of size > 2 that is monotone for all of them.

This captures the lower bound dim(Kₙ) ≥ ⌈log₂(⌈log₂ n⌉)⌉: fewer than ⌈log₂(⌈log₂ n⌉)⌉ linear orders cannot separate all triples.

theorem chapter28.KnDimension.kn_dimension_clog_bound (n p : ℕ) (hp : p < Nat.clog 2 (Nat.clog 2 n)) (fs : Fin p → Fin n → ℝ) (hfs : ∀ (i : Fin p), Function.Injective (fs i)) : ∃ (T : Finset (Fin n)), 2 < T.card ∧ ∀ (i : Fin p), StrictMonoOn (fs i) ↑T ∨ StrictAntiOn (fs i) ↑T

Ceiling-log formulation: If p < ⌈log₂(⌈log₂ n⌉)⌉, then p injective functions on Fin n cannot separate all triples. This is the dim(Kₙ) ≥ ⌈log₂(⌈log₂ n⌉)⌉ bound.

6. Sperner's Lemma

theorem chapter28.brouwer_fixed_point_2d_from_sperner (f : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2)) (hf : Continuous f) (hB : ∀ (x : EuclideanSpace ℝ (Fin 2)), ‖x‖ ≤ 1 → ‖f x‖ ≤ 1) : ∃ (x : EuclideanSpace ℝ (Fin 2)), ‖x‖ ≤ 1 ∧ f x = x

Transfer from simplex to disk.

Brouwer's fixed point theorem (n = 2)

theorem chapter28.brouwer_fixed_point_2d (f : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2)) (hf : Continuous f) (hB : ∀ (x : EuclideanSpace ℝ (Fin 2)), ‖x‖ ≤ 1 → ‖f x‖ ≤ 1) : ∃ (x : EuclideanSpace ℝ (Fin 2)), ‖x‖ ≤ 1 ∧ f x = x

The Reiman graph Gp: a tight construction for the C₄-free bound

The book constructs a graph Gp for each odd prime p:

• Vertices = points of PG(2,p), i.e., one-dimensional subspaces of (ZMod p)³
• Two vertices [u],[v] are adjacent iff ⟨u,v⟩ = u₁v₁ + u₂v₂ + u₃v₃ = 0
• Gp is C₄-free
• Edge count achieves the bound from c4_free_edge_bound

We use Mathlib's Projectivization and Projectivization.orthogonal.

@[reducible, inline]

abbrev chapter28.PG2 (p : ℕ) [Fact (Nat.Prime p)] : Type

The projective plane over 𝔽ₚ.

Equations

• chapter28.PG2 p = Projectivization (ZMod p) (Fin 3 → ZMod p)

noncomputable def chapter28.reimanGraph (p : ℕ) [Fact (Nat.Prime p)] : SimpleGraph (PG2 p)

The Reiman graph Gp: vertices are points of PG(2,p), adjacency is orthogonality.

Equations

• chapter28.reimanGraph p = { Adj := fun (v w : chapter28.PG2 p) => v ≠ w ∧ Projectivization.orthogonal v w, symm := ⋯, loopless := ⋯ }

theorem chapter28.reimanGraph_card_vertices (p : ℕ) [Fact (Nat.Prime p)] : Nat.card (PG2 p) = p ^ 2 + p + 1

The number of vertices of Gp is p² + p + 1. Note: The tex assumes p is an odd prime, but oddness is not needed for the cardinality formula — only that p is a prime (hence ZMod p is a field).

theorem chapter28.orthogonal_both_eq_cross {F : Type u_2} [Field F] [DecidableEq F] {a c : Projectivization F (Fin 3 → F)} (hac : a ≠ c) {x : Projectivization F (Fin 3 → F)} (hxa : x.orthogonal a) (hxc : x.orthogonal c) : x = a.cross c

In PG(2,F), if a point x is orthogonal to two distinct points a and c, then x = cross a c. This is the uniqueness of the intersection of two hyperplanes (each hyperplane is the set of points orthogonal to a given point). Proof: by the BAC-CAB identity, w × (u × v) = (w·v)u − (u·w)v = 0 when w·u = 0 and w·v = 0, so the representatives are proportional.

theorem chapter28.reimanGraph_no_C4 (p : ℕ) [Fact (Nat.Prime p)] (a b c d : PG2 p) : a ≠ c → b ≠ d → ¬((reimanGraph p).Adj a b ∧ (reimanGraph p).Adj b c ∧ (reimanGraph p).Adj c d ∧ (reimanGraph p).Adj d a)

Key lemma for no C₄: if two distinct points v, w are both orthogonal to two distinct points a, b, then v = w. Equivalently, the "orthogonal complement" hyperplanes of distinct points intersect in at most a single projective point.

This is the projective geometry fact that two distinct hyperplanes in PG(2,p) meet in exactly one point.

Note: The tex states this for 4 distinct vertices (6 pairwise ≠ conditions), but the proof only needs a ≠ c and b ≠ d. The other four ≠ conditions follow from Adj being irreflexive (loopless graph).

theorem chapter28.orthogonal_set_card (p : ℕ) [Fact (Nat.Prime p)] [Fintype (PG2 p)] (v : PG2 p) : {w : PG2 p | Projectivization.orthogonal v w}.card = p + 1

The projective hyperplane orthogonal to a point has p+1 elements.

theorem chapter28.reimanGraph_degree_eq (p : ℕ) [Fact (Nat.Prime p)] [Fintype (PG2 p)] [DecidableEq (PG2 p)] [DecidableRel (reimanGraph p).Adj] (v : PG2 p) : (reimanGraph p).degree v = if Projectivization.orthogonal v v then p else p + 1

Each vertex's degree: p if self-orthogonal, p+1 otherwise. The orthogonal hyperplane of [v] in PG(2,p) has p+1 projective points. If v·v = 0, then [v] is among them and the degree is p; otherwise p+1.