TDAF surfaces

The surfaces of TDAF, one directory per textbook and each aligned to its text section by section. A surface states a book's results in the book's own terms and proves them from Tdaf, the backbone: it is the integration test the backbone has to pass, not a place to prove new mathematics. A surface whose proof does not go through the backbone is a sign the backbone is missing something.

The dependency runs one way and never the other, which is why this is a library of its own: Tdaf builds and is read without any of it.

TdafSurface.Common holds what a surface shares with the next one rather than with a book. TdafSurface.Common.Euclidean instantiates the backbone's duality theory at ℝⁿ, so that a book working in coordinates does not restate it.

Rockafellar, Convex Analysis

TdafSurface.Rockafellar is the surface for R. T. Rockafellar, Convex Analysis (Princeton, 1970), covering all thirty-nine sections of the book over Tdaf.Analysis.Convex. Every numbered result is formalized except the five making up §22's elementary-vector development, which is combinatorial matroid theory that the book itself presents as independent of convexity. That module is the project's index: it carries the section-by-section outline and the places where formalizing the book corrected it.

Surface declarations are named for the results they state, so the name is the index: theorem_33_1 is Theorem 33.1 and corollary_37_5_2 is Corollary 37.5.2. Where one numbered result needs several declarations — its clauses, or the two directions of an equivalence — a trailing word distinguishes them, as in theorem_37_5_a and theorem_34_2_dom₁. Everything sits in the flat Rockafellar namespace.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970.