Relationship to the companion textbook

Chapters 2 through 6 of this blueprint are imported verbatim from the companion textbook with \lean{} annotations added at each theorem or definition whose informal statement corresponds to a formal declaration. The prose is otherwise unchanged. Figures are reused from the textbook.

Chapter 7 is the one chapter whose content does not appear in the textbook, because the Borel-analytic separation and the WellBehavedVCMeasTarget refinement of the fundamental theorem were discovered during the formalization work and are outside the textbook’s scope. The prose in that chapter is therefore written from scratch in the voice of the kernel rather than imported.