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

Closed

subfish-zhou wants to merge 26 commits intomo271:mainfrom

subfish-zhou:main

Commits on Mar 11, 2026

Chapter 28: Complete formalization of Pigeon-hole and Double Counting
subfish-zhou
committed
Fix linter warnings + add Mathlib source annotations
subfish-zhou
committed

Commits on Mar 13, 2026

Commits on Mar 14, 2026

Ch20: recover HGA three proofs + Mantel AM-GM + Laguerre (zero sorry)
subfish-zhou
committed
Ch20: add Erdős-Gallai framework (2 sorry remaining: HM-GM + integral bound)
subfish-zhou
committed
Ch20: fill Erdős-Gallai HM-GM + main theorem (zero sorry)
subfish-zhou
committed
Ch20: complete integral layer — Pólya symmetrization fully formalized (zero sorry)
subfish-zhou
committed
Tex: fill all TODOs from original book, align proof descriptions with Lean
subfish-zhou
committed
Ch20: add Laguerre endpoint formula (laguerre_root_interval)
subfish-zhou
committed
Align with original book: clean tex notes, restructure Ch44 proof to match book's 5 steps
subfish-zhou
committed
Ch44: add Dedekind infinite descent proof matching original book, keep coprime as alt
subfish-zhou
committed
Update module docs: Ch20 complete checklist, remove Yachiyo from Ch30 authors
subfish-zhou
committed
Rebuild blueprint PDF with updated tex
subfish-zhou
committed
Ch20: fix all 9 warnings (unused simp args, unused variables)
subfish-zhou
committed
Ch20: replace TODO comment with proper docstring on Mantel equality condition
subfish-zhou
committed
Ch20: add mantel_eq_adj_degree (equality condition, first step)
subfish-zhou
committed
Ch20: complete Mantel equality condition — regular + complete bipartite
subfish-zhou
committed
Ch28 tex: add 4 missing \leanok tags
subfish-zhou
committed

Commits on Mar 16, 2026