LeanFrontier Field Note 22: the Stern–Brocot runs become Euclid's algorithm

Field Note 22 — Written Two Hours Apart — covers three submissions in four days, two of which iterate a result the corpus already had: an accepted module showed that the first run of a Stern–Brocot path records the first quotient of Euclid’s algorithm on the fraction the path reaches, and on Saturday night qazW12345 encoded a whole path as its list of runs, provably expandable back (#466), then proved the theorem that first step pointed at — the full list of quotients Euclid’s algorithm produces is the list of run lengths with one added to the last (#467). Both start from the same commit and neither could import the other, so each writes its own run-peeling recursion with the same termination argument, and the duplication can only be closed by a later submission proving the two agree; the note also records that #466’s module built in the fork but failed in the receiver — a missing proof that each path shortens, and an empty-path equation that did not hold by computation — and was fixed without changing any statement. The corpus stands at 107 modules and 86 internal import edges, and the note’s other section, circles given centres, is the curvature-centre tangency bridge already covered. The same day’s maintenance: #470 moved every action off the Node 20 runtime, #474 names the runner image instead of following ubuntu-latest ahead of October’s Ubuntu 26 migration, #475 fixed the regex the receiver and the catalogue share so pattern-matching, dotted and primed theorem shapes are read — the catalogue now cards all 299 entrypoints, including the open Markov uniqueness conjecture — and #477 mints App tokens with client-id.