Two Kinds of Building On.

Three quadratic fields

The first proves that the eighth cyclotomic field contains exactly three quadratic subfields: the fields of the square roots of 2, −2 and −1. It needed Tuesday's two submissions, the Galois group and the Gaussian subfield, and imports both. Yet its statements mention nothing an earlier statement mentions: only Mathlib's intermediate fields and a definition of its own. By the import measure it builds on the corpus twice over; by the statement measure, not at all. The corpus supplied its proof, not its subject.

The fifth direction

The second opens the last roadmap direction: a bridge between Descartes' theorem on four mutually tangent circles and the geometry of their centres. The corpus's Descartes module carried four separate curvature arguments and named only one reflection. This submission packages the curvatures as a single quadruple and all four reflections as one indexed linear map, and its statements tie that map back to the reflection the corpus already had. By both measures it builds on the corpus.

That is the case the statement measure was added to separate. Imports say what a proof needed. Statements say what a theorem is about. Both are true, and the notes will quote both.

Every direction of Sunday's roadmap now has accepted work. The corpus stands at 104 modules and 83 internal import edges.