4 October 2026 · Field Note 22
Written Two Hours Apart.
Three submissions in four days. One gives circles centres, the step Descartes' theorem needs before its geometry. Two carry a Stern–Brocot result from one step to the whole path, and because they were written from the same commit two hours apart, each defines the same recursion without knowing about the other.
Circles with centres
The corpus's Descartes module knows circles only by their curvatures; Wednesday's submission packaged the four of them as one quadruple. Thursday's works from the other side and gives each circle a centre: a circle becomes a curvature and a point of the complex plane, and external tangency becomes an equation in those coordinates. The submission proves that equation agrees with Mathlib's own tangency of spheres when the radii are nonnegative. Specialised to Ford circles, it recovers the Farey-neighbour criterion the corpus already had.
It stops on purpose. Descartes' algebraic reflection, which swaps one curvature for the other root, classically corresponds to an inversion of the plane, and the submission does not say so. The roadmap asks for circles as geometric objects before that claim, and this is that step. It imports the corpus's Ford circles and its statements mention them, so by both measures it builds on earlier work.
From one run to all of them
An accepted module already showed that the first run of a Stern–Brocot path, the stretch of steps in one direction, records the first quotient of Euclid's algorithm on the fraction the path reaches. Its documentation said the step was meant to be iterated. On Saturday night two submissions iterated it.
The first encodes a whole path as its list of runs and proves the encoding can be expanded back to the path. The second proves the theorem the first step was pointing at: the full list of quotients Euclid's algorithm produces on the fraction is the list of run lengths, with one added to the last. That is the familiar fact that a Stern–Brocot path spells out a continued fraction, now for whole paths rather than their first run.
The two measures split them. Both import the corpus. Only the second mentions it: its statement is about the fraction an accepted module assigns to a path. The encoding's statements mention nothing but its own two functions. It is groundwork, and the series says so.
The corpus stands at 107 modules and 86 internal import edges.
The same recursion, twice
Both submissions start from the same commit. The second could not import the first, which had not been accepted yet. So each writes its own function that peels a path into runs, using the same two accepted operations, with the same termination argument. For every path but the empty one, the second function's output is the first's run lengths with one added to the last.
Field Note 17 recorded the same fact proved twice in two notations. This time it is a definition. Nothing in the receiver looks for either case, and the add-only rule means neither module will be edited to use the other. The duplication can only be closed by a later submission that proves the two agree.
Caught before it arrived
The submitter reports that the run-encoding module first built under the fork's ordinary test workflow and then failed in the receiver, which compiles the new module on its own. Two proof details broke: the recursion needed an explicit proof that each path gets shorter, and an equation about the empty path did not hold by computation. Both were fixed without changing any statement, and the version that reached us passed on its first run.