Adapting Families of Maps to Open Covers🔗

This website presents Lemma B.0.1 of Morrison and Walker's The Blob Complex (Appendix B): a complete informal proof, interleaved with the Lean 4 formalization from which it was derived.

The Lean proof is Lorenzo Luccioli's submission to the Lean proving benchmark problem families_of_maps_b01, reproduced here with the informal prose woven around it. Every line of the formalization appears on this site; the verbatim original files are in the original/ directory of the source repository. The informal proof was written by Claude by reading the Lean proof (and deliberately not the paper's Appendix B), so the prose follows the formalization's logical structure exactly — including where it departs from the paper's own argument.

All Lean code on this site is genuine: each block is elaborated and type-checked against Mathlib when the site is built, and carries hover information. Only import lines and module docstrings are omitted from the displayed blocks (imports move to the literate modules' headers; the docstrings' content became prose). Everything else is byte-identical to the original submission, as checked in CI.

The benchmark statement itself has a history worth recording: the original formalization of "boundary subpolyhedron" admitted arbitrary convex subsets of the frontier, which makes the lemma false — Lorenzo Luccioli, using Harmonic's Aristotle, gave a formal disproof, and the statement was repaired to require genuine faces of the polyhedron. The Statement chapter discusses the corrected form.