Chapter 28: Complete formalization of Pigeon-hole and Double Counting

[subfish-zhou]

Chapter 28: Complete formalization of Pigeon-hole and Double Counting

Overview

This PR completes the formalization of Chapter 28 (Pigeon-hole and double counting) from Proofs from THE BOOK. All 12 propositions from the chapter are now formalized in Lean 4 with zero sorry, zero errors, and zero warnings.

This formalization was produced entirely by OpenClaw, an open-source AI agent framework powered by Claude Opus 4.6 (Anthropic) via GitHub Copilot. The agent autonomously analyzed the LaTeX blueprint, planned proof strategies, wrote Lean 4 proofs, and verified compilation. Human involvement was limited to task initiation, periodic review, and high-level guidance.

What Changed

• FormalBook/Chapter_28.lean: 87 → ~930 lines.
• blueprint/src/chapter/chapter28.tex: Updated with \lean{} tags and proof annotations.

Proposition Correspondence

#	Book Statement	Lean Declaration	Faithful?	Notes
1	Pigeon-hole principle	chapter28.pigeon_hole_principle	✅
2	Claim 1 — coprime pair from {1,…,2n}	chapter28.claim1_coprime	✅
3	Claim 2 — divisibility in {1,…,2n}	chapter28.claim2_divisible	✅
4	Claim 3 — Erdős–Szekeres theorem	chapter28.claim3_erdos_szekeres	✅	Mathlib Archive (Theorems100.erdos_szekeres)
5	Claim 4 — contiguous sum divisible by n	chapter28.claim4_contiguous_sum	✅
6	Double counting identity	chapter28.double_counting	✅	Via Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow
7	Average divisor count ∑t(j) = ∑⌊n/i⌋	chapter28.sum_divisor_count	✅
7b	Asymptotic bound Hₙ − 1 < t̄(n) ≤ Hₙ	avg_divisor_count_le_harmonic + avg_divisor_count_lower_bound	✅	Both upper and lower bounds proven
8	Handshaking lemma ∑d(v) = 2|E|	chapter28.handshaking	✅
9	Cherry inequality ∑C(d(v),2) ≤ C(n,2)	chapter28.sum_choose_deg_le_choose_card	✅
10	C₄-free edge bound (Reiman)	chapter28.c4_free_edge_bound	✅
11	Sperner's lemma	chapter28.sperner_lemma	⚠️ abstract	See below
12	Brouwer fixed point theorem (n=2)	chapter28.brouwer_fixed_point_2d	⚠️ alt proof	See below

Areas Requiring Human Review

1. Sperner's Lemma — Abstracted Geometric Conditions

The book proves Sperner's lemma for triangulations of a triangle with boundary coloring constraints. Our formalization proves an abstract parity version: given a finset with a coloring function mapping to {0,1,2}, if the sum is odd, then the number of elements colored 1 is odd.

What's missing: The geometric infrastructure — triangulation of a simplex, boundary coloring conditions derived from the labeling rule λ(v) = min{i : f(v)ᵢ < vᵢ}, and the dual-graph door-counting argument that establishes the odd-sum hypothesis.

Why: Mathlib currently lacks formalized barycentric coordinates, simplicial triangulations, and mesh refinement. The abstract parity core is mathematically correct and is the combinatorial heart of the proof, but the geometric "interface" is assumed rather than derived.

Reviewer action: Verify that the abstract statement (sperner_lemma, sperner_lemma_exists) correctly captures the combinatorial content. The geometric gap is documented in comments.

2. Brouwer Fixed Point Theorem — Alternative Proof Path

The book derives Brouwer from Sperner via triangulation sequences + compactness. Our proof uses a completely different approach:

1. S¹ is not simply connected (via covering map ℝ → AddCircle)
2. A retract of a simply connected space is simply connected
3. B² is contractible (convex), hence simply connected
4. If f has no fixed point, construct a retraction B² → S¹ (ray from f(x) through x)
5. Contradiction: S¹ would be simply connected

Why the detour: The Sperner → Brouwer path requires barycentric subdivision, triangulation sequences with mesh → 0, and Bolzano–Weierstrass extraction — none of which are in Mathlib. The covering space approach uses IsCoveringMap, SimplyConnectedSpace, and ContractibleSpace, all available in Mathlib.

Consequence: Sperner's lemma and Brouwer's theorem are both proven but logically independent in this formalization. The book's "Sperner implies Brouwer" narrative is not captured.

Reviewer action: Verify the retraction construction (rR function) and the no-retraction argument. The ray-sphere intersection involves a quadratic formula — check that the discriminant bound and root selection are correct.

Acknowledgment

This formalization was produced by OpenClaw, an open-source AI agent framework, powered by Claude Opus 4.6 (Anthropic) via GitHub Copilot. The agent autonomously analyzed the LaTeX source, planned proof strategies, wrote and verified Lean 4 proofs through an orchestrator-worker architecture. Human involvement was limited to task initiation, periodic oversight, and final review.