Appendix: Geometric Infrastructure
Two pieces of infrastructure are used throughout the main text and are proved here:
every polytope has a subdivision (Section 7, used for the coarse subdivision T_0
and in the trivial regime of Section 3), and iterated barycentric subdivision refines
any subdivision to arbitrarily small mesh (Section 8, used for the fine subdivision
of Section 5.4).
The final chapter collects the remaining files of the formalization: infrastructure developed en route that the finished proof does not use.